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

Theorem hoidmv1le 40577
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 4204 . . . . . . . . . . . 12 (𝑍𝑉𝑍 ∈ {𝑍})
42, 3syl 17 . . . . . . . . . . 11 (𝜑𝑍 ∈ {𝑍})
5 hoidmv1le.x . . . . . . . . . . 11 𝑋 = {𝑍}
64, 5syl6eleqr 2711 . . . . . . . . . 10 (𝜑𝑍𝑋)
71, 6ffvelrnd 6358 . . . . . . . . 9 (𝜑 → (𝐵𝑍) ∈ ℝ)
8 hoidmv1le.a . . . . . . . . . 10 (𝜑𝐴:𝑋⟶ℝ)
98, 6ffvelrnd 6358 . . . . . . . . 9 (𝜑 → (𝐴𝑍) ∈ ℝ)
107, 9resubcld 10455 . . . . . . . 8 (𝜑 → ((𝐵𝑍) − (𝐴𝑍)) ∈ ℝ)
1110rexrd 10086 . . . . . . 7 (𝜑 → ((𝐵𝑍) − (𝐴𝑍)) ∈ ℝ*)
12 pnfxr 10089 . . . . . . . 8 +∞ ∈ ℝ*
1312a1i 11 . . . . . . 7 (𝜑 → +∞ ∈ ℝ*)
1410ltpnfd 11952 . . . . . . 7 (𝜑 → ((𝐵𝑍) − (𝐴𝑍)) < +∞)
1511, 13, 14xrltled 39305 . . . . . 6 (𝜑 → ((𝐵𝑍) − (𝐴𝑍)) ≤ +∞)
1615ad2antrr 762 . . . . 5 (((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) = +∞) → ((𝐵𝑍) − (𝐴𝑍)) ≤ +∞)
17 id 22 . . . . . . 7 ((Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) = +∞ → (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) = +∞)
1817eqcomd 2627 . . . . . 6 ((Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) = +∞ → +∞ = (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))))
1918adantl 482 . . . . 5 (((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) = +∞) → +∞ = (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))))
2016, 19breqtrd 4677 . . . 4 (((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) = +∞) → ((𝐵𝑍) − (𝐴𝑍)) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))))
21 simpl 473 . . . . 5 (((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) ∧ ¬ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) = +∞) → (𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)))
22 simpr 477 . . . . . 6 (((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) ∧ ¬ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) = +∞) → ¬ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) = +∞)
23 nnex 11023 . . . . . . . 8 ℕ ∈ V
2423a1i 11 . . . . . . 7 (((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) ∧ ¬ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) = +∞) → ℕ ∈ V)
25 hoidmv1le.l . . . . . . . . . . . 12 𝐿 = (𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑𝑚 𝑥), 𝑏 ∈ (ℝ ↑𝑚 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘𝑥 (vol‘((𝑎𝑘)[,)(𝑏𝑘))))))
265a1i 11 . . . . . . . . . . . . . 14 (𝜑𝑋 = {𝑍})
27 snfi 8035 . . . . . . . . . . . . . . 15 {𝑍} ∈ Fin
2827a1i 11 . . . . . . . . . . . . . 14 (𝜑 → {𝑍} ∈ Fin)
2926, 28eqeltrd 2700 . . . . . . . . . . . . 13 (𝜑𝑋 ∈ Fin)
3029adantr 481 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ) → 𝑋 ∈ Fin)
31 ne0i 3919 . . . . . . . . . . . . . 14 (𝑍𝑋𝑋 ≠ ∅)
326, 31syl 17 . . . . . . . . . . . . 13 (𝜑𝑋 ≠ ∅)
3332adantr 481 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ) → 𝑋 ≠ ∅)
34 hoidmv1le.c . . . . . . . . . . . . . 14 (𝜑𝐶:ℕ⟶(ℝ ↑𝑚 𝑋))
3534ffvelrnda 6357 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ ℕ) → (𝐶𝑗) ∈ (ℝ ↑𝑚 𝑋))
36 elmapi 7876 . . . . . . . . . . . . 13 ((𝐶𝑗) ∈ (ℝ ↑𝑚 𝑋) → (𝐶𝑗):𝑋⟶ℝ)
3735, 36syl 17 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ) → (𝐶𝑗):𝑋⟶ℝ)
38 hoidmv1le.d . . . . . . . . . . . . . 14 (𝜑𝐷:ℕ⟶(ℝ ↑𝑚 𝑋))
3938ffvelrnda 6357 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ ℕ) → (𝐷𝑗) ∈ (ℝ ↑𝑚 𝑋))
40 elmapi 7876 . . . . . . . . . . . . 13 ((𝐷𝑗) ∈ (ℝ ↑𝑚 𝑋) → (𝐷𝑗):𝑋⟶ℝ)
4139, 40syl 17 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ) → (𝐷𝑗):𝑋⟶ℝ)
4225, 30, 33, 37, 41hoidmvn0val 40567 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗)) = ∏𝑘𝑋 (vol‘(((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))))
435prodeq1i 14642 . . . . . . . . . . . 12 𝑘𝑋 (vol‘(((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) = ∏𝑘 ∈ {𝑍} (vol‘(((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
4443a1i 11 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ℕ) → ∏𝑘𝑋 (vol‘(((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) = ∏𝑘 ∈ {𝑍} (vol‘(((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))))
452adantr 481 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ) → 𝑍𝑉)
466adantr 481 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ ℕ) → 𝑍𝑋)
4737, 46ffvelrnd 6358 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗)‘𝑍) ∈ ℝ)
4841, 46ffvelrnd 6358 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ ℕ) → ((𝐷𝑗)‘𝑍) ∈ ℝ)
49 volicore 40564 . . . . . . . . . . . . . 14 ((((𝐶𝑗)‘𝑍) ∈ ℝ ∧ ((𝐷𝑗)‘𝑍) ∈ ℝ) → (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))) ∈ ℝ)
5047, 48, 49syl2anc 693 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ ℕ) → (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))) ∈ ℝ)
5150recnd 10065 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ) → (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))) ∈ ℂ)
52 fveq2 6189 . . . . . . . . . . . . . . 15 (𝑘 = 𝑍 → ((𝐶𝑗)‘𝑘) = ((𝐶𝑗)‘𝑍))
53 fveq2 6189 . . . . . . . . . . . . . . 15 (𝑘 = 𝑍 → ((𝐷𝑗)‘𝑘) = ((𝐷𝑗)‘𝑍))
5452, 53oveq12d 6665 . . . . . . . . . . . . . 14 (𝑘 = 𝑍 → (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) = (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))
5554fveq2d 6193 . . . . . . . . . . . . 13 (𝑘 = 𝑍 → (vol‘(((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) = (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))
5655prodsn 14686 . . . . . . . . . . . 12 ((𝑍𝑉 ∧ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))) ∈ ℂ) → ∏𝑘 ∈ {𝑍} (vol‘(((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) = (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))
5745, 51, 56syl2anc 693 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ℕ) → ∏𝑘 ∈ {𝑍} (vol‘(((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) = (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))
5842, 44, 573eqtrd 2659 . . . . . . . . . 10 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗)) = (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))
5958mpteq2dva 4742 . . . . . . . . 9 (𝜑 → (𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗))) = (𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))))
60 fveq2 6189 . . . . . . . . . . . . . . . . . . . 20 (𝑘 = 𝑙 → (𝑎𝑘) = (𝑎𝑙))
61 fveq2 6189 . . . . . . . . . . . . . . . . . . . 20 (𝑘 = 𝑙 → (𝑏𝑘) = (𝑏𝑙))
6260, 61oveq12d 6665 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 𝑙 → ((𝑎𝑘)[,)(𝑏𝑘)) = ((𝑎𝑙)[,)(𝑏𝑙)))
6362fveq2d 6193 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑙 → (vol‘((𝑎𝑘)[,)(𝑏𝑘))) = (vol‘((𝑎𝑙)[,)(𝑏𝑙))))
6463cbvprodv 14640 . . . . . . . . . . . . . . . . 17 𝑘𝑥 (vol‘((𝑎𝑘)[,)(𝑏𝑘))) = ∏𝑙𝑥 (vol‘((𝑎𝑙)[,)(𝑏𝑙)))
65 ifeq2 4089 . . . . . . . . . . . . . . . . 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 6717 . . . . . . . . . . . . . 14 (𝑎 ∈ (ℝ ↑𝑚 𝑥), 𝑏 ∈ (ℝ ↑𝑚 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘𝑥 (vol‘((𝑎𝑘)[,)(𝑏𝑘))))) = (𝑎 ∈ (ℝ ↑𝑚 𝑥), 𝑏 ∈ (ℝ ↑𝑚 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑙𝑥 (vol‘((𝑎𝑙)[,)(𝑏𝑙)))))
6968mpteq2i 4739 . . . . . . . . . . . . 13 (𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑𝑚 𝑥), 𝑏 ∈ (ℝ ↑𝑚 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘𝑥 (vol‘((𝑎𝑘)[,)(𝑏𝑘)))))) = (𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑𝑚 𝑥), 𝑏 ∈ (ℝ ↑𝑚 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑙𝑥 (vol‘((𝑎𝑙)[,)(𝑏𝑙))))))
7025, 69eqtri 2643 . . . . . . . . . . . 12 𝐿 = (𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑𝑚 𝑥), 𝑏 ∈ (ℝ ↑𝑚 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑙𝑥 (vol‘((𝑎𝑙)[,)(𝑏𝑙))))))
7170, 30, 37, 41hoidmvcl 40565 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗)) ∈ (0[,)+∞))
72 eqid 2621 . . . . . . . . . . 11 (𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗))) = (𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗)))
7371, 72fmptd 6383 . . . . . . . . . 10 (𝜑 → (𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗))):ℕ⟶(0[,)+∞))
74 icossicc 12257 . . . . . . . . . . 11 (0[,)+∞) ⊆ (0[,]+∞)
7574a1i 11 . . . . . . . . . 10 (𝜑 → (0[,)+∞) ⊆ (0[,]+∞))
7673, 75fssd 6055 . . . . . . . . 9 (𝜑 → (𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗))):ℕ⟶(0[,]+∞))
7759, 76feq1dd 39169 . . . . . . . 8 (𝜑 → (𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))):ℕ⟶(0[,]+∞))
7877ad2antrr 762 . . . . . . 7 (((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) ∧ ¬ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) = +∞) → (𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))):ℕ⟶(0[,]+∞))
7924, 78sge0repnf 40372 . . . . . 6 (((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) ∧ ¬ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) = +∞) → ((Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) ∈ ℝ ↔ ¬ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) = +∞))
8022, 79mpbird 247 . . . . 5 (((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) ∧ ¬ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) = +∞) → (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) ∈ ℝ)
819ad2antrr 762 . . . . . . 7 (((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) ∈ ℝ) → (𝐴𝑍) ∈ ℝ)
827ad2antrr 762 . . . . . . 7 (((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) ∈ ℝ) → (𝐵𝑍) ∈ ℝ)
83 simplr 792 . . . . . . 7 (((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) ∈ ℝ) → (𝐴𝑍) < (𝐵𝑍))
84 eqid 2621 . . . . . . . . 9 (𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍)) = (𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍))
8547, 84fmptd 6383 . . . . . . . 8 (𝜑 → (𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍)):ℕ⟶ℝ)
8685ad2antrr 762 . . . . . . 7 (((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) ∈ ℝ) → (𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍)):ℕ⟶ℝ)
87 eqid 2621 . . . . . . . . 9 (𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍)) = (𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))
8848, 87fmptd 6383 . . . . . . . 8 (𝜑 → (𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍)):ℕ⟶ℝ)
8988ad2antrr 762 . . . . . . 7 (((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) ∈ ℝ) → (𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍)):ℕ⟶ℝ)
90 hoidmv1le.s . . . . . . . . . . . . . . . . 17 (𝜑X𝑘𝑋 ((𝐴𝑘)[,)(𝐵𝑘)) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
915eleq2i 2692 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑘𝑋𝑘 ∈ {𝑍})
9291biimpi 206 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑘𝑋𝑘 ∈ {𝑍})
93 elsni 4192 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑘 ∈ {𝑍} → 𝑘 = 𝑍)
9492, 93syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑘𝑋𝑘 = 𝑍)
9594, 54syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘𝑋 → (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) = (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))
9695rgen 2921 . . . . . . . . . . . . . . . . . . . . 21 𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) = (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))
97 ixpeq2 7919 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) = (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) → X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) = X𝑘𝑋 (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))
9896, 97ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) = X𝑘𝑋 (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))
9998a1i 11 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ ℕ → X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) = X𝑘𝑋 (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))
10099iuneq2i 4537 . . . . . . . . . . . . . . . . . 18 𝑗 ∈ ℕ X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) = 𝑗 ∈ ℕ X𝑘𝑋 (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))
101100a1i 11 . . . . . . . . . . . . . . . . 17 (𝜑 𝑗 ∈ ℕ X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) = 𝑗 ∈ ℕ X𝑘𝑋 (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))
10290, 101sseqtrd 3639 . . . . . . . . . . . . . . . 16 (𝜑X𝑘𝑋 ((𝐴𝑘)[,)(𝐵𝑘)) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))
103102adantr 481 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ ((𝐴𝑍)[,)(𝐵𝑍))) → X𝑘𝑋 ((𝐴𝑘)[,)(𝐵𝑘)) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))
104 id 22 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ((𝐴𝑍)[,)(𝐵𝑍)) → 𝑥 ∈ ((𝐴𝑍)[,)(𝐵𝑍)))
105 eqidd 2622 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ((𝐴𝑍)[,)(𝐵𝑍)) → {⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑥⟩})
106 opeq2 4401 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 = 𝑥 → ⟨𝑍, 𝑦⟩ = ⟨𝑍, 𝑥⟩)
107106sneqd 4187 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 = 𝑥 → {⟨𝑍, 𝑦⟩} = {⟨𝑍, 𝑥⟩})
108107eqeq2d 2631 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = 𝑥 → ({⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩} ↔ {⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑥⟩}))
109108rspcev 3307 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ∈ ((𝐴𝑍)[,)(𝐵𝑍)) ∧ {⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑥⟩}) → ∃𝑦 ∈ ((𝐴𝑍)[,)(𝐵𝑍)){⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩})
110104, 105, 109syl2anc 693 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ((𝐴𝑍)[,)(𝐵𝑍)) → ∃𝑦 ∈ ((𝐴𝑍)[,)(𝐵𝑍)){⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩})
111110adantl 482 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ ((𝐴𝑍)[,)(𝐵𝑍))) → ∃𝑦 ∈ ((𝐴𝑍)[,)(𝐵𝑍)){⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩})
112 elixpsn 7944 . . . . . . . . . . . . . . . . . . 19 (𝑍𝑉 → ({⟨𝑍, 𝑥⟩} ∈ X𝑘 ∈ {𝑍} ((𝐴𝑍)[,)(𝐵𝑍)) ↔ ∃𝑦 ∈ ((𝐴𝑍)[,)(𝐵𝑍)){⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩}))
1132, 112syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑 → ({⟨𝑍, 𝑥⟩} ∈ X𝑘 ∈ {𝑍} ((𝐴𝑍)[,)(𝐵𝑍)) ↔ ∃𝑦 ∈ ((𝐴𝑍)[,)(𝐵𝑍)){⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩}))
114113adantr 481 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ ((𝐴𝑍)[,)(𝐵𝑍))) → ({⟨𝑍, 𝑥⟩} ∈ X𝑘 ∈ {𝑍} ((𝐴𝑍)[,)(𝐵𝑍)) ↔ ∃𝑦 ∈ ((𝐴𝑍)[,)(𝐵𝑍)){⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩}))
115111, 114mpbird 247 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ ((𝐴𝑍)[,)(𝐵𝑍))) → {⟨𝑍, 𝑥⟩} ∈ X𝑘 ∈ {𝑍} ((𝐴𝑍)[,)(𝐵𝑍)))
1165eqcomi 2630 . . . . . . . . . . . . . . . . . . . 20 {𝑍} = 𝑋
117 ixpeq1 7916 . . . . . . . . . . . . . . . . . . . 20 ({𝑍} = 𝑋X𝑘 ∈ {𝑍} ((𝐴𝑍)[,)(𝐵𝑍)) = X𝑘𝑋 ((𝐴𝑍)[,)(𝐵𝑍)))
118116, 117ax-mp 5 . . . . . . . . . . . . . . . . . . 19 X𝑘 ∈ {𝑍} ((𝐴𝑍)[,)(𝐵𝑍)) = X𝑘𝑋 ((𝐴𝑍)[,)(𝐵𝑍))
119 fveq2 6189 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑘 = 𝑍 → (𝐴𝑘) = (𝐴𝑍))
12094, 119syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑘𝑋 → (𝐴𝑘) = (𝐴𝑍))
121 fveq2 6189 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑘 = 𝑍 → (𝐵𝑘) = (𝐵𝑍))
12294, 121syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑘𝑋 → (𝐵𝑘) = (𝐵𝑍))
123120, 122oveq12d 6665 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘𝑋 → ((𝐴𝑘)[,)(𝐵𝑘)) = ((𝐴𝑍)[,)(𝐵𝑍)))
124123eqcomd 2627 . . . . . . . . . . . . . . . . . . . . 21 (𝑘𝑋 → ((𝐴𝑍)[,)(𝐵𝑍)) = ((𝐴𝑘)[,)(𝐵𝑘)))
125124rgen 2921 . . . . . . . . . . . . . . . . . . . 20 𝑘𝑋 ((𝐴𝑍)[,)(𝐵𝑍)) = ((𝐴𝑘)[,)(𝐵𝑘))
126 ixpeq2 7919 . . . . . . . . . . . . . . . . . . . 20 (∀𝑘𝑋 ((𝐴𝑍)[,)(𝐵𝑍)) = ((𝐴𝑘)[,)(𝐵𝑘)) → X𝑘𝑋 ((𝐴𝑍)[,)(𝐵𝑍)) = X𝑘𝑋 ((𝐴𝑘)[,)(𝐵𝑘)))
127125, 126ax-mp 5 . . . . . . . . . . . . . . . . . . 19 X𝑘𝑋 ((𝐴𝑍)[,)(𝐵𝑍)) = X𝑘𝑋 ((𝐴𝑘)[,)(𝐵𝑘))
128118, 127eqtri 2643 . . . . . . . . . . . . . . . . . 18 X𝑘 ∈ {𝑍} ((𝐴𝑍)[,)(𝐵𝑍)) = X𝑘𝑋 ((𝐴𝑘)[,)(𝐵𝑘))
129128a1i 11 . . . . . . . . . . . . . . . . 17 (𝜑X𝑘 ∈ {𝑍} ((𝐴𝑍)[,)(𝐵𝑍)) = X𝑘𝑋 ((𝐴𝑘)[,)(𝐵𝑘)))
130129adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ ((𝐴𝑍)[,)(𝐵𝑍))) → X𝑘 ∈ {𝑍} ((𝐴𝑍)[,)(𝐵𝑍)) = X𝑘𝑋 ((𝐴𝑘)[,)(𝐵𝑘)))
131115, 130eleqtrd 2702 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ ((𝐴𝑍)[,)(𝐵𝑍))) → {⟨𝑍, 𝑥⟩} ∈ X𝑘𝑋 ((𝐴𝑘)[,)(𝐵𝑘)))
132103, 131sseldd 3602 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ ((𝐴𝑍)[,)(𝐵𝑍))) → {⟨𝑍, 𝑥⟩} ∈ 𝑗 ∈ ℕ X𝑘𝑋 (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))
133 eliun 4522 . . . . . . . . . . . . . 14 ({⟨𝑍, 𝑥⟩} ∈ 𝑗 ∈ ℕ X𝑘𝑋 (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) ↔ ∃𝑗 ∈ ℕ {⟨𝑍, 𝑥⟩} ∈ X𝑘𝑋 (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))
134132, 133sylib 208 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ ((𝐴𝑍)[,)(𝐵𝑍))) → ∃𝑗 ∈ ℕ {⟨𝑍, 𝑥⟩} ∈ X𝑘𝑋 (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))
135 ixpeq1 7916 . . . . . . . . . . . . . . . . . . . . . 22 (𝑋 = {𝑍} → X𝑘𝑋 (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) = X𝑘 ∈ {𝑍} (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))
1365, 135ax-mp 5 . . . . . . . . . . . . . . . . . . . . 21 X𝑘𝑋 (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) = X𝑘 ∈ {𝑍} (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))
137136eleq2i 2692 . . . . . . . . . . . . . . . . . . . 20 ({⟨𝑍, 𝑥⟩} ∈ X𝑘𝑋 (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) ↔ {⟨𝑍, 𝑥⟩} ∈ X𝑘 ∈ {𝑍} (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))
138137biimpi 206 . . . . . . . . . . . . . . . . . . 19 ({⟨𝑍, 𝑥⟩} ∈ X𝑘𝑋 (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) → {⟨𝑍, 𝑥⟩} ∈ X𝑘 ∈ {𝑍} (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))
139138adantl 482 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ {⟨𝑍, 𝑥⟩} ∈ X𝑘𝑋 (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))) → {⟨𝑍, 𝑥⟩} ∈ X𝑘 ∈ {𝑍} (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))
140 elixpsn 7944 . . . . . . . . . . . . . . . . . . . 20 (𝑍𝑉 → ({⟨𝑍, 𝑥⟩} ∈ X𝑘 ∈ {𝑍} (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) ↔ ∃𝑦 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)){⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩}))
1412, 140syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ({⟨𝑍, 𝑥⟩} ∈ X𝑘 ∈ {𝑍} (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) ↔ ∃𝑦 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)){⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩}))
142141adantr 481 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ {⟨𝑍, 𝑥⟩} ∈ X𝑘𝑋 (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))) → ({⟨𝑍, 𝑥⟩} ∈ X𝑘 ∈ {𝑍} (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) ↔ ∃𝑦 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)){⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩}))
143139, 142mpbid 222 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ {⟨𝑍, 𝑥⟩} ∈ X𝑘𝑋 (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))) → ∃𝑦 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)){⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩})
144 opex 4930 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑍, 𝑥⟩ ∈ V
145144sneqr 4369 . . . . . . . . . . . . . . . . . . . . . . . . 25 ({⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩} → ⟨𝑍, 𝑥⟩ = ⟨𝑍, 𝑦⟩)
146145adantl 482 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ {⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩}) → ⟨𝑍, 𝑥⟩ = ⟨𝑍, 𝑦⟩)
147 vex 3201 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝑥 ∈ V
148147a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑𝑥 ∈ V)
149 opthg 4944 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑍𝑉𝑥 ∈ V) → (⟨𝑍, 𝑥⟩ = ⟨𝑍, 𝑦⟩ ↔ (𝑍 = 𝑍𝑥 = 𝑦)))
1502, 148, 149syl2anc 693 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (⟨𝑍, 𝑥⟩ = ⟨𝑍, 𝑦⟩ ↔ (𝑍 = 𝑍𝑥 = 𝑦)))
151150adantr 481 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ {⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩}) → (⟨𝑍, 𝑥⟩ = ⟨𝑍, 𝑦⟩ ↔ (𝑍 = 𝑍𝑥 = 𝑦)))
152146, 151mpbid 222 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ {⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩}) → (𝑍 = 𝑍𝑥 = 𝑦))
153152simprd 479 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ {⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩}) → 𝑥 = 𝑦)
1541533adant2 1079 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑦 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) ∧ {⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩}) → 𝑥 = 𝑦)
155 simp2 1061 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑦 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) ∧ {⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩}) → 𝑦 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))
156154, 155eqeltrd 2700 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑦 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) ∧ {⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩}) → 𝑥 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))
1571563exp 1263 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑦 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) → ({⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩} → 𝑥 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))))
158157adantr 481 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ {⟨𝑍, 𝑥⟩} ∈ X𝑘𝑋 (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))) → (𝑦 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) → ({⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩} → 𝑥 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))))
159158rexlimdv 3028 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ {⟨𝑍, 𝑥⟩} ∈ X𝑘𝑋 (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))) → (∃𝑦 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)){⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩} → 𝑥 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))
160143, 159mpd 15 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ {⟨𝑍, 𝑥⟩} ∈ X𝑘𝑋 (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))) → 𝑥 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))
161160ex 450 . . . . . . . . . . . . . . 15 (𝜑 → ({⟨𝑍, 𝑥⟩} ∈ X𝑘𝑋 (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) → 𝑥 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))
162161ad2antrr 762 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ ((𝐴𝑍)[,)(𝐵𝑍))) ∧ 𝑗 ∈ ℕ) → ({⟨𝑍, 𝑥⟩} ∈ X𝑘𝑋 (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) → 𝑥 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))
163162reximdva 3016 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ ((𝐴𝑍)[,)(𝐵𝑍))) → (∃𝑗 ∈ ℕ {⟨𝑍, 𝑥⟩} ∈ X𝑘𝑋 (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) → ∃𝑗 ∈ ℕ 𝑥 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))
164134, 163mpd 15 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ ((𝐴𝑍)[,)(𝐵𝑍))) → ∃𝑗 ∈ ℕ 𝑥 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))
165 eliun 4522 . . . . . . . . . . . 12 (𝑥 𝑗 ∈ ℕ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) ↔ ∃𝑗 ∈ ℕ 𝑥 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))
166164, 165sylibr 224 . . . . . . . . . . 11 ((𝜑𝑥 ∈ ((𝐴𝑍)[,)(𝐵𝑍))) → 𝑥 𝑗 ∈ ℕ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))
167166ralrimiva 2965 . . . . . . . . . 10 (𝜑 → ∀𝑥 ∈ ((𝐴𝑍)[,)(𝐵𝑍))𝑥 𝑗 ∈ ℕ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))
168 dfss3 3590 . . . . . . . . . 10 (((𝐴𝑍)[,)(𝐵𝑍)) ⊆ 𝑗 ∈ ℕ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) ↔ ∀𝑥 ∈ ((𝐴𝑍)[,)(𝐵𝑍))𝑥 𝑗 ∈ ℕ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))
169167, 168sylibr 224 . . . . . . . . 9 (𝜑 → ((𝐴𝑍)[,)(𝐵𝑍)) ⊆ 𝑗 ∈ ℕ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))
170 eqidd 2622 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ ℕ) → (𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍)) = (𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍)))
171 fveq2 6189 . . . . . . . . . . . . . . 15 (𝑗 = 𝑖 → (𝐶𝑗) = (𝐶𝑖))
172171fveq1d 6191 . . . . . . . . . . . . . 14 (𝑗 = 𝑖 → ((𝐶𝑗)‘𝑍) = ((𝐶𝑖)‘𝑍))
173172adantl 482 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ ℕ) ∧ 𝑗 = 𝑖) → ((𝐶𝑗)‘𝑍) = ((𝐶𝑖)‘𝑍))
174 simpr 477 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ ℕ) → 𝑖 ∈ ℕ)
175 fvexd 6201 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ ℕ) → ((𝐶𝑖)‘𝑍) ∈ V)
176170, 173, 174, 175fvmptd 6286 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ ℕ) → ((𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍))‘𝑖) = ((𝐶𝑖)‘𝑍))
177 eqidd 2622 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ ℕ) → (𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍)) = (𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍)))
178 fveq2 6189 . . . . . . . . . . . . . . 15 (𝑗 = 𝑖 → (𝐷𝑗) = (𝐷𝑖))
179178fveq1d 6191 . . . . . . . . . . . . . 14 (𝑗 = 𝑖 → ((𝐷𝑗)‘𝑍) = ((𝐷𝑖)‘𝑍))
180179adantl 482 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ ℕ) ∧ 𝑗 = 𝑖) → ((𝐷𝑗)‘𝑍) = ((𝐷𝑖)‘𝑍))
181 fvexd 6201 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ ℕ) → ((𝐷𝑖)‘𝑍) ∈ V)
182177, 180, 174, 181fvmptd 6286 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ ℕ) → ((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖) = ((𝐷𝑖)‘𝑍))
183176, 182oveq12d 6665 . . . . . . . . . . 11 ((𝜑𝑖 ∈ ℕ) → (((𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍))‘𝑖)[,)((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖)) = (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)))
184183iuneq2dv 4540 . . . . . . . . . 10 (𝜑 𝑖 ∈ ℕ (((𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍))‘𝑖)[,)((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖)) = 𝑖 ∈ ℕ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)))
185172, 179oveq12d 6665 . . . . . . . . . . . . 13 (𝑗 = 𝑖 → (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) = (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)))
186185cbviunv 4557 . . . . . . . . . . . 12 𝑗 ∈ ℕ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) = 𝑖 ∈ ℕ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍))
187186eqcomi 2630 . . . . . . . . . . 11 𝑖 ∈ ℕ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)) = 𝑗 ∈ ℕ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))
188187a1i 11 . . . . . . . . . 10 (𝜑 𝑖 ∈ ℕ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)) = 𝑗 ∈ ℕ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))
189184, 188eqtr2d 2656 . . . . . . . . 9 (𝜑 𝑗 ∈ ℕ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) = 𝑖 ∈ ℕ (((𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍))‘𝑖)[,)((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖)))
190169, 189sseqtrd 3639 . . . . . . . 8 (𝜑 → ((𝐴𝑍)[,)(𝐵𝑍)) ⊆ 𝑖 ∈ ℕ (((𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍))‘𝑖)[,)((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖)))
191190ad2antrr 762 . . . . . . 7 (((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) ∈ ℝ) → ((𝐴𝑍)[,)(𝐵𝑍)) ⊆ 𝑖 ∈ ℕ (((𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍))‘𝑖)[,)((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖)))
192 fvex 6199 . . . . . . . . . . . . . . 15 ((𝐶𝑖)‘𝑍) ∈ V
193172, 84, 192fvmpt 6280 . . . . . . . . . . . . . 14 (𝑖 ∈ ℕ → ((𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍))‘𝑖) = ((𝐶𝑖)‘𝑍))
194 fvex 6199 . . . . . . . . . . . . . . 15 ((𝐷𝑖)‘𝑍) ∈ V
195179, 87, 194fvmpt 6280 . . . . . . . . . . . . . 14 (𝑖 ∈ ℕ → ((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖) = ((𝐷𝑖)‘𝑍))
196193, 195oveq12d 6665 . . . . . . . . . . . . 13 (𝑖 ∈ ℕ → (((𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍))‘𝑖)[,)((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖)) = (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)))
197196fveq2d 6193 . . . . . . . . . . . 12 (𝑖 ∈ ℕ → (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍))‘𝑖)[,)((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖))) = (vol‘(((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍))))
198197mpteq2ia 4738 . . . . . . . . . . 11 (𝑖 ∈ ℕ ↦ (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍))‘𝑖)[,)((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖)))) = (𝑖 ∈ ℕ ↦ (vol‘(((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍))))
199 eqcom 2628 . . . . . . . . . . . . . . . 16 (𝑗 = 𝑖𝑖 = 𝑗)
200199imbi1i 339 . . . . . . . . . . . . . . 15 ((𝑗 = 𝑖 → (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) = (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍))) ↔ (𝑖 = 𝑗 → (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) = (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍))))
201 eqcom 2628 . . . . . . . . . . . . . . . 16 ((((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) = (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)) ↔ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)) = (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))
202201imbi2i 326 . . . . . . . . . . . . . . 15 ((𝑖 = 𝑗 → (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) = (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍))) ↔ (𝑖 = 𝑗 → (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)) = (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))
203200, 202bitri 264 . . . . . . . . . . . . . 14 ((𝑗 = 𝑖 → (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) = (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍))) ↔ (𝑖 = 𝑗 → (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)) = (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))
204185, 203mpbi 220 . . . . . . . . . . . . 13 (𝑖 = 𝑗 → (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)) = (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))
205204fveq2d 6193 . . . . . . . . . . . 12 (𝑖 = 𝑗 → (vol‘(((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍))) = (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))
206205cbvmptv 4748 . . . . . . . . . . 11 (𝑖 ∈ ℕ ↦ (vol‘(((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)))) = (𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))
207198, 206eqtri 2643 . . . . . . . . . 10 (𝑖 ∈ ℕ ↦ (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍))‘𝑖)[,)((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖)))) = (𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))
208207fveq2i 6192 . . . . . . . . 9 ^‘(𝑖 ∈ ℕ ↦ (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍))‘𝑖)[,)((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖))))) = (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))))
209208a1i 11 . . . . . . . 8 (((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) ∈ ℝ) → (Σ^‘(𝑖 ∈ ℕ ↦ (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍))‘𝑖)[,)((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖))))) = (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))))
210 simpr 477 . . . . . . . 8 (((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) ∈ ℝ) → (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) ∈ ℝ)
211209, 210eqeltrd 2700 . . . . . . 7 (((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) ∈ ℝ) → (Σ^‘(𝑖 ∈ ℕ ↦ (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍))‘𝑖)[,)((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖))))) ∈ ℝ)
212 oveq1 6654 . . . . . . . . 9 (𝑤 = 𝑧 → (𝑤 − (𝐴𝑍)) = (𝑧 − (𝐴𝑍)))
213195breq1d 4661 . . . . . . . . . . . . . . . . 17 (𝑖 ∈ ℕ → (((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖) ≤ 𝑧 ↔ ((𝐷𝑖)‘𝑍) ≤ 𝑧))
214213, 195ifbieq1d 4107 . . . . . . . . . . . . . . . 16 (𝑖 ∈ ℕ → if(((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖) ≤ 𝑧, ((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖), 𝑧) = if(((𝐷𝑖)‘𝑍) ≤ 𝑧, ((𝐷𝑖)‘𝑍), 𝑧))
215193, 214oveq12d 6665 . . . . . . . . . . . . . . 15 (𝑖 ∈ ℕ → (((𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍))‘𝑖)[,)if(((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖) ≤ 𝑧, ((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖), 𝑧)) = (((𝐶𝑖)‘𝑍)[,)if(((𝐷𝑖)‘𝑍) ≤ 𝑧, ((𝐷𝑖)‘𝑍), 𝑧)))
216215fveq2d 6193 . . . . . . . . . . . . . 14 (𝑖 ∈ ℕ → (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍))‘𝑖)[,)if(((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖) ≤ 𝑧, ((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖), 𝑧))) = (vol‘(((𝐶𝑖)‘𝑍)[,)if(((𝐷𝑖)‘𝑍) ≤ 𝑧, ((𝐷𝑖)‘𝑍), 𝑧))))
217216mpteq2ia 4738 . . . . . . . . . . . . 13 (𝑖 ∈ ℕ ↦ (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍))‘𝑖)[,)if(((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖) ≤ 𝑧, ((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖), 𝑧)))) = (𝑖 ∈ ℕ ↦ (vol‘(((𝐶𝑖)‘𝑍)[,)if(((𝐷𝑖)‘𝑍) ≤ 𝑧, ((𝐷𝑖)‘𝑍), 𝑧))))
218 fveq2 6189 . . . . . . . . . . . . . . . . 17 (𝑖 = → (𝐶𝑖) = (𝐶))
219218fveq1d 6191 . . . . . . . . . . . . . . . 16 (𝑖 = → ((𝐶𝑖)‘𝑍) = ((𝐶)‘𝑍))
220 fveq2 6189 . . . . . . . . . . . . . . . . . . 19 (𝑖 = → (𝐷𝑖) = (𝐷))
221220fveq1d 6191 . . . . . . . . . . . . . . . . . 18 (𝑖 = → ((𝐷𝑖)‘𝑍) = ((𝐷)‘𝑍))
222221breq1d 4661 . . . . . . . . . . . . . . . . 17 (𝑖 = → (((𝐷𝑖)‘𝑍) ≤ 𝑧 ↔ ((𝐷)‘𝑍) ≤ 𝑧))
223222, 221ifbieq1d 4107 . . . . . . . . . . . . . . . 16 (𝑖 = → if(((𝐷𝑖)‘𝑍) ≤ 𝑧, ((𝐷𝑖)‘𝑍), 𝑧) = if(((𝐷)‘𝑍) ≤ 𝑧, ((𝐷)‘𝑍), 𝑧))
224219, 223oveq12d 6665 . . . . . . . . . . . . . . 15 (𝑖 = → (((𝐶𝑖)‘𝑍)[,)if(((𝐷𝑖)‘𝑍) ≤ 𝑧, ((𝐷𝑖)‘𝑍), 𝑧)) = (((𝐶)‘𝑍)[,)if(((𝐷)‘𝑍) ≤ 𝑧, ((𝐷)‘𝑍), 𝑧)))
225224fveq2d 6193 . . . . . . . . . . . . . 14 (𝑖 = → (vol‘(((𝐶𝑖)‘𝑍)[,)if(((𝐷𝑖)‘𝑍) ≤ 𝑧, ((𝐷𝑖)‘𝑍), 𝑧))) = (vol‘(((𝐶)‘𝑍)[,)if(((𝐷)‘𝑍) ≤ 𝑧, ((𝐷)‘𝑍), 𝑧))))
226225cbvmptv 4748 . . . . . . . . . . . . 13 (𝑖 ∈ ℕ ↦ (vol‘(((𝐶𝑖)‘𝑍)[,)if(((𝐷𝑖)‘𝑍) ≤ 𝑧, ((𝐷𝑖)‘𝑍), 𝑧)))) = ( ∈ ℕ ↦ (vol‘(((𝐶)‘𝑍)[,)if(((𝐷)‘𝑍) ≤ 𝑧, ((𝐷)‘𝑍), 𝑧))))
227217, 226eqtri 2643 . . . . . . . . . . . 12 (𝑖 ∈ ℕ ↦ (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍))‘𝑖)[,)if(((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖) ≤ 𝑧, ((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖), 𝑧)))) = ( ∈ ℕ ↦ (vol‘(((𝐶)‘𝑍)[,)if(((𝐷)‘𝑍) ≤ 𝑧, ((𝐷)‘𝑍), 𝑧))))
228227a1i 11 . . . . . . . . . . 11 (𝑤 = 𝑧 → (𝑖 ∈ ℕ ↦ (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍))‘𝑖)[,)if(((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖) ≤ 𝑧, ((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖), 𝑧)))) = ( ∈ ℕ ↦ (vol‘(((𝐶)‘𝑍)[,)if(((𝐷)‘𝑍) ≤ 𝑧, ((𝐷)‘𝑍), 𝑧)))))
229 breq2 4655 . . . . . . . . . . . . . . . 16 (𝑤 = 𝑧 → (((𝐷)‘𝑍) ≤ 𝑤 ↔ ((𝐷)‘𝑍) ≤ 𝑧))
230 id 22 . . . . . . . . . . . . . . . 16 (𝑤 = 𝑧𝑤 = 𝑧)
231229, 230ifbieq2d 4109 . . . . . . . . . . . . . . 15 (𝑤 = 𝑧 → if(((𝐷)‘𝑍) ≤ 𝑤, ((𝐷)‘𝑍), 𝑤) = if(((𝐷)‘𝑍) ≤ 𝑧, ((𝐷)‘𝑍), 𝑧))
232231eqcomd 2627 . . . . . . . . . . . . . 14 (𝑤 = 𝑧 → if(((𝐷)‘𝑍) ≤ 𝑧, ((𝐷)‘𝑍), 𝑧) = if(((𝐷)‘𝑍) ≤ 𝑤, ((𝐷)‘𝑍), 𝑤))
233232oveq2d 6663 . . . . . . . . . . . . 13 (𝑤 = 𝑧 → (((𝐶)‘𝑍)[,)if(((𝐷)‘𝑍) ≤ 𝑧, ((𝐷)‘𝑍), 𝑧)) = (((𝐶)‘𝑍)[,)if(((𝐷)‘𝑍) ≤ 𝑤, ((𝐷)‘𝑍), 𝑤)))
234233fveq2d 6193 . . . . . . . . . . . 12 (𝑤 = 𝑧 → (vol‘(((𝐶)‘𝑍)[,)if(((𝐷)‘𝑍) ≤ 𝑧, ((𝐷)‘𝑍), 𝑧))) = (vol‘(((𝐶)‘𝑍)[,)if(((𝐷)‘𝑍) ≤ 𝑤, ((𝐷)‘𝑍), 𝑤))))
235234mpteq2dv 4743 . . . . . . . . . . 11 (𝑤 = 𝑧 → ( ∈ ℕ ↦ (vol‘(((𝐶)‘𝑍)[,)if(((𝐷)‘𝑍) ≤ 𝑧, ((𝐷)‘𝑍), 𝑧)))) = ( ∈ ℕ ↦ (vol‘(((𝐶)‘𝑍)[,)if(((𝐷)‘𝑍) ≤ 𝑤, ((𝐷)‘𝑍), 𝑤)))))
236228, 235eqtr2d 2656 . . . . . . . . . 10 (𝑤 = 𝑧 → ( ∈ ℕ ↦ (vol‘(((𝐶)‘𝑍)[,)if(((𝐷)‘𝑍) ≤ 𝑤, ((𝐷)‘𝑍), 𝑤)))) = (𝑖 ∈ ℕ ↦ (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍))‘𝑖)[,)if(((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖) ≤ 𝑧, ((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖), 𝑧)))))
237236fveq2d 6193 . . . . . . . . 9 (𝑤 = 𝑧 → (Σ^‘( ∈ ℕ ↦ (vol‘(((𝐶)‘𝑍)[,)if(((𝐷)‘𝑍) ≤ 𝑤, ((𝐷)‘𝑍), 𝑤))))) = (Σ^‘(𝑖 ∈ ℕ ↦ (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍))‘𝑖)[,)if(((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖) ≤ 𝑧, ((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖), 𝑧))))))
238212, 237breq12d 4664 . . . . . . . 8 (𝑤 = 𝑧 → ((𝑤 − (𝐴𝑍)) ≤ (Σ^‘( ∈ ℕ ↦ (vol‘(((𝐶)‘𝑍)[,)if(((𝐷)‘𝑍) ≤ 𝑤, ((𝐷)‘𝑍), 𝑤))))) ↔ (𝑧 − (𝐴𝑍)) ≤ (Σ^‘(𝑖 ∈ ℕ ↦ (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍))‘𝑖)[,)if(((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖) ≤ 𝑧, ((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖), 𝑧)))))))
239238cbvrabv 3197 . . . . . . 7 {𝑤 ∈ ((𝐴𝑍)[,](𝐵𝑍)) ∣ (𝑤 − (𝐴𝑍)) ≤ (Σ^‘( ∈ ℕ ↦ (vol‘(((𝐶)‘𝑍)[,)if(((𝐷)‘𝑍) ≤ 𝑤, ((𝐷)‘𝑍), 𝑤)))))} = {𝑧 ∈ ((𝐴𝑍)[,](𝐵𝑍)) ∣ (𝑧 − (𝐴𝑍)) ≤ (Σ^‘(𝑖 ∈ ℕ ↦ (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍))‘𝑖)[,)if(((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖) ≤ 𝑧, ((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖), 𝑧)))))}
240 eqid 2621 . . . . . . 7 sup({𝑤 ∈ ((𝐴𝑍)[,](𝐵𝑍)) ∣ (𝑤 − (𝐴𝑍)) ≤ (Σ^‘( ∈ ℕ ↦ (vol‘(((𝐶)‘𝑍)[,)if(((𝐷)‘𝑍) ≤ 𝑤, ((𝐷)‘𝑍), 𝑤)))))}, ℝ, < ) = sup({𝑤 ∈ ((𝐴𝑍)[,](𝐵𝑍)) ∣ (𝑤 − (𝐴𝑍)) ≤ (Σ^‘( ∈ ℕ ↦ (vol‘(((𝐶)‘𝑍)[,)if(((𝐷)‘𝑍) ≤ 𝑤, ((𝐷)‘𝑍), 𝑤)))))}, ℝ, < )
24181, 82, 83, 86, 89, 191, 211, 239, 240hoidmv1lelem3 40576 . . . . . 6 (((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) ∈ ℝ) → ((𝐵𝑍) − (𝐴𝑍)) ≤ (Σ^‘(𝑖 ∈ ℕ ↦ (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍))‘𝑖)[,)((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖))))))
242241, 209breqtrd 4677 . . . . 5 (((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) ∈ ℝ) → ((𝐵𝑍) − (𝐴𝑍)) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))))
24321, 80, 242syl2anc 693 . . . 4 (((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) ∧ ¬ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) = +∞) → ((𝐵𝑍) − (𝐴𝑍)) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))))
24420, 243pm2.61dan 832 . . 3 ((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) → ((𝐵𝑍) − (𝐴𝑍)) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))))
24525, 29, 32, 8, 1hoidmvn0val 40567 . . . . . . 7 (𝜑 → (𝐴(𝐿𝑋)𝐵) = ∏𝑘𝑋 (vol‘((𝐴𝑘)[,)(𝐵𝑘))))
24626prodeq1d 14645 . . . . . . 7 (𝜑 → ∏𝑘𝑋 (vol‘((𝐴𝑘)[,)(𝐵𝑘))) = ∏𝑘 ∈ {𝑍} (vol‘((𝐴𝑘)[,)(𝐵𝑘))))
247 volicore 40564 . . . . . . . . . 10 (((𝐴𝑍) ∈ ℝ ∧ (𝐵𝑍) ∈ ℝ) → (vol‘((𝐴𝑍)[,)(𝐵𝑍))) ∈ ℝ)
2489, 7, 247syl2anc 693 . . . . . . . . 9 (𝜑 → (vol‘((𝐴𝑍)[,)(𝐵𝑍))) ∈ ℝ)
249248recnd 10065 . . . . . . . 8 (𝜑 → (vol‘((𝐴𝑍)[,)(𝐵𝑍))) ∈ ℂ)
250119, 121oveq12d 6665 . . . . . . . . . 10 (𝑘 = 𝑍 → ((𝐴𝑘)[,)(𝐵𝑘)) = ((𝐴𝑍)[,)(𝐵𝑍)))
251250fveq2d 6193 . . . . . . . . 9 (𝑘 = 𝑍 → (vol‘((𝐴𝑘)[,)(𝐵𝑘))) = (vol‘((𝐴𝑍)[,)(𝐵𝑍))))
252251prodsn 14686 . . . . . . . 8 ((𝑍𝑉 ∧ (vol‘((𝐴𝑍)[,)(𝐵𝑍))) ∈ ℂ) → ∏𝑘 ∈ {𝑍} (vol‘((𝐴𝑘)[,)(𝐵𝑘))) = (vol‘((𝐴𝑍)[,)(𝐵𝑍))))
2532, 249, 252syl2anc 693 . . . . . . 7 (𝜑 → ∏𝑘 ∈ {𝑍} (vol‘((𝐴𝑘)[,)(𝐵𝑘))) = (vol‘((𝐴𝑍)[,)(𝐵𝑍))))
254245, 246, 2533eqtrd 2659 . . . . . 6 (𝜑 → (𝐴(𝐿𝑋)𝐵) = (vol‘((𝐴𝑍)[,)(𝐵𝑍))))
255254adantr 481 . . . . 5 ((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) → (𝐴(𝐿𝑋)𝐵) = (vol‘((𝐴𝑍)[,)(𝐵𝑍))))
256 volico 39969 . . . . . . 7 (((𝐴𝑍) ∈ ℝ ∧ (𝐵𝑍) ∈ ℝ) → (vol‘((𝐴𝑍)[,)(𝐵𝑍))) = if((𝐴𝑍) < (𝐵𝑍), ((𝐵𝑍) − (𝐴𝑍)), 0))
2579, 7, 256syl2anc 693 . . . . . 6 (𝜑 → (vol‘((𝐴𝑍)[,)(𝐵𝑍))) = if((𝐴𝑍) < (𝐵𝑍), ((𝐵𝑍) − (𝐴𝑍)), 0))
258257adantr 481 . . . . 5 ((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) → (vol‘((𝐴𝑍)[,)(𝐵𝑍))) = if((𝐴𝑍) < (𝐵𝑍), ((𝐵𝑍) − (𝐴𝑍)), 0))
259 iftrue 4090 . . . . . 6 ((𝐴𝑍) < (𝐵𝑍) → if((𝐴𝑍) < (𝐵𝑍), ((𝐵𝑍) − (𝐴𝑍)), 0) = ((𝐵𝑍) − (𝐴𝑍)))
260259adantl 482 . . . . 5 ((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) → if((𝐴𝑍) < (𝐵𝑍), ((𝐵𝑍) − (𝐴𝑍)), 0) = ((𝐵𝑍) − (𝐴𝑍)))
261255, 258, 2603eqtrd 2659 . . . 4 ((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) → (𝐴(𝐿𝑋)𝐵) = ((𝐵𝑍) − (𝐴𝑍)))
26259fveq2d 6193 . . . . 5 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗)))) = (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))))
263262adantr 481 . . . 4 ((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗)))) = (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))))
264261, 263breq12d 4664 . . 3 ((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) → ((𝐴(𝐿𝑋)𝐵) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗)))) ↔ ((𝐵𝑍) − (𝐴𝑍)) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))))))
265244, 264mpbird 247 . 2 ((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) → (𝐴(𝐿𝑋)𝐵) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗)))))
266245adantr 481 . . . 4 ((𝜑 ∧ ¬ (𝐴𝑍) < (𝐵𝑍)) → (𝐴(𝐿𝑋)𝐵) = ∏𝑘𝑋 (vol‘((𝐴𝑘)[,)(𝐵𝑘))))
267246adantr 481 . . . 4 ((𝜑 ∧ ¬ (𝐴𝑍) < (𝐵𝑍)) → ∏𝑘𝑋 (vol‘((𝐴𝑘)[,)(𝐵𝑘))) = ∏𝑘 ∈ {𝑍} (vol‘((𝐴𝑘)[,)(𝐵𝑘))))
268253adantr 481 . . . . 5 ((𝜑 ∧ ¬ (𝐴𝑍) < (𝐵𝑍)) → ∏𝑘 ∈ {𝑍} (vol‘((𝐴𝑘)[,)(𝐵𝑘))) = (vol‘((𝐴𝑍)[,)(𝐵𝑍))))
269257adantr 481 . . . . 5 ((𝜑 ∧ ¬ (𝐴𝑍) < (𝐵𝑍)) → (vol‘((𝐴𝑍)[,)(𝐵𝑍))) = if((𝐴𝑍) < (𝐵𝑍), ((𝐵𝑍) − (𝐴𝑍)), 0))
270 iffalse 4093 . . . . . 6 (¬ (𝐴𝑍) < (𝐵𝑍) → if((𝐴𝑍) < (𝐵𝑍), ((𝐵𝑍) − (𝐴𝑍)), 0) = 0)
271270adantl 482 . . . . 5 ((𝜑 ∧ ¬ (𝐴𝑍) < (𝐵𝑍)) → if((𝐴𝑍) < (𝐵𝑍), ((𝐵𝑍) − (𝐴𝑍)), 0) = 0)
272268, 269, 2713eqtrd 2659 . . . 4 ((𝜑 ∧ ¬ (𝐴𝑍) < (𝐵𝑍)) → ∏𝑘 ∈ {𝑍} (vol‘((𝐴𝑘)[,)(𝐵𝑘))) = 0)
273266, 267, 2723eqtrd 2659 . . 3 ((𝜑 ∧ ¬ (𝐴𝑍) < (𝐵𝑍)) → (𝐴(𝐿𝑋)𝐵) = 0)
27423a1i 11 . . . . 5 (𝜑 → ℕ ∈ V)
275274, 76sge0ge0 40370 . . . 4 (𝜑 → 0 ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗)))))
276275adantr 481 . . 3 ((𝜑 ∧ ¬ (𝐴𝑍) < (𝐵𝑍)) → 0 ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗)))))
277273, 276eqbrtrd 4673 . 2 ((𝜑 ∧ ¬ (𝐴𝑍) < (𝐵𝑍)) → (𝐴(𝐿𝑋)𝐵) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗)))))
278265, 277pm2.61dan 832 1 (𝜑 → (𝐴(𝐿𝑋)𝐵) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗)))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 384  w3a 1037   = wceq 1482  wcel 1989  wne 2793  wral 2911  wrex 2912  {crab 2915  Vcvv 3198  wss 3572  c0 3913  ifcif 4084  {csn 4175  cop 4181   ciun 4518   class class class wbr 4651  cmpt 4727  wf 5882  cfv 5886  (class class class)co 6647  cmpt2 6649  𝑚 cmap 7854  Xcixp 7905  Fincfn 7952  supcsup 8343  cc 9931  cr 9932  0cc0 9933  +∞cpnf 10068  *cxr 10070   < clt 10071  cle 10072  cmin 10263  cn 11017  [,)cico 12174  [,]cicc 12175  cprod 14629  volcvol 23226  Σ^csumge0 40348
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1721  ax-4 1736  ax-5 1838  ax-6 1887  ax-7 1934  ax-8 1991  ax-9 1998  ax-10 2018  ax-11 2033  ax-12 2046  ax-13 2245  ax-ext 2601  ax-rep 4769  ax-sep 4779  ax-nul 4787  ax-pow 4841  ax-pr 4904  ax-un 6946  ax-inf2 8535  ax-cnex 9989  ax-resscn 9990  ax-1cn 9991  ax-icn 9992  ax-addcl 9993  ax-addrcl 9994  ax-mulcl 9995  ax-mulrcl 9996  ax-mulcom 9997  ax-addass 9998  ax-mulass 9999  ax-distr 10000  ax-i2m1 10001  ax-1ne0 10002  ax-1rid 10003  ax-rnegex 10004  ax-rrecex 10005  ax-cnre 10006  ax-pre-lttri 10007  ax-pre-lttrn 10008  ax-pre-ltadd 10009  ax-pre-mulgt0 10010  ax-pre-sup 10011
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1485  df-fal 1488  df-ex 1704  df-nf 1709  df-sb 1880  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2752  df-ne 2794  df-nel 2897  df-ral 2916  df-rex 2917  df-reu 2918  df-rmo 2919  df-rab 2920  df-v 3200  df-sbc 3434  df-csb 3532  df-dif 3575  df-un 3577  df-in 3579  df-ss 3586  df-pss 3588  df-nul 3914  df-if 4085  df-pw 4158  df-sn 4176  df-pr 4178  df-tp 4180  df-op 4182  df-uni 4435  df-int 4474  df-iun 4520  df-br 4652  df-opab 4711  df-mpt 4728  df-tr 4751  df-id 5022  df-eprel 5027  df-po 5033  df-so 5034  df-fr 5071  df-se 5072  df-we 5073  df-xp 5118  df-rel 5119  df-cnv 5120  df-co 5121  df-dm 5122  df-rn 5123  df-res 5124  df-ima 5125  df-pred 5678  df-ord 5724  df-on 5725  df-lim 5726  df-suc 5727  df-iota 5849  df-fun 5888  df-fn 5889  df-f 5890  df-f1 5891  df-fo 5892  df-f1o 5893  df-fv 5894  df-isom 5895  df-riota 6608  df-ov 6650  df-oprab 6651  df-mpt2 6652  df-of 6894  df-om 7063  df-1st 7165  df-2nd 7166  df-wrecs 7404  df-recs 7465  df-rdg 7503  df-1o 7557  df-2o 7558  df-oadd 7561  df-er 7739  df-map 7856  df-pm 7857  df-ixp 7906  df-en 7953  df-dom 7954  df-sdom 7955  df-fin 7956  df-fi 8314  df-sup 8345  df-inf 8346  df-oi 8412  df-card 8762  df-cda 8987  df-pnf 10073  df-mnf 10074  df-xr 10075  df-ltxr 10076  df-le 10077  df-sub 10265  df-neg 10266  df-div 10682  df-nn 11018  df-2 11076  df-3 11077  df-n0 11290  df-z 11375  df-uz 11685  df-q 11786  df-rp 11830  df-xneg 11943  df-xadd 11944  df-xmul 11945  df-ioo 12176  df-ico 12178  df-icc 12179  df-fz 12324  df-fzo 12462  df-fl 12588  df-seq 12797  df-exp 12856  df-hash 13113  df-cj 13833  df-re 13834  df-im 13835  df-sqrt 13969  df-abs 13970  df-clim 14213  df-rlim 14214  df-sum 14411  df-prod 14630  df-rest 16077  df-topgen 16098  df-psmet 19732  df-xmet 19733  df-met 19734  df-bl 19735  df-mopn 19736  df-top 20693  df-topon 20710  df-bases 20744  df-cmp 21184  df-ovol 23227  df-vol 23228  df-sumge0 40349
This theorem is referenced by:  hoidmvle  40583
  Copyright terms: Public domain W3C validator