Mathbox for Glauco Siliprandi < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  hoidmv1le Structured version   Visualization version   GIF version

Theorem hoidmv1le 41328
 Description: The dimensional volume of a 1-dimensional half-open interval is less than or equal to the generalized sum of the dimensional volumes of countable half-open intervals that cover it. This is one of the two base cases of the induction of Lemma 115B of [Fremlin1] p. 29 (the other base case is the 0-dimensional case). This proof of the 1-dimensional case is given in Lemma 114B of [Fremlin1] p. 23. (Contributed by Glauco Siliprandi, 21-Nov-2020.)
Hypotheses
Ref Expression
hoidmv1le.l 𝐿 = (𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑𝑚 𝑥), 𝑏 ∈ (ℝ ↑𝑚 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘𝑥 (vol‘((𝑎𝑘)[,)(𝑏𝑘))))))
hoidmv1le.z (𝜑𝑍𝑉)
hoidmv1le.x 𝑋 = {𝑍}
hoidmv1le.a (𝜑𝐴:𝑋⟶ℝ)
hoidmv1le.b (𝜑𝐵:𝑋⟶ℝ)
hoidmv1le.c (𝜑𝐶:ℕ⟶(ℝ ↑𝑚 𝑋))
hoidmv1le.d (𝜑𝐷:ℕ⟶(ℝ ↑𝑚 𝑋))
hoidmv1le.s (𝜑X𝑘𝑋 ((𝐴𝑘)[,)(𝐵𝑘)) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
Assertion
Ref Expression
hoidmv1le (𝜑 → (𝐴(𝐿𝑋)𝐵) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗)))))
Distinct variable groups:   𝐴,𝑎,𝑏,𝑗,𝑘,𝑥   𝐵,𝑎,𝑏,𝑗,𝑘,𝑥   𝐶,𝑎,𝑏,𝑗,𝑘,𝑥   𝐷,𝑎,𝑏,𝑗,𝑘,𝑥   𝑘,𝑉   𝑋,𝑎,𝑏,𝑘,𝑥   𝑗,𝑍,𝑘,𝑥   𝜑,𝑎,𝑏,𝑗,𝑥
Allowed substitution hints:   𝜑(𝑘)   𝐿(𝑥,𝑗,𝑘,𝑎,𝑏)   𝑉(𝑥,𝑗,𝑎,𝑏)   𝑋(𝑗)   𝑍(𝑎,𝑏)

Proof of Theorem hoidmv1le
Dummy variables 𝑖 𝑤 𝑧 𝑦 𝑙 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 hoidmv1le.b . . . . . . . . . 10 (𝜑𝐵:𝑋⟶ℝ)
2 hoidmv1le.z . . . . . . . . . . . 12 (𝜑𝑍𝑉)
3 snidg 4345 . . . . . . . . . . . 12 (𝑍𝑉𝑍 ∈ {𝑍})
42, 3syl 17 . . . . . . . . . . 11 (𝜑𝑍 ∈ {𝑍})
5 hoidmv1le.x . . . . . . . . . . 11 𝑋 = {𝑍}
64, 5syl6eleqr 2861 . . . . . . . . . 10 (𝜑𝑍𝑋)
71, 6ffvelrnd 6503 . . . . . . . . 9 (𝜑 → (𝐵𝑍) ∈ ℝ)
8 hoidmv1le.a . . . . . . . . . 10 (𝜑𝐴:𝑋⟶ℝ)
98, 6ffvelrnd 6503 . . . . . . . . 9 (𝜑 → (𝐴𝑍) ∈ ℝ)
107, 9resubcld 10660 . . . . . . . 8 (𝜑 → ((𝐵𝑍) − (𝐴𝑍)) ∈ ℝ)
1110rexrd 10291 . . . . . . 7 (𝜑 → ((𝐵𝑍) − (𝐴𝑍)) ∈ ℝ*)
12 pnfxr 10294 . . . . . . . 8 +∞ ∈ ℝ*
1312a1i 11 . . . . . . 7 (𝜑 → +∞ ∈ ℝ*)
1410ltpnfd 12160 . . . . . . 7 (𝜑 → ((𝐵𝑍) − (𝐴𝑍)) < +∞)
1511, 13, 14xrltled 40004 . . . . . 6 (𝜑 → ((𝐵𝑍) − (𝐴𝑍)) ≤ +∞)
1615ad2antrr 705 . . . . 5 (((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) = +∞) → ((𝐵𝑍) − (𝐴𝑍)) ≤ +∞)
17 id 22 . . . . . . 7 ((Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) = +∞ → (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) = +∞)
1817eqcomd 2777 . . . . . 6 ((Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) = +∞ → +∞ = (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))))
1918adantl 467 . . . . 5 (((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) = +∞) → +∞ = (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))))
2016, 19breqtrd 4812 . . . 4 (((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) = +∞) → ((𝐵𝑍) − (𝐴𝑍)) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))))
21 simpl 468 . . . . 5 (((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) ∧ ¬ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) = +∞) → (𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)))
22 simpr 471 . . . . . 6 (((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) ∧ ¬ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) = +∞) → ¬ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) = +∞)
23 nnex 11228 . . . . . . . 8 ℕ ∈ V
2423a1i 11 . . . . . . 7 (((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) ∧ ¬ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) = +∞) → ℕ ∈ V)
25 hoidmv1le.l . . . . . . . . . . . 12 𝐿 = (𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑𝑚 𝑥), 𝑏 ∈ (ℝ ↑𝑚 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘𝑥 (vol‘((𝑎𝑘)[,)(𝑏𝑘))))))
265a1i 11 . . . . . . . . . . . . . 14 (𝜑𝑋 = {𝑍})
27 snfi 8194 . . . . . . . . . . . . . . 15 {𝑍} ∈ Fin
2827a1i 11 . . . . . . . . . . . . . 14 (𝜑 → {𝑍} ∈ Fin)
2926, 28eqeltrd 2850 . . . . . . . . . . . . 13 (𝜑𝑋 ∈ Fin)
3029adantr 466 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ) → 𝑋 ∈ Fin)
31 ne0i 4069 . . . . . . . . . . . . . 14 (𝑍𝑋𝑋 ≠ ∅)
326, 31syl 17 . . . . . . . . . . . . 13 (𝜑𝑋 ≠ ∅)
3332adantr 466 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ) → 𝑋 ≠ ∅)
34 hoidmv1le.c . . . . . . . . . . . . . 14 (𝜑𝐶:ℕ⟶(ℝ ↑𝑚 𝑋))
3534ffvelrnda 6502 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ ℕ) → (𝐶𝑗) ∈ (ℝ ↑𝑚 𝑋))
36 elmapi 8031 . . . . . . . . . . . . 13 ((𝐶𝑗) ∈ (ℝ ↑𝑚 𝑋) → (𝐶𝑗):𝑋⟶ℝ)
3735, 36syl 17 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ) → (𝐶𝑗):𝑋⟶ℝ)
38 hoidmv1le.d . . . . . . . . . . . . . 14 (𝜑𝐷:ℕ⟶(ℝ ↑𝑚 𝑋))
3938ffvelrnda 6502 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ ℕ) → (𝐷𝑗) ∈ (ℝ ↑𝑚 𝑋))
40 elmapi 8031 . . . . . . . . . . . . 13 ((𝐷𝑗) ∈ (ℝ ↑𝑚 𝑋) → (𝐷𝑗):𝑋⟶ℝ)
4139, 40syl 17 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ) → (𝐷𝑗):𝑋⟶ℝ)
4225, 30, 33, 37, 41hoidmvn0val 41318 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗)) = ∏𝑘𝑋 (vol‘(((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))))
435prodeq1i 14855 . . . . . . . . . . . 12 𝑘𝑋 (vol‘(((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) = ∏𝑘 ∈ {𝑍} (vol‘(((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
4443a1i 11 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ℕ) → ∏𝑘𝑋 (vol‘(((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) = ∏𝑘 ∈ {𝑍} (vol‘(((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))))
452adantr 466 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ) → 𝑍𝑉)
466adantr 466 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ ℕ) → 𝑍𝑋)
4737, 46ffvelrnd 6503 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗)‘𝑍) ∈ ℝ)
4841, 46ffvelrnd 6503 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ ℕ) → ((𝐷𝑗)‘𝑍) ∈ ℝ)
49 volicore 41315 . . . . . . . . . . . . . 14 ((((𝐶𝑗)‘𝑍) ∈ ℝ ∧ ((𝐷𝑗)‘𝑍) ∈ ℝ) → (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))) ∈ ℝ)
5047, 48, 49syl2anc 573 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ ℕ) → (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))) ∈ ℝ)
5150recnd 10270 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ) → (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))) ∈ ℂ)
52 fveq2 6332 . . . . . . . . . . . . . . 15 (𝑘 = 𝑍 → ((𝐶𝑗)‘𝑘) = ((𝐶𝑗)‘𝑍))
53 fveq2 6332 . . . . . . . . . . . . . . 15 (𝑘 = 𝑍 → ((𝐷𝑗)‘𝑘) = ((𝐷𝑗)‘𝑍))
5452, 53oveq12d 6811 . . . . . . . . . . . . . 14 (𝑘 = 𝑍 → (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) = (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))
5554fveq2d 6336 . . . . . . . . . . . . 13 (𝑘 = 𝑍 → (vol‘(((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) = (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))
5655prodsn 14899 . . . . . . . . . . . 12 ((𝑍𝑉 ∧ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))) ∈ ℂ) → ∏𝑘 ∈ {𝑍} (vol‘(((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) = (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))
5745, 51, 56syl2anc 573 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ℕ) → ∏𝑘 ∈ {𝑍} (vol‘(((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) = (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))
5842, 44, 573eqtrd 2809 . . . . . . . . . 10 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗)) = (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))
5958mpteq2dva 4878 . . . . . . . . 9 (𝜑 → (𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗))) = (𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))))
60 fveq2 6332 . . . . . . . . . . . . . . . . . . . 20 (𝑘 = 𝑙 → (𝑎𝑘) = (𝑎𝑙))
61 fveq2 6332 . . . . . . . . . . . . . . . . . . . 20 (𝑘 = 𝑙 → (𝑏𝑘) = (𝑏𝑙))
6260, 61oveq12d 6811 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 𝑙 → ((𝑎𝑘)[,)(𝑏𝑘)) = ((𝑎𝑙)[,)(𝑏𝑙)))
6362fveq2d 6336 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑙 → (vol‘((𝑎𝑘)[,)(𝑏𝑘))) = (vol‘((𝑎𝑙)[,)(𝑏𝑙))))
6463cbvprodv 14853 . . . . . . . . . . . . . . . . 17 𝑘𝑥 (vol‘((𝑎𝑘)[,)(𝑏𝑘))) = ∏𝑙𝑥 (vol‘((𝑎𝑙)[,)(𝑏𝑙)))
65 ifeq2 4230 . . . . . . . . . . . . . . . . 17 (∏𝑘𝑥 (vol‘((𝑎𝑘)[,)(𝑏𝑘))) = ∏𝑙𝑥 (vol‘((𝑎𝑙)[,)(𝑏𝑙))) → if(𝑥 = ∅, 0, ∏𝑘𝑥 (vol‘((𝑎𝑘)[,)(𝑏𝑘)))) = if(𝑥 = ∅, 0, ∏𝑙𝑥 (vol‘((𝑎𝑙)[,)(𝑏𝑙)))))
6664, 65ax-mp 5 . . . . . . . . . . . . . . . 16 if(𝑥 = ∅, 0, ∏𝑘𝑥 (vol‘((𝑎𝑘)[,)(𝑏𝑘)))) = if(𝑥 = ∅, 0, ∏𝑙𝑥 (vol‘((𝑎𝑙)[,)(𝑏𝑙))))
6766a1i 11 . . . . . . . . . . . . . . 15 ((𝑎 ∈ (ℝ ↑𝑚 𝑥) ∧ 𝑏 ∈ (ℝ ↑𝑚 𝑥)) → if(𝑥 = ∅, 0, ∏𝑘𝑥 (vol‘((𝑎𝑘)[,)(𝑏𝑘)))) = if(𝑥 = ∅, 0, ∏𝑙𝑥 (vol‘((𝑎𝑙)[,)(𝑏𝑙)))))
6867mpt2eq3ia 6867 . . . . . . . . . . . . . 14 (𝑎 ∈ (ℝ ↑𝑚 𝑥), 𝑏 ∈ (ℝ ↑𝑚 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘𝑥 (vol‘((𝑎𝑘)[,)(𝑏𝑘))))) = (𝑎 ∈ (ℝ ↑𝑚 𝑥), 𝑏 ∈ (ℝ ↑𝑚 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑙𝑥 (vol‘((𝑎𝑙)[,)(𝑏𝑙)))))
6968mpteq2i 4875 . . . . . . . . . . . . 13 (𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑𝑚 𝑥), 𝑏 ∈ (ℝ ↑𝑚 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘𝑥 (vol‘((𝑎𝑘)[,)(𝑏𝑘)))))) = (𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑𝑚 𝑥), 𝑏 ∈ (ℝ ↑𝑚 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑙𝑥 (vol‘((𝑎𝑙)[,)(𝑏𝑙))))))
7025, 69eqtri 2793 . . . . . . . . . . . 12 𝐿 = (𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑𝑚 𝑥), 𝑏 ∈ (ℝ ↑𝑚 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑙𝑥 (vol‘((𝑎𝑙)[,)(𝑏𝑙))))))
7170, 30, 37, 41hoidmvcl 41316 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗)) ∈ (0[,)+∞))
72 eqid 2771 . . . . . . . . . . 11 (𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗))) = (𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗)))
7371, 72fmptd 6527 . . . . . . . . . 10 (𝜑 → (𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗))):ℕ⟶(0[,)+∞))
74 icossicc 12466 . . . . . . . . . . 11 (0[,)+∞) ⊆ (0[,]+∞)
7574a1i 11 . . . . . . . . . 10 (𝜑 → (0[,)+∞) ⊆ (0[,]+∞))
7673, 75fssd 6197 . . . . . . . . 9 (𝜑 → (𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗))):ℕ⟶(0[,]+∞))
7759, 76feq1dd 39867 . . . . . . . 8 (𝜑 → (𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))):ℕ⟶(0[,]+∞))
7877ad2antrr 705 . . . . . . 7 (((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) ∧ ¬ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) = +∞) → (𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))):ℕ⟶(0[,]+∞))
7924, 78sge0repnf 41120 . . . . . 6 (((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) ∧ ¬ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) = +∞) → ((Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) ∈ ℝ ↔ ¬ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) = +∞))
8022, 79mpbird 247 . . . . 5 (((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) ∧ ¬ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) = +∞) → (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) ∈ ℝ)
819ad2antrr 705 . . . . . . 7 (((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) ∈ ℝ) → (𝐴𝑍) ∈ ℝ)
827ad2antrr 705 . . . . . . 7 (((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) ∈ ℝ) → (𝐵𝑍) ∈ ℝ)
83 simplr 752 . . . . . . 7 (((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) ∈ ℝ) → (𝐴𝑍) < (𝐵𝑍))
84 eqid 2771 . . . . . . . . 9 (𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍)) = (𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍))
8547, 84fmptd 6527 . . . . . . . 8 (𝜑 → (𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍)):ℕ⟶ℝ)
8685ad2antrr 705 . . . . . . 7 (((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) ∈ ℝ) → (𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍)):ℕ⟶ℝ)
87 eqid 2771 . . . . . . . . 9 (𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍)) = (𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))
8848, 87fmptd 6527 . . . . . . . 8 (𝜑 → (𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍)):ℕ⟶ℝ)
8988ad2antrr 705 . . . . . . 7 (((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) ∈ ℝ) → (𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍)):ℕ⟶ℝ)
90 hoidmv1le.s . . . . . . . . . . . . . . . . 17 (𝜑X𝑘𝑋 ((𝐴𝑘)[,)(𝐵𝑘)) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
915eleq2i 2842 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑘𝑋𝑘 ∈ {𝑍})
9291biimpi 206 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑘𝑋𝑘 ∈ {𝑍})
93 elsni 4333 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑘 ∈ {𝑍} → 𝑘 = 𝑍)
9492, 93syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑘𝑋𝑘 = 𝑍)
9594, 54syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘𝑋 → (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) = (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))
9695rgen 3071 . . . . . . . . . . . . . . . . . . . . 21 𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) = (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))
97 ixpeq2 8076 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) = (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) → X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) = X𝑘𝑋 (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))
9896, 97ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) = X𝑘𝑋 (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))
9998a1i 11 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ ℕ → X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) = X𝑘𝑋 (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))
10099iuneq2i 4673 . . . . . . . . . . . . . . . . . 18 𝑗 ∈ ℕ X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) = 𝑗 ∈ ℕ X𝑘𝑋 (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))
101100a1i 11 . . . . . . . . . . . . . . . . 17 (𝜑 𝑗 ∈ ℕ X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) = 𝑗 ∈ ℕ X𝑘𝑋 (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))
10290, 101sseqtrd 3790 . . . . . . . . . . . . . . . 16 (𝜑X𝑘𝑋 ((𝐴𝑘)[,)(𝐵𝑘)) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))
103102adantr 466 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ ((𝐴𝑍)[,)(𝐵𝑍))) → X𝑘𝑋 ((𝐴𝑘)[,)(𝐵𝑘)) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))
104 id 22 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ((𝐴𝑍)[,)(𝐵𝑍)) → 𝑥 ∈ ((𝐴𝑍)[,)(𝐵𝑍)))
105 eqidd 2772 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ((𝐴𝑍)[,)(𝐵𝑍)) → {⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑥⟩})
106 opeq2 4540 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 = 𝑥 → ⟨𝑍, 𝑦⟩ = ⟨𝑍, 𝑥⟩)
107106sneqd 4328 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 = 𝑥 → {⟨𝑍, 𝑦⟩} = {⟨𝑍, 𝑥⟩})
108107eqeq2d 2781 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = 𝑥 → ({⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩} ↔ {⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑥⟩}))
109108rspcev 3460 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ∈ ((𝐴𝑍)[,)(𝐵𝑍)) ∧ {⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑥⟩}) → ∃𝑦 ∈ ((𝐴𝑍)[,)(𝐵𝑍)){⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩})
110104, 105, 109syl2anc 573 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ((𝐴𝑍)[,)(𝐵𝑍)) → ∃𝑦 ∈ ((𝐴𝑍)[,)(𝐵𝑍)){⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩})
111110adantl 467 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ ((𝐴𝑍)[,)(𝐵𝑍))) → ∃𝑦 ∈ ((𝐴𝑍)[,)(𝐵𝑍)){⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩})
112 elixpsn 8101 . . . . . . . . . . . . . . . . . . 19 (𝑍𝑉 → ({⟨𝑍, 𝑥⟩} ∈ X𝑘 ∈ {𝑍} ((𝐴𝑍)[,)(𝐵𝑍)) ↔ ∃𝑦 ∈ ((𝐴𝑍)[,)(𝐵𝑍)){⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩}))
1132, 112syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑 → ({⟨𝑍, 𝑥⟩} ∈ X𝑘 ∈ {𝑍} ((𝐴𝑍)[,)(𝐵𝑍)) ↔ ∃𝑦 ∈ ((𝐴𝑍)[,)(𝐵𝑍)){⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩}))
114113adantr 466 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ ((𝐴𝑍)[,)(𝐵𝑍))) → ({⟨𝑍, 𝑥⟩} ∈ X𝑘 ∈ {𝑍} ((𝐴𝑍)[,)(𝐵𝑍)) ↔ ∃𝑦 ∈ ((𝐴𝑍)[,)(𝐵𝑍)){⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩}))
115111, 114mpbird 247 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ ((𝐴𝑍)[,)(𝐵𝑍))) → {⟨𝑍, 𝑥⟩} ∈ X𝑘 ∈ {𝑍} ((𝐴𝑍)[,)(𝐵𝑍)))
1165eqcomi 2780 . . . . . . . . . . . . . . . . . . . 20 {𝑍} = 𝑋
117 ixpeq1 8073 . . . . . . . . . . . . . . . . . . . 20 ({𝑍} = 𝑋X𝑘 ∈ {𝑍} ((𝐴𝑍)[,)(𝐵𝑍)) = X𝑘𝑋 ((𝐴𝑍)[,)(𝐵𝑍)))
118116, 117ax-mp 5 . . . . . . . . . . . . . . . . . . 19 X𝑘 ∈ {𝑍} ((𝐴𝑍)[,)(𝐵𝑍)) = X𝑘𝑋 ((𝐴𝑍)[,)(𝐵𝑍))
119 fveq2 6332 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑘 = 𝑍 → (𝐴𝑘) = (𝐴𝑍))
12094, 119syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑘𝑋 → (𝐴𝑘) = (𝐴𝑍))
121 fveq2 6332 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑘 = 𝑍 → (𝐵𝑘) = (𝐵𝑍))
12294, 121syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑘𝑋 → (𝐵𝑘) = (𝐵𝑍))
123120, 122oveq12d 6811 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘𝑋 → ((𝐴𝑘)[,)(𝐵𝑘)) = ((𝐴𝑍)[,)(𝐵𝑍)))
124123eqcomd 2777 . . . . . . . . . . . . . . . . . . . . 21 (𝑘𝑋 → ((𝐴𝑍)[,)(𝐵𝑍)) = ((𝐴𝑘)[,)(𝐵𝑘)))
125124rgen 3071 . . . . . . . . . . . . . . . . . . . 20 𝑘𝑋 ((𝐴𝑍)[,)(𝐵𝑍)) = ((𝐴𝑘)[,)(𝐵𝑘))
126 ixpeq2 8076 . . . . . . . . . . . . . . . . . . . 20 (∀𝑘𝑋 ((𝐴𝑍)[,)(𝐵𝑍)) = ((𝐴𝑘)[,)(𝐵𝑘)) → X𝑘𝑋 ((𝐴𝑍)[,)(𝐵𝑍)) = X𝑘𝑋 ((𝐴𝑘)[,)(𝐵𝑘)))
127125, 126ax-mp 5 . . . . . . . . . . . . . . . . . . 19 X𝑘𝑋 ((𝐴𝑍)[,)(𝐵𝑍)) = X𝑘𝑋 ((𝐴𝑘)[,)(𝐵𝑘))
128118, 127eqtri 2793 . . . . . . . . . . . . . . . . . 18 X𝑘 ∈ {𝑍} ((𝐴𝑍)[,)(𝐵𝑍)) = X𝑘𝑋 ((𝐴𝑘)[,)(𝐵𝑘))
129128a1i 11 . . . . . . . . . . . . . . . . 17 (𝜑X𝑘 ∈ {𝑍} ((𝐴𝑍)[,)(𝐵𝑍)) = X𝑘𝑋 ((𝐴𝑘)[,)(𝐵𝑘)))
130129adantr 466 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ ((𝐴𝑍)[,)(𝐵𝑍))) → X𝑘 ∈ {𝑍} ((𝐴𝑍)[,)(𝐵𝑍)) = X𝑘𝑋 ((𝐴𝑘)[,)(𝐵𝑘)))
131115, 130eleqtrd 2852 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ ((𝐴𝑍)[,)(𝐵𝑍))) → {⟨𝑍, 𝑥⟩} ∈ X𝑘𝑋 ((𝐴𝑘)[,)(𝐵𝑘)))
132103, 131sseldd 3753 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ ((𝐴𝑍)[,)(𝐵𝑍))) → {⟨𝑍, 𝑥⟩} ∈ 𝑗 ∈ ℕ X𝑘𝑋 (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))
133 eliun 4658 . . . . . . . . . . . . . 14 ({⟨𝑍, 𝑥⟩} ∈ 𝑗 ∈ ℕ X𝑘𝑋 (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) ↔ ∃𝑗 ∈ ℕ {⟨𝑍, 𝑥⟩} ∈ X𝑘𝑋 (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))
134132, 133sylib 208 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ ((𝐴𝑍)[,)(𝐵𝑍))) → ∃𝑗 ∈ ℕ {⟨𝑍, 𝑥⟩} ∈ X𝑘𝑋 (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))
135 ixpeq1 8073 . . . . . . . . . . . . . . . . . . . . . 22 (𝑋 = {𝑍} → X𝑘𝑋 (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) = X𝑘 ∈ {𝑍} (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))
1365, 135ax-mp 5 . . . . . . . . . . . . . . . . . . . . 21 X𝑘𝑋 (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) = X𝑘 ∈ {𝑍} (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))
137136eleq2i 2842 . . . . . . . . . . . . . . . . . . . 20 ({⟨𝑍, 𝑥⟩} ∈ X𝑘𝑋 (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) ↔ {⟨𝑍, 𝑥⟩} ∈ X𝑘 ∈ {𝑍} (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))
138137biimpi 206 . . . . . . . . . . . . . . . . . . 19 ({⟨𝑍, 𝑥⟩} ∈ X𝑘𝑋 (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) → {⟨𝑍, 𝑥⟩} ∈ X𝑘 ∈ {𝑍} (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))
139138adantl 467 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ {⟨𝑍, 𝑥⟩} ∈ X𝑘𝑋 (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))) → {⟨𝑍, 𝑥⟩} ∈ X𝑘 ∈ {𝑍} (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))
140 elixpsn 8101 . . . . . . . . . . . . . . . . . . . 20 (𝑍𝑉 → ({⟨𝑍, 𝑥⟩} ∈ X𝑘 ∈ {𝑍} (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) ↔ ∃𝑦 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)){⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩}))
1412, 140syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ({⟨𝑍, 𝑥⟩} ∈ X𝑘 ∈ {𝑍} (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) ↔ ∃𝑦 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)){⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩}))
142141adantr 466 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ {⟨𝑍, 𝑥⟩} ∈ X𝑘𝑋 (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))) → ({⟨𝑍, 𝑥⟩} ∈ X𝑘 ∈ {𝑍} (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) ↔ ∃𝑦 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)){⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩}))
143139, 142mpbid 222 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ {⟨𝑍, 𝑥⟩} ∈ X𝑘𝑋 (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))) → ∃𝑦 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)){⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩})
144 opex 5060 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑍, 𝑥⟩ ∈ V
145144sneqr 4504 . . . . . . . . . . . . . . . . . . . . . . . . 25 ({⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩} → ⟨𝑍, 𝑥⟩ = ⟨𝑍, 𝑦⟩)
146145adantl 467 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ {⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩}) → ⟨𝑍, 𝑥⟩ = ⟨𝑍, 𝑦⟩)
147 vex 3354 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝑥 ∈ V
148147a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑𝑥 ∈ V)
149 opthg 5073 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑍𝑉𝑥 ∈ V) → (⟨𝑍, 𝑥⟩ = ⟨𝑍, 𝑦⟩ ↔ (𝑍 = 𝑍𝑥 = 𝑦)))
1502, 148, 149syl2anc 573 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (⟨𝑍, 𝑥⟩ = ⟨𝑍, 𝑦⟩ ↔ (𝑍 = 𝑍𝑥 = 𝑦)))
151150adantr 466 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ {⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩}) → (⟨𝑍, 𝑥⟩ = ⟨𝑍, 𝑦⟩ ↔ (𝑍 = 𝑍𝑥 = 𝑦)))
152146, 151mpbid 222 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ {⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩}) → (𝑍 = 𝑍𝑥 = 𝑦))
153152simprd 483 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ {⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩}) → 𝑥 = 𝑦)
1541533adant2 1125 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑦 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) ∧ {⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩}) → 𝑥 = 𝑦)
155 simp2 1131 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑦 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) ∧ {⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩}) → 𝑦 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))
156154, 155eqeltrd 2850 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑦 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) ∧ {⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩}) → 𝑥 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))
1571563exp 1112 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑦 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) → ({⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩} → 𝑥 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))))
158157adantr 466 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ {⟨𝑍, 𝑥⟩} ∈ X𝑘𝑋 (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))) → (𝑦 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) → ({⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩} → 𝑥 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))))
159158rexlimdv 3178 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ {⟨𝑍, 𝑥⟩} ∈ X𝑘𝑋 (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))) → (∃𝑦 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)){⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩} → 𝑥 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))
160143, 159mpd 15 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ {⟨𝑍, 𝑥⟩} ∈ X𝑘𝑋 (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))) → 𝑥 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))
161160ex 397 . . . . . . . . . . . . . . 15 (𝜑 → ({⟨𝑍, 𝑥⟩} ∈ X𝑘𝑋 (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) → 𝑥 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))
162161ad2antrr 705 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ ((𝐴𝑍)[,)(𝐵𝑍))) ∧ 𝑗 ∈ ℕ) → ({⟨𝑍, 𝑥⟩} ∈ X𝑘𝑋 (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) → 𝑥 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))
163162reximdva 3165 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ ((𝐴𝑍)[,)(𝐵𝑍))) → (∃𝑗 ∈ ℕ {⟨𝑍, 𝑥⟩} ∈ X𝑘𝑋 (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) → ∃𝑗 ∈ ℕ 𝑥 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))
164134, 163mpd 15 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ ((𝐴𝑍)[,)(𝐵𝑍))) → ∃𝑗 ∈ ℕ 𝑥 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))
165 eliun 4658 . . . . . . . . . . . 12 (𝑥 𝑗 ∈ ℕ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) ↔ ∃𝑗 ∈ ℕ 𝑥 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))
166164, 165sylibr 224 . . . . . . . . . . 11 ((𝜑𝑥 ∈ ((𝐴𝑍)[,)(𝐵𝑍))) → 𝑥 𝑗 ∈ ℕ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))
167166ralrimiva 3115 . . . . . . . . . 10 (𝜑 → ∀𝑥 ∈ ((𝐴𝑍)[,)(𝐵𝑍))𝑥 𝑗 ∈ ℕ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))
168 dfss3 3741 . . . . . . . . . 10 (((𝐴𝑍)[,)(𝐵𝑍)) ⊆ 𝑗 ∈ ℕ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) ↔ ∀𝑥 ∈ ((𝐴𝑍)[,)(𝐵𝑍))𝑥 𝑗 ∈ ℕ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))
169167, 168sylibr 224 . . . . . . . . 9 (𝜑 → ((𝐴𝑍)[,)(𝐵𝑍)) ⊆ 𝑗 ∈ ℕ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))
170 eqidd 2772 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ ℕ) → (𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍)) = (𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍)))
171 fveq2 6332 . . . . . . . . . . . . . . 15 (𝑗 = 𝑖 → (𝐶𝑗) = (𝐶𝑖))
172171fveq1d 6334 . . . . . . . . . . . . . 14 (𝑗 = 𝑖 → ((𝐶𝑗)‘𝑍) = ((𝐶𝑖)‘𝑍))
173172adantl 467 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ ℕ) ∧ 𝑗 = 𝑖) → ((𝐶𝑗)‘𝑍) = ((𝐶𝑖)‘𝑍))
174 simpr 471 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ ℕ) → 𝑖 ∈ ℕ)
175 fvexd 6344 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ ℕ) → ((𝐶𝑖)‘𝑍) ∈ V)
176170, 173, 174, 175fvmptd 6430 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ ℕ) → ((𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍))‘𝑖) = ((𝐶𝑖)‘𝑍))
177 eqidd 2772 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ ℕ) → (𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍)) = (𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍)))
178 fveq2 6332 . . . . . . . . . . . . . . 15 (𝑗 = 𝑖 → (𝐷𝑗) = (𝐷𝑖))
179178fveq1d 6334 . . . . . . . . . . . . . 14 (𝑗 = 𝑖 → ((𝐷𝑗)‘𝑍) = ((𝐷𝑖)‘𝑍))
180179adantl 467 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ ℕ) ∧ 𝑗 = 𝑖) → ((𝐷𝑗)‘𝑍) = ((𝐷𝑖)‘𝑍))
181 fvexd 6344 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ ℕ) → ((𝐷𝑖)‘𝑍) ∈ V)
182177, 180, 174, 181fvmptd 6430 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ ℕ) → ((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖) = ((𝐷𝑖)‘𝑍))
183176, 182oveq12d 6811 . . . . . . . . . . 11 ((𝜑𝑖 ∈ ℕ) → (((𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍))‘𝑖)[,)((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖)) = (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)))
184183iuneq2dv 4676 . . . . . . . . . 10 (𝜑 𝑖 ∈ ℕ (((𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍))‘𝑖)[,)((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖)) = 𝑖 ∈ ℕ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)))
185172, 179oveq12d 6811 . . . . . . . . . . . . 13 (𝑗 = 𝑖 → (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) = (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)))
186185cbviunv 4693 . . . . . . . . . . . 12 𝑗 ∈ ℕ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) = 𝑖 ∈ ℕ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍))
187186eqcomi 2780 . . . . . . . . . . 11 𝑖 ∈ ℕ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)) = 𝑗 ∈ ℕ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))
188187a1i 11 . . . . . . . . . 10 (𝜑 𝑖 ∈ ℕ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)) = 𝑗 ∈ ℕ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))
189184, 188eqtr2d 2806 . . . . . . . . 9 (𝜑 𝑗 ∈ ℕ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) = 𝑖 ∈ ℕ (((𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍))‘𝑖)[,)((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖)))
190169, 189sseqtrd 3790 . . . . . . . 8 (𝜑 → ((𝐴𝑍)[,)(𝐵𝑍)) ⊆ 𝑖 ∈ ℕ (((𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍))‘𝑖)[,)((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖)))
191190ad2antrr 705 . . . . . . 7 (((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) ∈ ℝ) → ((𝐴𝑍)[,)(𝐵𝑍)) ⊆ 𝑖 ∈ ℕ (((𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍))‘𝑖)[,)((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖)))
192 fvex 6342 . . . . . . . . . . . . . . 15 ((𝐶𝑖)‘𝑍) ∈ V
193172, 84, 192fvmpt 6424 . . . . . . . . . . . . . 14 (𝑖 ∈ ℕ → ((𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍))‘𝑖) = ((𝐶𝑖)‘𝑍))
194 fvex 6342 . . . . . . . . . . . . . . 15 ((𝐷𝑖)‘𝑍) ∈ V
195179, 87, 194fvmpt 6424 . . . . . . . . . . . . . 14 (𝑖 ∈ ℕ → ((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖) = ((𝐷𝑖)‘𝑍))
196193, 195oveq12d 6811 . . . . . . . . . . . . 13 (𝑖 ∈ ℕ → (((𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍))‘𝑖)[,)((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖)) = (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)))
197196fveq2d 6336 . . . . . . . . . . . 12 (𝑖 ∈ ℕ → (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍))‘𝑖)[,)((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖))) = (vol‘(((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍))))
198197mpteq2ia 4874 . . . . . . . . . . 11 (𝑖 ∈ ℕ ↦ (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍))‘𝑖)[,)((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖)))) = (𝑖 ∈ ℕ ↦ (vol‘(((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍))))
199 eqcom 2778 . . . . . . . . . . . . . . . 16 (𝑗 = 𝑖𝑖 = 𝑗)
200199imbi1i 338 . . . . . . . . . . . . . . 15 ((𝑗 = 𝑖 → (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) = (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍))) ↔ (𝑖 = 𝑗 → (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) = (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍))))
201 eqcom 2778 . . . . . . . . . . . . . . . 16 ((((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) = (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)) ↔ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)) = (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))
202201imbi2i 325 . . . . . . . . . . . . . . 15 ((𝑖 = 𝑗 → (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) = (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍))) ↔ (𝑖 = 𝑗 → (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)) = (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))
203200, 202bitri 264 . . . . . . . . . . . . . 14 ((𝑗 = 𝑖 → (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) = (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍))) ↔ (𝑖 = 𝑗 → (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)) = (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))
204185, 203mpbi 220 . . . . . . . . . . . . 13 (𝑖 = 𝑗 → (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)) = (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))
205204fveq2d 6336 . . . . . . . . . . . 12 (𝑖 = 𝑗 → (vol‘(((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍))) = (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))
206205cbvmptv 4884 . . . . . . . . . . 11 (𝑖 ∈ ℕ ↦ (vol‘(((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)))) = (𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))
207198, 206eqtri 2793 . . . . . . . . . 10 (𝑖 ∈ ℕ ↦ (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍))‘𝑖)[,)((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖)))) = (𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))
208207fveq2i 6335 . . . . . . . . 9 ^‘(𝑖 ∈ ℕ ↦ (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍))‘𝑖)[,)((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖))))) = (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))))
209208a1i 11 . . . . . . . 8 (((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) ∈ ℝ) → (Σ^‘(𝑖 ∈ ℕ ↦ (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍))‘𝑖)[,)((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖))))) = (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))))
210 simpr 471 . . . . . . . 8 (((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) ∈ ℝ) → (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) ∈ ℝ)
211209, 210eqeltrd 2850 . . . . . . 7 (((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) ∈ ℝ) → (Σ^‘(𝑖 ∈ ℕ ↦ (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍))‘𝑖)[,)((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖))))) ∈ ℝ)
212 oveq1 6800 . . . . . . . . 9 (𝑤 = 𝑧 → (𝑤 − (𝐴𝑍)) = (𝑧 − (𝐴𝑍)))
213195breq1d 4796 . . . . . . . . . . . . . . . . 17 (𝑖 ∈ ℕ → (((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖) ≤ 𝑧 ↔ ((𝐷𝑖)‘𝑍) ≤ 𝑧))
214213, 195ifbieq1d 4248 . . . . . . . . . . . . . . . 16 (𝑖 ∈ ℕ → if(((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖) ≤ 𝑧, ((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖), 𝑧) = if(((𝐷𝑖)‘𝑍) ≤ 𝑧, ((𝐷𝑖)‘𝑍), 𝑧))
215193, 214oveq12d 6811 . . . . . . . . . . . . . . 15 (𝑖 ∈ ℕ → (((𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍))‘𝑖)[,)if(((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖) ≤ 𝑧, ((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖), 𝑧)) = (((𝐶𝑖)‘𝑍)[,)if(((𝐷𝑖)‘𝑍) ≤ 𝑧, ((𝐷𝑖)‘𝑍), 𝑧)))
216215fveq2d 6336 . . . . . . . . . . . . . 14 (𝑖 ∈ ℕ → (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍))‘𝑖)[,)if(((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖) ≤ 𝑧, ((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖), 𝑧))) = (vol‘(((𝐶𝑖)‘𝑍)[,)if(((𝐷𝑖)‘𝑍) ≤ 𝑧, ((𝐷𝑖)‘𝑍), 𝑧))))
217216mpteq2ia 4874 . . . . . . . . . . . . 13 (𝑖 ∈ ℕ ↦ (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍))‘𝑖)[,)if(((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖) ≤ 𝑧, ((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖), 𝑧)))) = (𝑖 ∈ ℕ ↦ (vol‘(((𝐶𝑖)‘𝑍)[,)if(((𝐷𝑖)‘𝑍) ≤ 𝑧, ((𝐷𝑖)‘𝑍), 𝑧))))
218 fveq2 6332 . . . . . . . . . . . . . . . . 17 (𝑖 = → (𝐶𝑖) = (𝐶))
219218fveq1d 6334 . . . . . . . . . . . . . . . 16 (𝑖 = → ((𝐶𝑖)‘𝑍) = ((𝐶)‘𝑍))
220 fveq2 6332 . . . . . . . . . . . . . . . . . . 19 (𝑖 = → (𝐷𝑖) = (𝐷))
221220fveq1d 6334 . . . . . . . . . . . . . . . . . 18 (𝑖 = → ((𝐷𝑖)‘𝑍) = ((𝐷)‘𝑍))
222221breq1d 4796 . . . . . . . . . . . . . . . . 17 (𝑖 = → (((𝐷𝑖)‘𝑍) ≤ 𝑧 ↔ ((𝐷)‘𝑍) ≤ 𝑧))
223222, 221ifbieq1d 4248 . . . . . . . . . . . . . . . 16 (𝑖 = → if(((𝐷𝑖)‘𝑍) ≤ 𝑧, ((𝐷𝑖)‘𝑍), 𝑧) = if(((𝐷)‘𝑍) ≤ 𝑧, ((𝐷)‘𝑍), 𝑧))
224219, 223oveq12d 6811 . . . . . . . . . . . . . . 15 (𝑖 = → (((𝐶𝑖)‘𝑍)[,)if(((𝐷𝑖)‘𝑍) ≤ 𝑧, ((𝐷𝑖)‘𝑍), 𝑧)) = (((𝐶)‘𝑍)[,)if(((𝐷)‘𝑍) ≤ 𝑧, ((𝐷)‘𝑍), 𝑧)))
225224fveq2d 6336 . . . . . . . . . . . . . 14 (𝑖 = → (vol‘(((𝐶𝑖)‘𝑍)[,)if(((𝐷𝑖)‘𝑍) ≤ 𝑧, ((𝐷𝑖)‘𝑍), 𝑧))) = (vol‘(((𝐶)‘𝑍)[,)if(((𝐷)‘𝑍) ≤ 𝑧, ((𝐷)‘𝑍), 𝑧))))
226225cbvmptv 4884 . . . . . . . . . . . . 13 (𝑖 ∈ ℕ ↦ (vol‘(((𝐶𝑖)‘𝑍)[,)if(((𝐷𝑖)‘𝑍) ≤ 𝑧, ((𝐷𝑖)‘𝑍), 𝑧)))) = ( ∈ ℕ ↦ (vol‘(((𝐶)‘𝑍)[,)if(((𝐷)‘𝑍) ≤ 𝑧, ((𝐷)‘𝑍), 𝑧))))
227217, 226eqtri 2793 . . . . . . . . . . . 12 (𝑖 ∈ ℕ ↦ (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍))‘𝑖)[,)if(((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖) ≤ 𝑧, ((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖), 𝑧)))) = ( ∈ ℕ ↦ (vol‘(((𝐶)‘𝑍)[,)if(((𝐷)‘𝑍) ≤ 𝑧, ((𝐷)‘𝑍), 𝑧))))
228227a1i 11 . . . . . . . . . . 11 (𝑤 = 𝑧 → (𝑖 ∈ ℕ ↦ (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍))‘𝑖)[,)if(((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖) ≤ 𝑧, ((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖), 𝑧)))) = ( ∈ ℕ ↦ (vol‘(((𝐶)‘𝑍)[,)if(((𝐷)‘𝑍) ≤ 𝑧, ((𝐷)‘𝑍), 𝑧)))))
229 breq2 4790 . . . . . . . . . . . . . . . 16 (𝑤 = 𝑧 → (((𝐷)‘𝑍) ≤ 𝑤 ↔ ((𝐷)‘𝑍) ≤ 𝑧))
230 id 22 . . . . . . . . . . . . . . . 16 (𝑤 = 𝑧𝑤 = 𝑧)
231229, 230ifbieq2d 4250 . . . . . . . . . . . . . . 15 (𝑤 = 𝑧 → if(((𝐷)‘𝑍) ≤ 𝑤, ((𝐷)‘𝑍), 𝑤) = if(((𝐷)‘𝑍) ≤ 𝑧, ((𝐷)‘𝑍), 𝑧))
232231eqcomd 2777 . . . . . . . . . . . . . 14 (𝑤 = 𝑧 → if(((𝐷)‘𝑍) ≤ 𝑧, ((𝐷)‘𝑍), 𝑧) = if(((𝐷)‘𝑍) ≤ 𝑤, ((𝐷)‘𝑍), 𝑤))
233232oveq2d 6809 . . . . . . . . . . . . 13 (𝑤 = 𝑧 → (((𝐶)‘𝑍)[,)if(((𝐷)‘𝑍) ≤ 𝑧, ((𝐷)‘𝑍), 𝑧)) = (((𝐶)‘𝑍)[,)if(((𝐷)‘𝑍) ≤ 𝑤, ((𝐷)‘𝑍), 𝑤)))
234233fveq2d 6336 . . . . . . . . . . . 12 (𝑤 = 𝑧 → (vol‘(((𝐶)‘𝑍)[,)if(((𝐷)‘𝑍) ≤ 𝑧, ((𝐷)‘𝑍), 𝑧))) = (vol‘(((𝐶)‘𝑍)[,)if(((𝐷)‘𝑍) ≤ 𝑤, ((𝐷)‘𝑍), 𝑤))))
235234mpteq2dv 4879 . . . . . . . . . . 11 (𝑤 = 𝑧 → ( ∈ ℕ ↦ (vol‘(((𝐶)‘𝑍)[,)if(((𝐷)‘𝑍) ≤ 𝑧, ((𝐷)‘𝑍), 𝑧)))) = ( ∈ ℕ ↦ (vol‘(((𝐶)‘𝑍)[,)if(((𝐷)‘𝑍) ≤ 𝑤, ((𝐷)‘𝑍), 𝑤)))))
236228, 235eqtr2d 2806 . . . . . . . . . 10 (𝑤 = 𝑧 → ( ∈ ℕ ↦ (vol‘(((𝐶)‘𝑍)[,)if(((𝐷)‘𝑍) ≤ 𝑤, ((𝐷)‘𝑍), 𝑤)))) = (𝑖 ∈ ℕ ↦ (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍))‘𝑖)[,)if(((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖) ≤ 𝑧, ((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖), 𝑧)))))
237236fveq2d 6336 . . . . . . . . 9 (𝑤 = 𝑧 → (Σ^‘( ∈ ℕ ↦ (vol‘(((𝐶)‘𝑍)[,)if(((𝐷)‘𝑍) ≤ 𝑤, ((𝐷)‘𝑍), 𝑤))))) = (Σ^‘(𝑖 ∈ ℕ ↦ (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍))‘𝑖)[,)if(((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖) ≤ 𝑧, ((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖), 𝑧))))))
238212, 237breq12d 4799 . . . . . . . 8 (𝑤 = 𝑧 → ((𝑤 − (𝐴𝑍)) ≤ (Σ^‘( ∈ ℕ ↦ (vol‘(((𝐶)‘𝑍)[,)if(((𝐷)‘𝑍) ≤ 𝑤, ((𝐷)‘𝑍), 𝑤))))) ↔ (𝑧 − (𝐴𝑍)) ≤ (Σ^‘(𝑖 ∈ ℕ ↦ (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍))‘𝑖)[,)if(((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖) ≤ 𝑧, ((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖), 𝑧)))))))
239238cbvrabv 3349 . . . . . . 7 {𝑤 ∈ ((𝐴𝑍)[,](𝐵𝑍)) ∣ (𝑤 − (𝐴𝑍)) ≤ (Σ^‘( ∈ ℕ ↦ (vol‘(((𝐶)‘𝑍)[,)if(((𝐷)‘𝑍) ≤ 𝑤, ((𝐷)‘𝑍), 𝑤)))))} = {𝑧 ∈ ((𝐴𝑍)[,](𝐵𝑍)) ∣ (𝑧 − (𝐴𝑍)) ≤ (Σ^‘(𝑖 ∈ ℕ ↦ (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍))‘𝑖)[,)if(((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖) ≤ 𝑧, ((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖), 𝑧)))))}
240 eqid 2771 . . . . . . 7 sup({𝑤 ∈ ((𝐴𝑍)[,](𝐵𝑍)) ∣ (𝑤 − (𝐴𝑍)) ≤ (Σ^‘( ∈ ℕ ↦ (vol‘(((𝐶)‘𝑍)[,)if(((𝐷)‘𝑍) ≤ 𝑤, ((𝐷)‘𝑍), 𝑤)))))}, ℝ, < ) = sup({𝑤 ∈ ((𝐴𝑍)[,](𝐵𝑍)) ∣ (𝑤 − (𝐴𝑍)) ≤ (Σ^‘( ∈ ℕ ↦ (vol‘(((𝐶)‘𝑍)[,)if(((𝐷)‘𝑍) ≤ 𝑤, ((𝐷)‘𝑍), 𝑤)))))}, ℝ, < )
24181, 82, 83, 86, 89, 191, 211, 239, 240hoidmv1lelem3 41327 . . . . . 6 (((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) ∈ ℝ) → ((𝐵𝑍) − (𝐴𝑍)) ≤ (Σ^‘(𝑖 ∈ ℕ ↦ (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍))‘𝑖)[,)((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖))))))
242241, 209breqtrd 4812 . . . . 5 (((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) ∈ ℝ) → ((𝐵𝑍) − (𝐴𝑍)) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))))
24321, 80, 242syl2anc 573 . . . 4 (((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) ∧ ¬ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) = +∞) → ((𝐵𝑍) − (𝐴𝑍)) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))))
24420, 243pm2.61dan 813 . . 3 ((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) → ((𝐵𝑍) − (𝐴𝑍)) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))))
24525, 29, 32, 8, 1hoidmvn0val 41318 . . . . . . 7 (𝜑 → (𝐴(𝐿𝑋)𝐵) = ∏𝑘𝑋 (vol‘((𝐴𝑘)[,)(𝐵𝑘))))
24626prodeq1d 14858 . . . . . . 7 (𝜑 → ∏𝑘𝑋 (vol‘((𝐴𝑘)[,)(𝐵𝑘))) = ∏𝑘 ∈ {𝑍} (vol‘((𝐴𝑘)[,)(𝐵𝑘))))
247 volicore 41315 . . . . . . . . . 10 (((𝐴𝑍) ∈ ℝ ∧ (𝐵𝑍) ∈ ℝ) → (vol‘((𝐴𝑍)[,)(𝐵𝑍))) ∈ ℝ)
2489, 7, 247syl2anc 573 . . . . . . . . 9 (𝜑 → (vol‘((𝐴𝑍)[,)(𝐵𝑍))) ∈ ℝ)
249248recnd 10270 . . . . . . . 8 (𝜑 → (vol‘((𝐴𝑍)[,)(𝐵𝑍))) ∈ ℂ)
250119, 121oveq12d 6811 . . . . . . . . . 10 (𝑘 = 𝑍 → ((𝐴𝑘)[,)(𝐵𝑘)) = ((𝐴𝑍)[,)(𝐵𝑍)))
251250fveq2d 6336 . . . . . . . . 9 (𝑘 = 𝑍 → (vol‘((𝐴𝑘)[,)(𝐵𝑘))) = (vol‘((𝐴𝑍)[,)(𝐵𝑍))))
252251prodsn 14899 . . . . . . . 8 ((𝑍𝑉 ∧ (vol‘((𝐴𝑍)[,)(𝐵𝑍))) ∈ ℂ) → ∏𝑘 ∈ {𝑍} (vol‘((𝐴𝑘)[,)(𝐵𝑘))) = (vol‘((𝐴𝑍)[,)(𝐵𝑍))))
2532, 249, 252syl2anc 573 . . . . . . 7 (𝜑 → ∏𝑘 ∈ {𝑍} (vol‘((𝐴𝑘)[,)(𝐵𝑘))) = (vol‘((𝐴𝑍)[,)(𝐵𝑍))))
254245, 246, 2533eqtrd 2809 . . . . . 6 (𝜑 → (𝐴(𝐿𝑋)𝐵) = (vol‘((𝐴𝑍)[,)(𝐵𝑍))))
255254adantr 466 . . . . 5 ((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) → (𝐴(𝐿𝑋)𝐵) = (vol‘((𝐴𝑍)[,)(𝐵𝑍))))
256 volico 40717 . . . . . . 7 (((𝐴𝑍) ∈ ℝ ∧ (𝐵𝑍) ∈ ℝ) → (vol‘((𝐴𝑍)[,)(𝐵𝑍))) = if((𝐴𝑍) < (𝐵𝑍), ((𝐵𝑍) − (𝐴𝑍)), 0))
2579, 7, 256syl2anc 573 . . . . . 6 (𝜑 → (vol‘((𝐴𝑍)[,)(𝐵𝑍))) = if((𝐴𝑍) < (𝐵𝑍), ((𝐵𝑍) − (𝐴𝑍)), 0))
258257adantr 466 . . . . 5 ((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) → (vol‘((𝐴𝑍)[,)(𝐵𝑍))) = if((𝐴𝑍) < (𝐵𝑍), ((𝐵𝑍) − (𝐴𝑍)), 0))
259 iftrue 4231 . . . . . 6 ((𝐴𝑍) < (𝐵𝑍) → if((𝐴𝑍) < (𝐵𝑍), ((𝐵𝑍) − (𝐴𝑍)), 0) = ((𝐵𝑍) − (𝐴𝑍)))
260259adantl 467 . . . . 5 ((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) → if((𝐴𝑍) < (𝐵𝑍), ((𝐵𝑍) − (𝐴𝑍)), 0) = ((𝐵𝑍) − (𝐴𝑍)))
261255, 258, 2603eqtrd 2809 . . . 4 ((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) → (𝐴(𝐿𝑋)𝐵) = ((𝐵𝑍) − (𝐴𝑍)))
26259fveq2d 6336 . . . . 5 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗)))) = (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))))
263262adantr 466 . . . 4 ((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗)))) = (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))))
264261, 263breq12d 4799 . . 3 ((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) → ((𝐴(𝐿𝑋)𝐵) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗)))) ↔ ((𝐵𝑍) − (𝐴𝑍)) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))))))
265244, 264mpbird 247 . 2 ((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) → (𝐴(𝐿𝑋)𝐵) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗)))))
266245adantr 466 . . . 4 ((𝜑 ∧ ¬ (𝐴𝑍) < (𝐵𝑍)) → (𝐴(𝐿𝑋)𝐵) = ∏𝑘𝑋 (vol‘((𝐴𝑘)[,)(𝐵𝑘))))
267246adantr 466 . . . 4 ((𝜑 ∧ ¬ (𝐴𝑍) < (𝐵𝑍)) → ∏𝑘𝑋 (vol‘((𝐴𝑘)[,)(𝐵𝑘))) = ∏𝑘 ∈ {𝑍} (vol‘((𝐴𝑘)[,)(𝐵𝑘))))
268253adantr 466 . . . . 5 ((𝜑 ∧ ¬ (𝐴𝑍) < (𝐵𝑍)) → ∏𝑘 ∈ {𝑍} (vol‘((𝐴𝑘)[,)(𝐵𝑘))) = (vol‘((𝐴𝑍)[,)(𝐵𝑍))))
269257adantr 466 . . . . 5 ((𝜑 ∧ ¬ (𝐴𝑍) < (𝐵𝑍)) → (vol‘((𝐴𝑍)[,)(𝐵𝑍))) = if((𝐴𝑍) < (𝐵𝑍), ((𝐵𝑍) − (𝐴𝑍)), 0))
270 iffalse 4234 . . . . . 6 (¬ (𝐴𝑍) < (𝐵𝑍) → if((𝐴𝑍) < (𝐵𝑍), ((𝐵𝑍) − (𝐴𝑍)), 0) = 0)
271270adantl 467 . . . . 5 ((𝜑 ∧ ¬ (𝐴𝑍) < (𝐵𝑍)) → if((𝐴𝑍) < (𝐵𝑍), ((𝐵𝑍) − (𝐴𝑍)), 0) = 0)
272268, 269, 2713eqtrd 2809 . . . 4 ((𝜑 ∧ ¬ (𝐴𝑍) < (𝐵𝑍)) → ∏𝑘 ∈ {𝑍} (vol‘((𝐴𝑘)[,)(𝐵𝑘))) = 0)
273266, 267, 2723eqtrd 2809 . . 3 ((𝜑 ∧ ¬ (𝐴𝑍) < (𝐵𝑍)) → (𝐴(𝐿𝑋)𝐵) = 0)
27423a1i 11 . . . . 5 (𝜑 → ℕ ∈ V)
275274, 76sge0ge0 41118 . . . 4 (𝜑 → 0 ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗)))))
276275adantr 466 . . 3 ((𝜑 ∧ ¬ (𝐴𝑍) < (𝐵𝑍)) → 0 ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗)))))
277273, 276eqbrtrd 4808 . 2 ((𝜑 ∧ ¬ (𝐴𝑍) < (𝐵𝑍)) → (𝐴(𝐿𝑋)𝐵) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗)))))
278265, 277pm2.61dan 813 1 (𝜑 → (𝐴(𝐿𝑋)𝐵) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗)))))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∧ wa 382   ∧ w3a 1071   = wceq 1631   ∈ wcel 2145   ≠ wne 2943  ∀wral 3061  ∃wrex 3062  {crab 3065  Vcvv 3351   ⊆ wss 3723  ∅c0 4063  ifcif 4225  {csn 4316  ⟨cop 4322  ∪ ciun 4654   class class class wbr 4786   ↦ cmpt 4863  ⟶wf 6027  ‘cfv 6031  (class class class)co 6793   ↦ cmpt2 6795   ↑𝑚 cmap 8009  Xcixp 8062  Fincfn 8109  supcsup 8502  ℂcc 10136  ℝcr 10137  0cc0 10138  +∞cpnf 10273  ℝ*cxr 10275   < clt 10276   ≤ cle 10277   − cmin 10468  ℕcn 11222  [,)cico 12382  [,]cicc 12383  ∏cprod 14842  volcvol 23451  Σ^csumge0 41096 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-rep 4904  ax-sep 4915  ax-nul 4923  ax-pow 4974  ax-pr 5034  ax-un 7096  ax-inf2 8702  ax-cnex 10194  ax-resscn 10195  ax-1cn 10196  ax-icn 10197  ax-addcl 10198  ax-addrcl 10199  ax-mulcl 10200  ax-mulrcl 10201  ax-mulcom 10202  ax-addass 10203  ax-mulass 10204  ax-distr 10205  ax-i2m1 10206  ax-1ne0 10207  ax-1rid 10208  ax-rnegex 10209  ax-rrecex 10210  ax-cnre 10211  ax-pre-lttri 10212  ax-pre-lttrn 10213  ax-pre-ltadd 10214  ax-pre-mulgt0 10215  ax-pre-sup 10216 This theorem depends on definitions:  df-bi 197  df-an 383  df-or 835  df-3or 1072  df-3an 1073  df-tru 1634  df-fal 1637  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-nel 3047  df-ral 3066  df-rex 3067  df-reu 3068  df-rmo 3069  df-rab 3070  df-v 3353  df-sbc 3588  df-csb 3683  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-pss 3739  df-nul 4064  df-if 4226  df-pw 4299  df-sn 4317  df-pr 4319  df-tp 4321  df-op 4323  df-uni 4575  df-int 4612  df-iun 4656  df-br 4787  df-opab 4847  df-mpt 4864  df-tr 4887  df-id 5157  df-eprel 5162  df-po 5170  df-so 5171  df-fr 5208  df-se 5209  df-we 5210  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-res 5261  df-ima 5262  df-pred 5823  df-ord 5869  df-on 5870  df-lim 5871  df-suc 5872  df-iota 5994  df-fun 6033  df-fn 6034  df-f 6035  df-f1 6036  df-fo 6037  df-f1o 6038  df-fv 6039  df-isom 6040  df-riota 6754  df-ov 6796  df-oprab 6797  df-mpt2 6798  df-of 7044  df-om 7213  df-1st 7315  df-2nd 7316  df-wrecs 7559  df-recs 7621  df-rdg 7659  df-1o 7713  df-2o 7714  df-oadd 7717  df-er 7896  df-map 8011  df-pm 8012  df-ixp 8063  df-en 8110  df-dom 8111  df-sdom 8112  df-fin 8113  df-fi 8473  df-sup 8504  df-inf 8505  df-oi 8571  df-card 8965  df-cda 9192  df-pnf 10278  df-mnf 10279  df-xr 10280  df-ltxr 10281  df-le 10282  df-sub 10470  df-neg 10471  df-div 10887  df-nn 11223  df-2 11281  df-3 11282  df-n0 11495  df-z 11580  df-uz 11889  df-q 11992  df-rp 12036  df-xneg 12151  df-xadd 12152  df-xmul 12153  df-ioo 12384  df-ico 12386  df-icc 12387  df-fz 12534  df-fzo 12674  df-fl 12801  df-seq 13009  df-exp 13068  df-hash 13322  df-cj 14047  df-re 14048  df-im 14049  df-sqrt 14183  df-abs 14184  df-clim 14427  df-rlim 14428  df-sum 14625  df-prod 14843  df-rest 16291  df-topgen 16312  df-psmet 19953  df-xmet 19954  df-met 19955  df-bl 19956  df-mopn 19957  df-top 20919  df-topon 20936  df-bases 20971  df-cmp 21411  df-ovol 23452  df-vol 23453  df-sumge0 41097 This theorem is referenced by:  hoidmvle  41334
 Copyright terms: Public domain W3C validator