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

Theorem hoidmv1le 39484
 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 4153 . . . . . . . . . . . 12 (𝑍𝑉𝑍 ∈ {𝑍})
42, 3syl 17 . . . . . . . . . . 11 (𝜑𝑍 ∈ {𝑍})
5 hoidmv1le.x . . . . . . . . . . 11 𝑋 = {𝑍}
64, 5syl6eleqr 2699 . . . . . . . . . 10 (𝜑𝑍𝑋)
71, 6ffvelrnd 6268 . . . . . . . . 9 (𝜑 → (𝐵𝑍) ∈ ℝ)
8 hoidmv1le.a . . . . . . . . . 10 (𝜑𝐴:𝑋⟶ℝ)
98, 6ffvelrnd 6268 . . . . . . . . 9 (𝜑 → (𝐴𝑍) ∈ ℝ)
107, 9resubcld 10337 . . . . . . . 8 (𝜑 → ((𝐵𝑍) − (𝐴𝑍)) ∈ ℝ)
1110rexrd 9968 . . . . . . 7 (𝜑 → ((𝐵𝑍) − (𝐴𝑍)) ∈ ℝ*)
12 pnfxr 9971 . . . . . . . 8 +∞ ∈ ℝ*
1312a1i 11 . . . . . . 7 (𝜑 → +∞ ∈ ℝ*)
1410ltpnfd 11831 . . . . . . 7 (𝜑 → ((𝐵𝑍) − (𝐴𝑍)) < +∞)
1511, 13, 14xrltled 38427 . . . . . 6 (𝜑 → ((𝐵𝑍) − (𝐴𝑍)) ≤ +∞)
1615ad2antrr 758 . . . . 5 (((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) = +∞) → ((𝐵𝑍) − (𝐴𝑍)) ≤ +∞)
17 id 22 . . . . . . 7 ((Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) = +∞ → (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) = +∞)
1817eqcomd 2616 . . . . . 6 ((Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) = +∞ → +∞ = (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))))
1918adantl 481 . . . . 5 (((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) = +∞) → +∞ = (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))))
2016, 19breqtrd 4609 . . . 4 (((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) = +∞) → ((𝐵𝑍) − (𝐴𝑍)) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))))
21 simpl 472 . . . . 5 (((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) ∧ ¬ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) = +∞) → (𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)))
22 simpr 476 . . . . . 6 (((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) ∧ ¬ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) = +∞) → ¬ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) = +∞)
23 nnex 10903 . . . . . . . 8 ℕ ∈ V
2423a1i 11 . . . . . . 7 (((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) ∧ ¬ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) = +∞) → ℕ ∈ V)
25 hoidmv1le.l . . . . . . . . . . . 12 𝐿 = (𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑𝑚 𝑥), 𝑏 ∈ (ℝ ↑𝑚 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘𝑥 (vol‘((𝑎𝑘)[,)(𝑏𝑘))))))
265a1i 11 . . . . . . . . . . . . . 14 (𝜑𝑋 = {𝑍})
27 snfi 7923 . . . . . . . . . . . . . . 15 {𝑍} ∈ Fin
2827a1i 11 . . . . . . . . . . . . . 14 (𝜑 → {𝑍} ∈ Fin)
2926, 28eqeltrd 2688 . . . . . . . . . . . . 13 (𝜑𝑋 ∈ Fin)
3029adantr 480 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ) → 𝑋 ∈ Fin)
31 ne0i 3880 . . . . . . . . . . . . . 14 (𝑍𝑋𝑋 ≠ ∅)
326, 31syl 17 . . . . . . . . . . . . 13 (𝜑𝑋 ≠ ∅)
3332adantr 480 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ) → 𝑋 ≠ ∅)
34 hoidmv1le.c . . . . . . . . . . . . . 14 (𝜑𝐶:ℕ⟶(ℝ ↑𝑚 𝑋))
3534ffvelrnda 6267 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ ℕ) → (𝐶𝑗) ∈ (ℝ ↑𝑚 𝑋))
36 elmapi 7765 . . . . . . . . . . . . 13 ((𝐶𝑗) ∈ (ℝ ↑𝑚 𝑋) → (𝐶𝑗):𝑋⟶ℝ)
3735, 36syl 17 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ) → (𝐶𝑗):𝑋⟶ℝ)
38 hoidmv1le.d . . . . . . . . . . . . . 14 (𝜑𝐷:ℕ⟶(ℝ ↑𝑚 𝑋))
3938ffvelrnda 6267 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ ℕ) → (𝐷𝑗) ∈ (ℝ ↑𝑚 𝑋))
40 elmapi 7765 . . . . . . . . . . . . 13 ((𝐷𝑗) ∈ (ℝ ↑𝑚 𝑋) → (𝐷𝑗):𝑋⟶ℝ)
4139, 40syl 17 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ) → (𝐷𝑗):𝑋⟶ℝ)
4225, 30, 33, 37, 41hoidmvn0val 39474 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗)) = ∏𝑘𝑋 (vol‘(((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))))
435prodeq1i 14487 . . . . . . . . . . . 12 𝑘𝑋 (vol‘(((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) = ∏𝑘 ∈ {𝑍} (vol‘(((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
4443a1i 11 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ℕ) → ∏𝑘𝑋 (vol‘(((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) = ∏𝑘 ∈ {𝑍} (vol‘(((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))))
452adantr 480 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ) → 𝑍𝑉)
466adantr 480 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ ℕ) → 𝑍𝑋)
4737, 46ffvelrnd 6268 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗)‘𝑍) ∈ ℝ)
4841, 46ffvelrnd 6268 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ ℕ) → ((𝐷𝑗)‘𝑍) ∈ ℝ)
49 volicore 39471 . . . . . . . . . . . . . 14 ((((𝐶𝑗)‘𝑍) ∈ ℝ ∧ ((𝐷𝑗)‘𝑍) ∈ ℝ) → (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))) ∈ ℝ)
5047, 48, 49syl2anc 691 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ ℕ) → (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))) ∈ ℝ)
5150recnd 9947 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ) → (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))) ∈ ℂ)
52 fveq2 6103 . . . . . . . . . . . . . . 15 (𝑘 = 𝑍 → ((𝐶𝑗)‘𝑘) = ((𝐶𝑗)‘𝑍))
53 fveq2 6103 . . . . . . . . . . . . . . 15 (𝑘 = 𝑍 → ((𝐷𝑗)‘𝑘) = ((𝐷𝑗)‘𝑍))
5452, 53oveq12d 6567 . . . . . . . . . . . . . 14 (𝑘 = 𝑍 → (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) = (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))
5554fveq2d 6107 . . . . . . . . . . . . 13 (𝑘 = 𝑍 → (vol‘(((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) = (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))
5655prodsn 14531 . . . . . . . . . . . 12 ((𝑍𝑉 ∧ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))) ∈ ℂ) → ∏𝑘 ∈ {𝑍} (vol‘(((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) = (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))
5745, 51, 56syl2anc 691 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ℕ) → ∏𝑘 ∈ {𝑍} (vol‘(((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) = (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))
5842, 44, 573eqtrd 2648 . . . . . . . . . 10 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗)) = (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))
5958mpteq2dva 4672 . . . . . . . . 9 (𝜑 → (𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗))) = (𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))))
60 fveq2 6103 . . . . . . . . . . . . . . . . . . . 20 (𝑘 = 𝑙 → (𝑎𝑘) = (𝑎𝑙))
61 fveq2 6103 . . . . . . . . . . . . . . . . . . . 20 (𝑘 = 𝑙 → (𝑏𝑘) = (𝑏𝑙))
6260, 61oveq12d 6567 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 𝑙 → ((𝑎𝑘)[,)(𝑏𝑘)) = ((𝑎𝑙)[,)(𝑏𝑙)))
6362fveq2d 6107 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑙 → (vol‘((𝑎𝑘)[,)(𝑏𝑘))) = (vol‘((𝑎𝑙)[,)(𝑏𝑙))))
6463cbvprodv 14485 . . . . . . . . . . . . . . . . 17 𝑘𝑥 (vol‘((𝑎𝑘)[,)(𝑏𝑘))) = ∏𝑙𝑥 (vol‘((𝑎𝑙)[,)(𝑏𝑙)))
65 ifeq2 4041 . . . . . . . . . . . . . . . . 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 6618 . . . . . . . . . . . . . 14 (𝑎 ∈ (ℝ ↑𝑚 𝑥), 𝑏 ∈ (ℝ ↑𝑚 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘𝑥 (vol‘((𝑎𝑘)[,)(𝑏𝑘))))) = (𝑎 ∈ (ℝ ↑𝑚 𝑥), 𝑏 ∈ (ℝ ↑𝑚 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑙𝑥 (vol‘((𝑎𝑙)[,)(𝑏𝑙)))))
6968mpteq2i 4669 . . . . . . . . . . . . 13 (𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑𝑚 𝑥), 𝑏 ∈ (ℝ ↑𝑚 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘𝑥 (vol‘((𝑎𝑘)[,)(𝑏𝑘)))))) = (𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑𝑚 𝑥), 𝑏 ∈ (ℝ ↑𝑚 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑙𝑥 (vol‘((𝑎𝑙)[,)(𝑏𝑙))))))
7025, 69eqtri 2632 . . . . . . . . . . . 12 𝐿 = (𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑𝑚 𝑥), 𝑏 ∈ (ℝ ↑𝑚 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑙𝑥 (vol‘((𝑎𝑙)[,)(𝑏𝑙))))))
7170, 30, 37, 41hoidmvcl 39472 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗)) ∈ (0[,)+∞))
72 eqid 2610 . . . . . . . . . . 11 (𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗))) = (𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗)))
7371, 72fmptd 6292 . . . . . . . . . 10 (𝜑 → (𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗))):ℕ⟶(0[,)+∞))
74 icossicc 12131 . . . . . . . . . . 11 (0[,)+∞) ⊆ (0[,]+∞)
7574a1i 11 . . . . . . . . . 10 (𝜑 → (0[,)+∞) ⊆ (0[,]+∞))
7673, 75fssd 5970 . . . . . . . . 9 (𝜑 → (𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗))):ℕ⟶(0[,]+∞))
7759, 76feq1dd 38341 . . . . . . . 8 (𝜑 → (𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))):ℕ⟶(0[,]+∞))
7877ad2antrr 758 . . . . . . 7 (((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) ∧ ¬ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) = +∞) → (𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))):ℕ⟶(0[,]+∞))
7924, 78sge0repnf 39279 . . . . . 6 (((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) ∧ ¬ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) = +∞) → ((Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) ∈ ℝ ↔ ¬ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) = +∞))
8022, 79mpbird 246 . . . . 5 (((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) ∧ ¬ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) = +∞) → (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) ∈ ℝ)
819ad2antrr 758 . . . . . . 7 (((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) ∈ ℝ) → (𝐴𝑍) ∈ ℝ)
827ad2antrr 758 . . . . . . 7 (((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) ∈ ℝ) → (𝐵𝑍) ∈ ℝ)
83 simplr 788 . . . . . . 7 (((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) ∈ ℝ) → (𝐴𝑍) < (𝐵𝑍))
84 eqid 2610 . . . . . . . . 9 (𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍)) = (𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍))
8547, 84fmptd 6292 . . . . . . . 8 (𝜑 → (𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍)):ℕ⟶ℝ)
8685ad2antrr 758 . . . . . . 7 (((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) ∈ ℝ) → (𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍)):ℕ⟶ℝ)
87 eqid 2610 . . . . . . . . 9 (𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍)) = (𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))
8848, 87fmptd 6292 . . . . . . . 8 (𝜑 → (𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍)):ℕ⟶ℝ)
8988ad2antrr 758 . . . . . . 7 (((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) ∈ ℝ) → (𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍)):ℕ⟶ℝ)
90 hoidmv1le.s . . . . . . . . . . . . . . . . 17 (𝜑X𝑘𝑋 ((𝐴𝑘)[,)(𝐵𝑘)) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
915eleq2i 2680 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑘𝑋𝑘 ∈ {𝑍})
9291biimpi 205 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑘𝑋𝑘 ∈ {𝑍})
93 elsni 4142 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑘 ∈ {𝑍} → 𝑘 = 𝑍)
9492, 93syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑘𝑋𝑘 = 𝑍)
9594, 54syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘𝑋 → (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) = (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))
9695rgen 2906 . . . . . . . . . . . . . . . . . . . . 21 𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) = (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))
97 ixpeq2 7808 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) = (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) → X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) = X𝑘𝑋 (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))
9896, 97ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) = X𝑘𝑋 (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))
9998a1i 11 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ ℕ → X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) = X𝑘𝑋 (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))
10099iuneq2i 4475 . . . . . . . . . . . . . . . . . 18 𝑗 ∈ ℕ X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) = 𝑗 ∈ ℕ X𝑘𝑋 (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))
101100a1i 11 . . . . . . . . . . . . . . . . 17 (𝜑 𝑗 ∈ ℕ X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) = 𝑗 ∈ ℕ X𝑘𝑋 (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))
10290, 101sseqtrd 3604 . . . . . . . . . . . . . . . 16 (𝜑X𝑘𝑋 ((𝐴𝑘)[,)(𝐵𝑘)) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))
103102adantr 480 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ ((𝐴𝑍)[,)(𝐵𝑍))) → X𝑘𝑋 ((𝐴𝑘)[,)(𝐵𝑘)) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))
104 id 22 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ((𝐴𝑍)[,)(𝐵𝑍)) → 𝑥 ∈ ((𝐴𝑍)[,)(𝐵𝑍)))
105 eqidd 2611 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ((𝐴𝑍)[,)(𝐵𝑍)) → {⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑥⟩})
106 opeq2 4341 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 = 𝑥 → ⟨𝑍, 𝑦⟩ = ⟨𝑍, 𝑥⟩)
107106sneqd 4137 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 = 𝑥 → {⟨𝑍, 𝑦⟩} = {⟨𝑍, 𝑥⟩})
108107eqeq2d 2620 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = 𝑥 → ({⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩} ↔ {⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑥⟩}))
109108rspcev 3282 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ∈ ((𝐴𝑍)[,)(𝐵𝑍)) ∧ {⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑥⟩}) → ∃𝑦 ∈ ((𝐴𝑍)[,)(𝐵𝑍)){⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩})
110104, 105, 109syl2anc 691 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ((𝐴𝑍)[,)(𝐵𝑍)) → ∃𝑦 ∈ ((𝐴𝑍)[,)(𝐵𝑍)){⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩})
111110adantl 481 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ ((𝐴𝑍)[,)(𝐵𝑍))) → ∃𝑦 ∈ ((𝐴𝑍)[,)(𝐵𝑍)){⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩})
112 elixpsn 7833 . . . . . . . . . . . . . . . . . . 19 (𝑍𝑉 → ({⟨𝑍, 𝑥⟩} ∈ X𝑘 ∈ {𝑍} ((𝐴𝑍)[,)(𝐵𝑍)) ↔ ∃𝑦 ∈ ((𝐴𝑍)[,)(𝐵𝑍)){⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩}))
1132, 112syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑 → ({⟨𝑍, 𝑥⟩} ∈ X𝑘 ∈ {𝑍} ((𝐴𝑍)[,)(𝐵𝑍)) ↔ ∃𝑦 ∈ ((𝐴𝑍)[,)(𝐵𝑍)){⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩}))
114113adantr 480 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ ((𝐴𝑍)[,)(𝐵𝑍))) → ({⟨𝑍, 𝑥⟩} ∈ X𝑘 ∈ {𝑍} ((𝐴𝑍)[,)(𝐵𝑍)) ↔ ∃𝑦 ∈ ((𝐴𝑍)[,)(𝐵𝑍)){⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩}))
115111, 114mpbird 246 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ ((𝐴𝑍)[,)(𝐵𝑍))) → {⟨𝑍, 𝑥⟩} ∈ X𝑘 ∈ {𝑍} ((𝐴𝑍)[,)(𝐵𝑍)))
1165eqcomi 2619 . . . . . . . . . . . . . . . . . . . 20 {𝑍} = 𝑋
117 ixpeq1 7805 . . . . . . . . . . . . . . . . . . . 20 ({𝑍} = 𝑋X𝑘 ∈ {𝑍} ((𝐴𝑍)[,)(𝐵𝑍)) = X𝑘𝑋 ((𝐴𝑍)[,)(𝐵𝑍)))
118116, 117ax-mp 5 . . . . . . . . . . . . . . . . . . 19 X𝑘 ∈ {𝑍} ((𝐴𝑍)[,)(𝐵𝑍)) = X𝑘𝑋 ((𝐴𝑍)[,)(𝐵𝑍))
119 fveq2 6103 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑘 = 𝑍 → (𝐴𝑘) = (𝐴𝑍))
12094, 119syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑘𝑋 → (𝐴𝑘) = (𝐴𝑍))
121 fveq2 6103 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑘 = 𝑍 → (𝐵𝑘) = (𝐵𝑍))
12294, 121syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑘𝑋 → (𝐵𝑘) = (𝐵𝑍))
123120, 122oveq12d 6567 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘𝑋 → ((𝐴𝑘)[,)(𝐵𝑘)) = ((𝐴𝑍)[,)(𝐵𝑍)))
124123eqcomd 2616 . . . . . . . . . . . . . . . . . . . . 21 (𝑘𝑋 → ((𝐴𝑍)[,)(𝐵𝑍)) = ((𝐴𝑘)[,)(𝐵𝑘)))
125124rgen 2906 . . . . . . . . . . . . . . . . . . . 20 𝑘𝑋 ((𝐴𝑍)[,)(𝐵𝑍)) = ((𝐴𝑘)[,)(𝐵𝑘))
126 ixpeq2 7808 . . . . . . . . . . . . . . . . . . . 20 (∀𝑘𝑋 ((𝐴𝑍)[,)(𝐵𝑍)) = ((𝐴𝑘)[,)(𝐵𝑘)) → X𝑘𝑋 ((𝐴𝑍)[,)(𝐵𝑍)) = X𝑘𝑋 ((𝐴𝑘)[,)(𝐵𝑘)))
127125, 126ax-mp 5 . . . . . . . . . . . . . . . . . . 19 X𝑘𝑋 ((𝐴𝑍)[,)(𝐵𝑍)) = X𝑘𝑋 ((𝐴𝑘)[,)(𝐵𝑘))
128118, 127eqtri 2632 . . . . . . . . . . . . . . . . . 18 X𝑘 ∈ {𝑍} ((𝐴𝑍)[,)(𝐵𝑍)) = X𝑘𝑋 ((𝐴𝑘)[,)(𝐵𝑘))
129128a1i 11 . . . . . . . . . . . . . . . . 17 (𝜑X𝑘 ∈ {𝑍} ((𝐴𝑍)[,)(𝐵𝑍)) = X𝑘𝑋 ((𝐴𝑘)[,)(𝐵𝑘)))
130129adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ ((𝐴𝑍)[,)(𝐵𝑍))) → X𝑘 ∈ {𝑍} ((𝐴𝑍)[,)(𝐵𝑍)) = X𝑘𝑋 ((𝐴𝑘)[,)(𝐵𝑘)))
131115, 130eleqtrd 2690 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ ((𝐴𝑍)[,)(𝐵𝑍))) → {⟨𝑍, 𝑥⟩} ∈ X𝑘𝑋 ((𝐴𝑘)[,)(𝐵𝑘)))
132103, 131sseldd 3569 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ ((𝐴𝑍)[,)(𝐵𝑍))) → {⟨𝑍, 𝑥⟩} ∈ 𝑗 ∈ ℕ X𝑘𝑋 (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))
133 eliun 4460 . . . . . . . . . . . . . 14 ({⟨𝑍, 𝑥⟩} ∈ 𝑗 ∈ ℕ X𝑘𝑋 (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) ↔ ∃𝑗 ∈ ℕ {⟨𝑍, 𝑥⟩} ∈ X𝑘𝑋 (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))
134132, 133sylib 207 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ ((𝐴𝑍)[,)(𝐵𝑍))) → ∃𝑗 ∈ ℕ {⟨𝑍, 𝑥⟩} ∈ X𝑘𝑋 (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))
135 ixpeq1 7805 . . . . . . . . . . . . . . . . . . . . . 22 (𝑋 = {𝑍} → X𝑘𝑋 (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) = X𝑘 ∈ {𝑍} (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))
1365, 135ax-mp 5 . . . . . . . . . . . . . . . . . . . . 21 X𝑘𝑋 (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) = X𝑘 ∈ {𝑍} (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))
137136eleq2i 2680 . . . . . . . . . . . . . . . . . . . 20 ({⟨𝑍, 𝑥⟩} ∈ X𝑘𝑋 (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) ↔ {⟨𝑍, 𝑥⟩} ∈ X𝑘 ∈ {𝑍} (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))
138137biimpi 205 . . . . . . . . . . . . . . . . . . 19 ({⟨𝑍, 𝑥⟩} ∈ X𝑘𝑋 (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) → {⟨𝑍, 𝑥⟩} ∈ X𝑘 ∈ {𝑍} (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))
139138adantl 481 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ {⟨𝑍, 𝑥⟩} ∈ X𝑘𝑋 (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))) → {⟨𝑍, 𝑥⟩} ∈ X𝑘 ∈ {𝑍} (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))
140 elixpsn 7833 . . . . . . . . . . . . . . . . . . . 20 (𝑍𝑉 → ({⟨𝑍, 𝑥⟩} ∈ X𝑘 ∈ {𝑍} (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) ↔ ∃𝑦 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)){⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩}))
1412, 140syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ({⟨𝑍, 𝑥⟩} ∈ X𝑘 ∈ {𝑍} (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) ↔ ∃𝑦 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)){⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩}))
142141adantr 480 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ {⟨𝑍, 𝑥⟩} ∈ X𝑘𝑋 (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))) → ({⟨𝑍, 𝑥⟩} ∈ X𝑘 ∈ {𝑍} (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) ↔ ∃𝑦 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)){⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩}))
143139, 142mpbid 221 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ {⟨𝑍, 𝑥⟩} ∈ X𝑘𝑋 (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))) → ∃𝑦 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)){⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩})
144 opex 4859 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑍, 𝑥⟩ ∈ V
145144sneqr 4311 . . . . . . . . . . . . . . . . . . . . . . . . 25 ({⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩} → ⟨𝑍, 𝑥⟩ = ⟨𝑍, 𝑦⟩)
146145adantl 481 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ {⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩}) → ⟨𝑍, 𝑥⟩ = ⟨𝑍, 𝑦⟩)
147 vex 3176 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝑥 ∈ V
148147a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑𝑥 ∈ V)
149 opthg 4872 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑍𝑉𝑥 ∈ V) → (⟨𝑍, 𝑥⟩ = ⟨𝑍, 𝑦⟩ ↔ (𝑍 = 𝑍𝑥 = 𝑦)))
1502, 148, 149syl2anc 691 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (⟨𝑍, 𝑥⟩ = ⟨𝑍, 𝑦⟩ ↔ (𝑍 = 𝑍𝑥 = 𝑦)))
151150adantr 480 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ {⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩}) → (⟨𝑍, 𝑥⟩ = ⟨𝑍, 𝑦⟩ ↔ (𝑍 = 𝑍𝑥 = 𝑦)))
152146, 151mpbid 221 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ {⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩}) → (𝑍 = 𝑍𝑥 = 𝑦))
153152simprd 478 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ {⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩}) → 𝑥 = 𝑦)
1541533adant2 1073 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑦 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) ∧ {⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩}) → 𝑥 = 𝑦)
155 simp2 1055 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑦 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) ∧ {⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩}) → 𝑦 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))
156154, 155eqeltrd 2688 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑦 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) ∧ {⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩}) → 𝑥 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))
1571563exp 1256 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑦 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) → ({⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩} → 𝑥 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))))
158157adantr 480 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ {⟨𝑍, 𝑥⟩} ∈ X𝑘𝑋 (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))) → (𝑦 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) → ({⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩} → 𝑥 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))))
159158rexlimdv 3012 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ {⟨𝑍, 𝑥⟩} ∈ X𝑘𝑋 (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))) → (∃𝑦 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)){⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩} → 𝑥 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))
160143, 159mpd 15 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ {⟨𝑍, 𝑥⟩} ∈ X𝑘𝑋 (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))) → 𝑥 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))
161160ex 449 . . . . . . . . . . . . . . 15 (𝜑 → ({⟨𝑍, 𝑥⟩} ∈ X𝑘𝑋 (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) → 𝑥 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))
162161ad2antrr 758 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ ((𝐴𝑍)[,)(𝐵𝑍))) ∧ 𝑗 ∈ ℕ) → ({⟨𝑍, 𝑥⟩} ∈ X𝑘𝑋 (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) → 𝑥 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))
163162reximdva 3000 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ ((𝐴𝑍)[,)(𝐵𝑍))) → (∃𝑗 ∈ ℕ {⟨𝑍, 𝑥⟩} ∈ X𝑘𝑋 (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) → ∃𝑗 ∈ ℕ 𝑥 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))
164134, 163mpd 15 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ ((𝐴𝑍)[,)(𝐵𝑍))) → ∃𝑗 ∈ ℕ 𝑥 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))
165 eliun 4460 . . . . . . . . . . . 12 (𝑥 𝑗 ∈ ℕ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) ↔ ∃𝑗 ∈ ℕ 𝑥 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))
166164, 165sylibr 223 . . . . . . . . . . 11 ((𝜑𝑥 ∈ ((𝐴𝑍)[,)(𝐵𝑍))) → 𝑥 𝑗 ∈ ℕ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))
167166ralrimiva 2949 . . . . . . . . . 10 (𝜑 → ∀𝑥 ∈ ((𝐴𝑍)[,)(𝐵𝑍))𝑥 𝑗 ∈ ℕ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))
168 dfss3 3558 . . . . . . . . . 10 (((𝐴𝑍)[,)(𝐵𝑍)) ⊆ 𝑗 ∈ ℕ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) ↔ ∀𝑥 ∈ ((𝐴𝑍)[,)(𝐵𝑍))𝑥 𝑗 ∈ ℕ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))
169167, 168sylibr 223 . . . . . . . . 9 (𝜑 → ((𝐴𝑍)[,)(𝐵𝑍)) ⊆ 𝑗 ∈ ℕ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))
170 eqidd 2611 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ ℕ) → (𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍)) = (𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍)))
171 fveq2 6103 . . . . . . . . . . . . . . 15 (𝑗 = 𝑖 → (𝐶𝑗) = (𝐶𝑖))
172171fveq1d 6105 . . . . . . . . . . . . . 14 (𝑗 = 𝑖 → ((𝐶𝑗)‘𝑍) = ((𝐶𝑖)‘𝑍))
173172adantl 481 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ ℕ) ∧ 𝑗 = 𝑖) → ((𝐶𝑗)‘𝑍) = ((𝐶𝑖)‘𝑍))
174 simpr 476 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ ℕ) → 𝑖 ∈ ℕ)
175 fvex 6113 . . . . . . . . . . . . . 14 ((𝐶𝑖)‘𝑍) ∈ V
176175a1i 11 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ ℕ) → ((𝐶𝑖)‘𝑍) ∈ V)
177170, 173, 174, 176fvmptd 6197 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ ℕ) → ((𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍))‘𝑖) = ((𝐶𝑖)‘𝑍))
178 eqidd 2611 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ ℕ) → (𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍)) = (𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍)))
179 fveq2 6103 . . . . . . . . . . . . . . 15 (𝑗 = 𝑖 → (𝐷𝑗) = (𝐷𝑖))
180179fveq1d 6105 . . . . . . . . . . . . . 14 (𝑗 = 𝑖 → ((𝐷𝑗)‘𝑍) = ((𝐷𝑖)‘𝑍))
181180adantl 481 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ ℕ) ∧ 𝑗 = 𝑖) → ((𝐷𝑗)‘𝑍) = ((𝐷𝑖)‘𝑍))
182 fvex 6113 . . . . . . . . . . . . . 14 ((𝐷𝑖)‘𝑍) ∈ V
183182a1i 11 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ ℕ) → ((𝐷𝑖)‘𝑍) ∈ V)
184178, 181, 174, 183fvmptd 6197 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ ℕ) → ((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖) = ((𝐷𝑖)‘𝑍))
185177, 184oveq12d 6567 . . . . . . . . . . 11 ((𝜑𝑖 ∈ ℕ) → (((𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍))‘𝑖)[,)((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖)) = (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)))
186185iuneq2dv 4478 . . . . . . . . . 10 (𝜑 𝑖 ∈ ℕ (((𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍))‘𝑖)[,)((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖)) = 𝑖 ∈ ℕ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)))
187172, 180oveq12d 6567 . . . . . . . . . . . . 13 (𝑗 = 𝑖 → (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) = (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)))
188187cbviunv 4495 . . . . . . . . . . . 12 𝑗 ∈ ℕ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) = 𝑖 ∈ ℕ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍))
189188eqcomi 2619 . . . . . . . . . . 11 𝑖 ∈ ℕ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)) = 𝑗 ∈ ℕ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))
190189a1i 11 . . . . . . . . . 10 (𝜑 𝑖 ∈ ℕ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)) = 𝑗 ∈ ℕ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))
191186, 190eqtr2d 2645 . . . . . . . . 9 (𝜑 𝑗 ∈ ℕ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) = 𝑖 ∈ ℕ (((𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍))‘𝑖)[,)((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖)))
192169, 191sseqtrd 3604 . . . . . . . 8 (𝜑 → ((𝐴𝑍)[,)(𝐵𝑍)) ⊆ 𝑖 ∈ ℕ (((𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍))‘𝑖)[,)((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖)))
193192ad2antrr 758 . . . . . . 7 (((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) ∈ ℝ) → ((𝐴𝑍)[,)(𝐵𝑍)) ⊆ 𝑖 ∈ ℕ (((𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍))‘𝑖)[,)((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖)))
194172, 84, 175fvmpt 6191 . . . . . . . . . . . . . 14 (𝑖 ∈ ℕ → ((𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍))‘𝑖) = ((𝐶𝑖)‘𝑍))
195180, 87, 182fvmpt 6191 . . . . . . . . . . . . . 14 (𝑖 ∈ ℕ → ((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖) = ((𝐷𝑖)‘𝑍))
196194, 195oveq12d 6567 . . . . . . . . . . . . 13 (𝑖 ∈ ℕ → (((𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍))‘𝑖)[,)((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖)) = (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)))
197196fveq2d 6107 . . . . . . . . . . . 12 (𝑖 ∈ ℕ → (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍))‘𝑖)[,)((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖))) = (vol‘(((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍))))
198197mpteq2ia 4668 . . . . . . . . . . 11 (𝑖 ∈ ℕ ↦ (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍))‘𝑖)[,)((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖)))) = (𝑖 ∈ ℕ ↦ (vol‘(((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍))))
199 eqcom 2617 . . . . . . . . . . . . . . . 16 (𝑗 = 𝑖𝑖 = 𝑗)
200199imbi1i 338 . . . . . . . . . . . . . . 15 ((𝑗 = 𝑖 → (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) = (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍))) ↔ (𝑖 = 𝑗 → (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) = (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍))))
201 eqcom 2617 . . . . . . . . . . . . . . . 16 ((((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) = (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)) ↔ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)) = (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))
202201imbi2i 325 . . . . . . . . . . . . . . 15 ((𝑖 = 𝑗 → (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) = (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍))) ↔ (𝑖 = 𝑗 → (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)) = (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))
203200, 202bitri 263 . . . . . . . . . . . . . 14 ((𝑗 = 𝑖 → (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) = (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍))) ↔ (𝑖 = 𝑗 → (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)) = (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))
204187, 203mpbi 219 . . . . . . . . . . . . 13 (𝑖 = 𝑗 → (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)) = (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))
205204fveq2d 6107 . . . . . . . . . . . 12 (𝑖 = 𝑗 → (vol‘(((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍))) = (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))
206205cbvmptv 4678 . . . . . . . . . . 11 (𝑖 ∈ ℕ ↦ (vol‘(((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)))) = (𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))
207198, 206eqtri 2632 . . . . . . . . . 10 (𝑖 ∈ ℕ ↦ (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍))‘𝑖)[,)((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖)))) = (𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))
208207fveq2i 6106 . . . . . . . . 9 ^‘(𝑖 ∈ ℕ ↦ (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍))‘𝑖)[,)((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖))))) = (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))))
209208a1i 11 . . . . . . . 8 (((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) ∈ ℝ) → (Σ^‘(𝑖 ∈ ℕ ↦ (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍))‘𝑖)[,)((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖))))) = (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))))
210 simpr 476 . . . . . . . 8 (((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) ∈ ℝ) → (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) ∈ ℝ)
211209, 210eqeltrd 2688 . . . . . . 7 (((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) ∈ ℝ) → (Σ^‘(𝑖 ∈ ℕ ↦ (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍))‘𝑖)[,)((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖))))) ∈ ℝ)
212 oveq1 6556 . . . . . . . . 9 (𝑤 = 𝑧 → (𝑤 − (𝐴𝑍)) = (𝑧 − (𝐴𝑍)))
213195breq1d 4593 . . . . . . . . . . . . . . . . 17 (𝑖 ∈ ℕ → (((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖) ≤ 𝑧 ↔ ((𝐷𝑖)‘𝑍) ≤ 𝑧))
214213, 195ifbieq1d 4059 . . . . . . . . . . . . . . . 16 (𝑖 ∈ ℕ → if(((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖) ≤ 𝑧, ((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖), 𝑧) = if(((𝐷𝑖)‘𝑍) ≤ 𝑧, ((𝐷𝑖)‘𝑍), 𝑧))
215194, 214oveq12d 6567 . . . . . . . . . . . . . . 15 (𝑖 ∈ ℕ → (((𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍))‘𝑖)[,)if(((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖) ≤ 𝑧, ((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖), 𝑧)) = (((𝐶𝑖)‘𝑍)[,)if(((𝐷𝑖)‘𝑍) ≤ 𝑧, ((𝐷𝑖)‘𝑍), 𝑧)))
216215fveq2d 6107 . . . . . . . . . . . . . 14 (𝑖 ∈ ℕ → (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍))‘𝑖)[,)if(((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖) ≤ 𝑧, ((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖), 𝑧))) = (vol‘(((𝐶𝑖)‘𝑍)[,)if(((𝐷𝑖)‘𝑍) ≤ 𝑧, ((𝐷𝑖)‘𝑍), 𝑧))))
217216mpteq2ia 4668 . . . . . . . . . . . . 13 (𝑖 ∈ ℕ ↦ (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍))‘𝑖)[,)if(((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖) ≤ 𝑧, ((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖), 𝑧)))) = (𝑖 ∈ ℕ ↦ (vol‘(((𝐶𝑖)‘𝑍)[,)if(((𝐷𝑖)‘𝑍) ≤ 𝑧, ((𝐷𝑖)‘𝑍), 𝑧))))
218 fveq2 6103 . . . . . . . . . . . . . . . . 17 (𝑖 = → (𝐶𝑖) = (𝐶))
219218fveq1d 6105 . . . . . . . . . . . . . . . 16 (𝑖 = → ((𝐶𝑖)‘𝑍) = ((𝐶)‘𝑍))
220 fveq2 6103 . . . . . . . . . . . . . . . . . . 19 (𝑖 = → (𝐷𝑖) = (𝐷))
221220fveq1d 6105 . . . . . . . . . . . . . . . . . 18 (𝑖 = → ((𝐷𝑖)‘𝑍) = ((𝐷)‘𝑍))
222221breq1d 4593 . . . . . . . . . . . . . . . . 17 (𝑖 = → (((𝐷𝑖)‘𝑍) ≤ 𝑧 ↔ ((𝐷)‘𝑍) ≤ 𝑧))
223222, 221ifbieq1d 4059 . . . . . . . . . . . . . . . 16 (𝑖 = → if(((𝐷𝑖)‘𝑍) ≤ 𝑧, ((𝐷𝑖)‘𝑍), 𝑧) = if(((𝐷)‘𝑍) ≤ 𝑧, ((𝐷)‘𝑍), 𝑧))
224219, 223oveq12d 6567 . . . . . . . . . . . . . . 15 (𝑖 = → (((𝐶𝑖)‘𝑍)[,)if(((𝐷𝑖)‘𝑍) ≤ 𝑧, ((𝐷𝑖)‘𝑍), 𝑧)) = (((𝐶)‘𝑍)[,)if(((𝐷)‘𝑍) ≤ 𝑧, ((𝐷)‘𝑍), 𝑧)))
225224fveq2d 6107 . . . . . . . . . . . . . 14 (𝑖 = → (vol‘(((𝐶𝑖)‘𝑍)[,)if(((𝐷𝑖)‘𝑍) ≤ 𝑧, ((𝐷𝑖)‘𝑍), 𝑧))) = (vol‘(((𝐶)‘𝑍)[,)if(((𝐷)‘𝑍) ≤ 𝑧, ((𝐷)‘𝑍), 𝑧))))
226225cbvmptv 4678 . . . . . . . . . . . . 13 (𝑖 ∈ ℕ ↦ (vol‘(((𝐶𝑖)‘𝑍)[,)if(((𝐷𝑖)‘𝑍) ≤ 𝑧, ((𝐷𝑖)‘𝑍), 𝑧)))) = ( ∈ ℕ ↦ (vol‘(((𝐶)‘𝑍)[,)if(((𝐷)‘𝑍) ≤ 𝑧, ((𝐷)‘𝑍), 𝑧))))
227217, 226eqtri 2632 . . . . . . . . . . . 12 (𝑖 ∈ ℕ ↦ (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍))‘𝑖)[,)if(((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖) ≤ 𝑧, ((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖), 𝑧)))) = ( ∈ ℕ ↦ (vol‘(((𝐶)‘𝑍)[,)if(((𝐷)‘𝑍) ≤ 𝑧, ((𝐷)‘𝑍), 𝑧))))
228227a1i 11 . . . . . . . . . . 11 (𝑤 = 𝑧 → (𝑖 ∈ ℕ ↦ (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍))‘𝑖)[,)if(((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖) ≤ 𝑧, ((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖), 𝑧)))) = ( ∈ ℕ ↦ (vol‘(((𝐶)‘𝑍)[,)if(((𝐷)‘𝑍) ≤ 𝑧, ((𝐷)‘𝑍), 𝑧)))))
229 breq2 4587 . . . . . . . . . . . . . . . 16 (𝑤 = 𝑧 → (((𝐷)‘𝑍) ≤ 𝑤 ↔ ((𝐷)‘𝑍) ≤ 𝑧))
230 id 22 . . . . . . . . . . . . . . . 16 (𝑤 = 𝑧𝑤 = 𝑧)
231229, 230ifbieq2d 4061 . . . . . . . . . . . . . . 15 (𝑤 = 𝑧 → if(((𝐷)‘𝑍) ≤ 𝑤, ((𝐷)‘𝑍), 𝑤) = if(((𝐷)‘𝑍) ≤ 𝑧, ((𝐷)‘𝑍), 𝑧))
232231eqcomd 2616 . . . . . . . . . . . . . 14 (𝑤 = 𝑧 → if(((𝐷)‘𝑍) ≤ 𝑧, ((𝐷)‘𝑍), 𝑧) = if(((𝐷)‘𝑍) ≤ 𝑤, ((𝐷)‘𝑍), 𝑤))
233232oveq2d 6565 . . . . . . . . . . . . 13 (𝑤 = 𝑧 → (((𝐶)‘𝑍)[,)if(((𝐷)‘𝑍) ≤ 𝑧, ((𝐷)‘𝑍), 𝑧)) = (((𝐶)‘𝑍)[,)if(((𝐷)‘𝑍) ≤ 𝑤, ((𝐷)‘𝑍), 𝑤)))
234233fveq2d 6107 . . . . . . . . . . . 12 (𝑤 = 𝑧 → (vol‘(((𝐶)‘𝑍)[,)if(((𝐷)‘𝑍) ≤ 𝑧, ((𝐷)‘𝑍), 𝑧))) = (vol‘(((𝐶)‘𝑍)[,)if(((𝐷)‘𝑍) ≤ 𝑤, ((𝐷)‘𝑍), 𝑤))))
235234mpteq2dv 4673 . . . . . . . . . . 11 (𝑤 = 𝑧 → ( ∈ ℕ ↦ (vol‘(((𝐶)‘𝑍)[,)if(((𝐷)‘𝑍) ≤ 𝑧, ((𝐷)‘𝑍), 𝑧)))) = ( ∈ ℕ ↦ (vol‘(((𝐶)‘𝑍)[,)if(((𝐷)‘𝑍) ≤ 𝑤, ((𝐷)‘𝑍), 𝑤)))))
236228, 235eqtr2d 2645 . . . . . . . . . 10 (𝑤 = 𝑧 → ( ∈ ℕ ↦ (vol‘(((𝐶)‘𝑍)[,)if(((𝐷)‘𝑍) ≤ 𝑤, ((𝐷)‘𝑍), 𝑤)))) = (𝑖 ∈ ℕ ↦ (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍))‘𝑖)[,)if(((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖) ≤ 𝑧, ((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖), 𝑧)))))
237236fveq2d 6107 . . . . . . . . 9 (𝑤 = 𝑧 → (Σ^‘( ∈ ℕ ↦ (vol‘(((𝐶)‘𝑍)[,)if(((𝐷)‘𝑍) ≤ 𝑤, ((𝐷)‘𝑍), 𝑤))))) = (Σ^‘(𝑖 ∈ ℕ ↦ (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍))‘𝑖)[,)if(((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖) ≤ 𝑧, ((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖), 𝑧))))))
238212, 237breq12d 4596 . . . . . . . 8 (𝑤 = 𝑧 → ((𝑤 − (𝐴𝑍)) ≤ (Σ^‘( ∈ ℕ ↦ (vol‘(((𝐶)‘𝑍)[,)if(((𝐷)‘𝑍) ≤ 𝑤, ((𝐷)‘𝑍), 𝑤))))) ↔ (𝑧 − (𝐴𝑍)) ≤ (Σ^‘(𝑖 ∈ ℕ ↦ (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍))‘𝑖)[,)if(((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖) ≤ 𝑧, ((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖), 𝑧)))))))
239238cbvrabv 3172 . . . . . . 7 {𝑤 ∈ ((𝐴𝑍)[,](𝐵𝑍)) ∣ (𝑤 − (𝐴𝑍)) ≤ (Σ^‘( ∈ ℕ ↦ (vol‘(((𝐶)‘𝑍)[,)if(((𝐷)‘𝑍) ≤ 𝑤, ((𝐷)‘𝑍), 𝑤)))))} = {𝑧 ∈ ((𝐴𝑍)[,](𝐵𝑍)) ∣ (𝑧 − (𝐴𝑍)) ≤ (Σ^‘(𝑖 ∈ ℕ ↦ (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍))‘𝑖)[,)if(((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖) ≤ 𝑧, ((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖), 𝑧)))))}
240 eqid 2610 . . . . . . 7 sup({𝑤 ∈ ((𝐴𝑍)[,](𝐵𝑍)) ∣ (𝑤 − (𝐴𝑍)) ≤ (Σ^‘( ∈ ℕ ↦ (vol‘(((𝐶)‘𝑍)[,)if(((𝐷)‘𝑍) ≤ 𝑤, ((𝐷)‘𝑍), 𝑤)))))}, ℝ, < ) = sup({𝑤 ∈ ((𝐴𝑍)[,](𝐵𝑍)) ∣ (𝑤 − (𝐴𝑍)) ≤ (Σ^‘( ∈ ℕ ↦ (vol‘(((𝐶)‘𝑍)[,)if(((𝐷)‘𝑍) ≤ 𝑤, ((𝐷)‘𝑍), 𝑤)))))}, ℝ, < )
24181, 82, 83, 86, 89, 193, 211, 239, 240hoidmv1lelem3 39483 . . . . . 6 (((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) ∈ ℝ) → ((𝐵𝑍) − (𝐴𝑍)) ≤ (Σ^‘(𝑖 ∈ ℕ ↦ (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍))‘𝑖)[,)((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖))))))
242241, 209breqtrd 4609 . . . . 5 (((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) ∈ ℝ) → ((𝐵𝑍) − (𝐴𝑍)) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))))
24321, 80, 242syl2anc 691 . . . 4 (((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) ∧ ¬ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) = +∞) → ((𝐵𝑍) − (𝐴𝑍)) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))))
24420, 243pm2.61dan 828 . . 3 ((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) → ((𝐵𝑍) − (𝐴𝑍)) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))))
24525, 29, 32, 8, 1hoidmvn0val 39474 . . . . . . 7 (𝜑 → (𝐴(𝐿𝑋)𝐵) = ∏𝑘𝑋 (vol‘((𝐴𝑘)[,)(𝐵𝑘))))
24626prodeq1d 14490 . . . . . . 7 (𝜑 → ∏𝑘𝑋 (vol‘((𝐴𝑘)[,)(𝐵𝑘))) = ∏𝑘 ∈ {𝑍} (vol‘((𝐴𝑘)[,)(𝐵𝑘))))
247 volicore 39471 . . . . . . . . . 10 (((𝐴𝑍) ∈ ℝ ∧ (𝐵𝑍) ∈ ℝ) → (vol‘((𝐴𝑍)[,)(𝐵𝑍))) ∈ ℝ)
2489, 7, 247syl2anc 691 . . . . . . . . 9 (𝜑 → (vol‘((𝐴𝑍)[,)(𝐵𝑍))) ∈ ℝ)
249248recnd 9947 . . . . . . . 8 (𝜑 → (vol‘((𝐴𝑍)[,)(𝐵𝑍))) ∈ ℂ)
250119, 121oveq12d 6567 . . . . . . . . . 10 (𝑘 = 𝑍 → ((𝐴𝑘)[,)(𝐵𝑘)) = ((𝐴𝑍)[,)(𝐵𝑍)))
251250fveq2d 6107 . . . . . . . . 9 (𝑘 = 𝑍 → (vol‘((𝐴𝑘)[,)(𝐵𝑘))) = (vol‘((𝐴𝑍)[,)(𝐵𝑍))))
252251prodsn 14531 . . . . . . . 8 ((𝑍𝑉 ∧ (vol‘((𝐴𝑍)[,)(𝐵𝑍))) ∈ ℂ) → ∏𝑘 ∈ {𝑍} (vol‘((𝐴𝑘)[,)(𝐵𝑘))) = (vol‘((𝐴𝑍)[,)(𝐵𝑍))))
2532, 249, 252syl2anc 691 . . . . . . 7 (𝜑 → ∏𝑘 ∈ {𝑍} (vol‘((𝐴𝑘)[,)(𝐵𝑘))) = (vol‘((𝐴𝑍)[,)(𝐵𝑍))))
254245, 246, 2533eqtrd 2648 . . . . . 6 (𝜑 → (𝐴(𝐿𝑋)𝐵) = (vol‘((𝐴𝑍)[,)(𝐵𝑍))))
255254adantr 480 . . . . 5 ((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) → (𝐴(𝐿𝑋)𝐵) = (vol‘((𝐴𝑍)[,)(𝐵𝑍))))
256 volico 38876 . . . . . . 7 (((𝐴𝑍) ∈ ℝ ∧ (𝐵𝑍) ∈ ℝ) → (vol‘((𝐴𝑍)[,)(𝐵𝑍))) = if((𝐴𝑍) < (𝐵𝑍), ((𝐵𝑍) − (𝐴𝑍)), 0))
2579, 7, 256syl2anc 691 . . . . . 6 (𝜑 → (vol‘((𝐴𝑍)[,)(𝐵𝑍))) = if((𝐴𝑍) < (𝐵𝑍), ((𝐵𝑍) − (𝐴𝑍)), 0))
258257adantr 480 . . . . 5 ((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) → (vol‘((𝐴𝑍)[,)(𝐵𝑍))) = if((𝐴𝑍) < (𝐵𝑍), ((𝐵𝑍) − (𝐴𝑍)), 0))
259 iftrue 4042 . . . . . 6 ((𝐴𝑍) < (𝐵𝑍) → if((𝐴𝑍) < (𝐵𝑍), ((𝐵𝑍) − (𝐴𝑍)), 0) = ((𝐵𝑍) − (𝐴𝑍)))
260259adantl 481 . . . . 5 ((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) → if((𝐴𝑍) < (𝐵𝑍), ((𝐵𝑍) − (𝐴𝑍)), 0) = ((𝐵𝑍) − (𝐴𝑍)))
261255, 258, 2603eqtrd 2648 . . . 4 ((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) → (𝐴(𝐿𝑋)𝐵) = ((𝐵𝑍) − (𝐴𝑍)))
26259fveq2d 6107 . . . . 5 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗)))) = (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))))
263262adantr 480 . . . 4 ((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗)))) = (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))))
264261, 263breq12d 4596 . . 3 ((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) → ((𝐴(𝐿𝑋)𝐵) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗)))) ↔ ((𝐵𝑍) − (𝐴𝑍)) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))))))
265244, 264mpbird 246 . 2 ((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) → (𝐴(𝐿𝑋)𝐵) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗)))))
266245adantr 480 . . . 4 ((𝜑 ∧ ¬ (𝐴𝑍) < (𝐵𝑍)) → (𝐴(𝐿𝑋)𝐵) = ∏𝑘𝑋 (vol‘((𝐴𝑘)[,)(𝐵𝑘))))
267246adantr 480 . . . 4 ((𝜑 ∧ ¬ (𝐴𝑍) < (𝐵𝑍)) → ∏𝑘𝑋 (vol‘((𝐴𝑘)[,)(𝐵𝑘))) = ∏𝑘 ∈ {𝑍} (vol‘((𝐴𝑘)[,)(𝐵𝑘))))
268253adantr 480 . . . . 5 ((𝜑 ∧ ¬ (𝐴𝑍) < (𝐵𝑍)) → ∏𝑘 ∈ {𝑍} (vol‘((𝐴𝑘)[,)(𝐵𝑘))) = (vol‘((𝐴𝑍)[,)(𝐵𝑍))))
269257adantr 480 . . . . 5 ((𝜑 ∧ ¬ (𝐴𝑍) < (𝐵𝑍)) → (vol‘((𝐴𝑍)[,)(𝐵𝑍))) = if((𝐴𝑍) < (𝐵𝑍), ((𝐵𝑍) − (𝐴𝑍)), 0))
270 iffalse 4045 . . . . . 6 (¬ (𝐴𝑍) < (𝐵𝑍) → if((𝐴𝑍) < (𝐵𝑍), ((𝐵𝑍) − (𝐴𝑍)), 0) = 0)
271270adantl 481 . . . . 5 ((𝜑 ∧ ¬ (𝐴𝑍) < (𝐵𝑍)) → if((𝐴𝑍) < (𝐵𝑍), ((𝐵𝑍) − (𝐴𝑍)), 0) = 0)
272268, 269, 2713eqtrd 2648 . . . 4 ((𝜑 ∧ ¬ (𝐴𝑍) < (𝐵𝑍)) → ∏𝑘 ∈ {𝑍} (vol‘((𝐴𝑘)[,)(𝐵𝑘))) = 0)
273266, 267, 2723eqtrd 2648 . . 3 ((𝜑 ∧ ¬ (𝐴𝑍) < (𝐵𝑍)) → (𝐴(𝐿𝑋)𝐵) = 0)
27423a1i 11 . . . . 5 (𝜑 → ℕ ∈ V)
275274, 76sge0ge0 39277 . . . 4 (𝜑 → 0 ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗)))))
276275adantr 480 . . 3 ((𝜑 ∧ ¬ (𝐴𝑍) < (𝐵𝑍)) → 0 ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗)))))
277273, 276eqbrtrd 4605 . 2 ((𝜑 ∧ ¬ (𝐴𝑍) < (𝐵𝑍)) → (𝐴(𝐿𝑋)𝐵) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗)))))
278265, 277pm2.61dan 828 1 (𝜑 → (𝐴(𝐿𝑋)𝐵) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗)))))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∧ wa 383   ∧ w3a 1031   = wceq 1475   ∈ wcel 1977   ≠ wne 2780  ∀wral 2896  ∃wrex 2897  {crab 2900  Vcvv 3173   ⊆ wss 3540  ∅c0 3874  ifcif 4036  {csn 4125  ⟨cop 4131  ∪ ciun 4455   class class class wbr 4583   ↦ cmpt 4643  ⟶wf 5800  ‘cfv 5804  (class class class)co 6549   ↦ cmpt2 6551   ↑𝑚 cmap 7744  Xcixp 7794  Fincfn 7841  supcsup 8229  ℂcc 9813  ℝcr 9814  0cc0 9815  +∞cpnf 9950  ℝ*cxr 9952   < clt 9953   ≤ cle 9954   − cmin 10145  ℕcn 10897  [,)cico 12048  [,]cicc 12049  ∏cprod 14474  volcvol 23039  Σ^csumge0 39255 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-inf2 8421  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892  ax-pre-sup 9893 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-fal 1481  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-se 4998  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-isom 5813  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-of 6795  df-om 6958  df-1st 7059  df-2nd 7060  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-2o 7448  df-oadd 7451  df-er 7629  df-map 7746  df-pm 7747  df-ixp 7795  df-en 7842  df-dom 7843  df-sdom 7844  df-fin 7845  df-fi 8200  df-sup 8231  df-inf 8232  df-oi 8298  df-card 8648  df-cda 8873  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-div 10564  df-nn 10898  df-2 10956  df-3 10957  df-n0 11170  df-z 11255  df-uz 11564  df-q 11665  df-rp 11709  df-xneg 11822  df-xadd 11823  df-xmul 11824  df-ioo 12050  df-ico 12052  df-icc 12053  df-fz 12198  df-fzo 12335  df-fl 12455  df-seq 12664  df-exp 12723  df-hash 12980  df-cj 13687  df-re 13688  df-im 13689  df-sqrt 13823  df-abs 13824  df-clim 14067  df-rlim 14068  df-sum 14265  df-prod 14475  df-rest 15906  df-topgen 15927  df-psmet 19559  df-xmet 19560  df-met 19561  df-bl 19562  df-mopn 19563  df-top 20521  df-bases 20522  df-topon 20523  df-cmp 21000  df-ovol 23040  df-vol 23041  df-sumge0 39256 This theorem is referenced by:  hoidmvle  39490
 Copyright terms: Public domain W3C validator