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 42761
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 ↦ (𝑎 ∈ (ℝ ↑m 𝑥), 𝑏 ∈ (ℝ ↑m 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘𝑥 (vol‘((𝑎𝑘)[,)(𝑏𝑘))))))
hoidmv1le.z (𝜑𝑍𝑉)
hoidmv1le.x 𝑋 = {𝑍}
hoidmv1le.a (𝜑𝐴:𝑋⟶ℝ)
hoidmv1le.b (𝜑𝐵:𝑋⟶ℝ)
hoidmv1le.c (𝜑𝐶:ℕ⟶(ℝ ↑m 𝑋))
hoidmv1le.d (𝜑𝐷:ℕ⟶(ℝ ↑m 𝑋))
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 4596 . . . . . . . . . . . 12 (𝑍𝑉𝑍 ∈ {𝑍})
42, 3syl 17 . . . . . . . . . . 11 (𝜑𝑍 ∈ {𝑍})
5 hoidmv1le.x . . . . . . . . . . 11 𝑋 = {𝑍}
64, 5syl6eleqr 2929 . . . . . . . . . 10 (𝜑𝑍𝑋)
71, 6ffvelrnd 6850 . . . . . . . . 9 (𝜑 → (𝐵𝑍) ∈ ℝ)
8 hoidmv1le.a . . . . . . . . . 10 (𝜑𝐴:𝑋⟶ℝ)
98, 6ffvelrnd 6850 . . . . . . . . 9 (𝜑 → (𝐴𝑍) ∈ ℝ)
107, 9resubcld 11062 . . . . . . . 8 (𝜑 → ((𝐵𝑍) − (𝐴𝑍)) ∈ ℝ)
1110rexrd 10685 . . . . . . 7 (𝜑 → ((𝐵𝑍) − (𝐴𝑍)) ∈ ℝ*)
12 pnfxr 10689 . . . . . . . 8 +∞ ∈ ℝ*
1312a1i 11 . . . . . . 7 (𝜑 → +∞ ∈ ℝ*)
1410ltpnfd 12511 . . . . . . 7 (𝜑 → ((𝐵𝑍) − (𝐴𝑍)) < +∞)
1511, 13, 14xrltled 12538 . . . . . 6 (𝜑 → ((𝐵𝑍) − (𝐴𝑍)) ≤ +∞)
1615ad2antrr 722 . . . . 5 (((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) = +∞) → ((𝐵𝑍) − (𝐴𝑍)) ≤ +∞)
17 id 22 . . . . . . 7 ((Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) = +∞ → (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) = +∞)
1817eqcomd 2832 . . . . . 6 ((Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) = +∞ → +∞ = (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))))
1918adantl 482 . . . . 5 (((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) = +∞) → +∞ = (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))))
2016, 19breqtrd 5089 . . . 4 (((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) = +∞) → ((𝐵𝑍) − (𝐴𝑍)) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))))
21 simpl 483 . . . . 5 (((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) ∧ ¬ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) = +∞) → (𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)))
22 simpr 485 . . . . . 6 (((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) ∧ ¬ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) = +∞) → ¬ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) = +∞)
23 nnex 11638 . . . . . . . 8 ℕ ∈ V
2423a1i 11 . . . . . . 7 (((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) ∧ ¬ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) = +∞) → ℕ ∈ V)
25 hoidmv1le.l . . . . . . . . . . . 12 𝐿 = (𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑m 𝑥), 𝑏 ∈ (ℝ ↑m 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘𝑥 (vol‘((𝑎𝑘)[,)(𝑏𝑘))))))
265a1i 11 . . . . . . . . . . . . . 14 (𝜑𝑋 = {𝑍})
27 snfi 8588 . . . . . . . . . . . . . . 15 {𝑍} ∈ Fin
2827a1i 11 . . . . . . . . . . . . . 14 (𝜑 → {𝑍} ∈ Fin)
2926, 28eqeltrd 2918 . . . . . . . . . . . . 13 (𝜑𝑋 ∈ Fin)
3029adantr 481 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ) → 𝑋 ∈ Fin)
316ne0d 4305 . . . . . . . . . . . . 13 (𝜑𝑋 ≠ ∅)
3231adantr 481 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ) → 𝑋 ≠ ∅)
33 hoidmv1le.c . . . . . . . . . . . . . 14 (𝜑𝐶:ℕ⟶(ℝ ↑m 𝑋))
3433ffvelrnda 6849 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ ℕ) → (𝐶𝑗) ∈ (ℝ ↑m 𝑋))
35 elmapi 8423 . . . . . . . . . . . . 13 ((𝐶𝑗) ∈ (ℝ ↑m 𝑋) → (𝐶𝑗):𝑋⟶ℝ)
3634, 35syl 17 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ) → (𝐶𝑗):𝑋⟶ℝ)
37 hoidmv1le.d . . . . . . . . . . . . . 14 (𝜑𝐷:ℕ⟶(ℝ ↑m 𝑋))
3837ffvelrnda 6849 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ ℕ) → (𝐷𝑗) ∈ (ℝ ↑m 𝑋))
39 elmapi 8423 . . . . . . . . . . . . 13 ((𝐷𝑗) ∈ (ℝ ↑m 𝑋) → (𝐷𝑗):𝑋⟶ℝ)
4038, 39syl 17 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ) → (𝐷𝑗):𝑋⟶ℝ)
4125, 30, 32, 36, 40hoidmvn0val 42751 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗)) = ∏𝑘𝑋 (vol‘(((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))))
425prodeq1i 15267 . . . . . . . . . . . 12 𝑘𝑋 (vol‘(((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) = ∏𝑘 ∈ {𝑍} (vol‘(((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
4342a1i 11 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ℕ) → ∏𝑘𝑋 (vol‘(((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) = ∏𝑘 ∈ {𝑍} (vol‘(((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))))
442adantr 481 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ) → 𝑍𝑉)
456adantr 481 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ ℕ) → 𝑍𝑋)
4636, 45ffvelrnd 6850 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗)‘𝑍) ∈ ℝ)
4740, 45ffvelrnd 6850 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ ℕ) → ((𝐷𝑗)‘𝑍) ∈ ℝ)
48 volicore 42748 . . . . . . . . . . . . . 14 ((((𝐶𝑗)‘𝑍) ∈ ℝ ∧ ((𝐷𝑗)‘𝑍) ∈ ℝ) → (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))) ∈ ℝ)
4946, 47, 48syl2anc 584 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ ℕ) → (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))) ∈ ℝ)
5049recnd 10663 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ) → (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))) ∈ ℂ)
51 fveq2 6669 . . . . . . . . . . . . . . 15 (𝑘 = 𝑍 → ((𝐶𝑗)‘𝑘) = ((𝐶𝑗)‘𝑍))
52 fveq2 6669 . . . . . . . . . . . . . . 15 (𝑘 = 𝑍 → ((𝐷𝑗)‘𝑘) = ((𝐷𝑗)‘𝑍))
5351, 52oveq12d 7168 . . . . . . . . . . . . . 14 (𝑘 = 𝑍 → (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) = (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))
5453fveq2d 6673 . . . . . . . . . . . . 13 (𝑘 = 𝑍 → (vol‘(((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) = (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))
5554prodsn 15311 . . . . . . . . . . . 12 ((𝑍𝑉 ∧ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))) ∈ ℂ) → ∏𝑘 ∈ {𝑍} (vol‘(((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) = (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))
5644, 50, 55syl2anc 584 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ℕ) → ∏𝑘 ∈ {𝑍} (vol‘(((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) = (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))
5741, 43, 563eqtrd 2865 . . . . . . . . . 10 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗)) = (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))
5857mpteq2dva 5158 . . . . . . . . 9 (𝜑 → (𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗))) = (𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))))
59 fveq2 6669 . . . . . . . . . . . . . . . . . . . 20 (𝑘 = 𝑙 → (𝑎𝑘) = (𝑎𝑙))
60 fveq2 6669 . . . . . . . . . . . . . . . . . . . 20 (𝑘 = 𝑙 → (𝑏𝑘) = (𝑏𝑙))
6159, 60oveq12d 7168 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 𝑙 → ((𝑎𝑘)[,)(𝑏𝑘)) = ((𝑎𝑙)[,)(𝑏𝑙)))
6261fveq2d 6673 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑙 → (vol‘((𝑎𝑘)[,)(𝑏𝑘))) = (vol‘((𝑎𝑙)[,)(𝑏𝑙))))
6362cbvprodv 15265 . . . . . . . . . . . . . . . . 17 𝑘𝑥 (vol‘((𝑎𝑘)[,)(𝑏𝑘))) = ∏𝑙𝑥 (vol‘((𝑎𝑙)[,)(𝑏𝑙)))
64 ifeq2 4475 . . . . . . . . . . . . . . . . 17 (∏𝑘𝑥 (vol‘((𝑎𝑘)[,)(𝑏𝑘))) = ∏𝑙𝑥 (vol‘((𝑎𝑙)[,)(𝑏𝑙))) → if(𝑥 = ∅, 0, ∏𝑘𝑥 (vol‘((𝑎𝑘)[,)(𝑏𝑘)))) = if(𝑥 = ∅, 0, ∏𝑙𝑥 (vol‘((𝑎𝑙)[,)(𝑏𝑙)))))
6563, 64ax-mp 5 . . . . . . . . . . . . . . . 16 if(𝑥 = ∅, 0, ∏𝑘𝑥 (vol‘((𝑎𝑘)[,)(𝑏𝑘)))) = if(𝑥 = ∅, 0, ∏𝑙𝑥 (vol‘((𝑎𝑙)[,)(𝑏𝑙))))
6665a1i 11 . . . . . . . . . . . . . . 15 ((𝑎 ∈ (ℝ ↑m 𝑥) ∧ 𝑏 ∈ (ℝ ↑m 𝑥)) → if(𝑥 = ∅, 0, ∏𝑘𝑥 (vol‘((𝑎𝑘)[,)(𝑏𝑘)))) = if(𝑥 = ∅, 0, ∏𝑙𝑥 (vol‘((𝑎𝑙)[,)(𝑏𝑙)))))
6766mpoeq3ia 7226 . . . . . . . . . . . . . 14 (𝑎 ∈ (ℝ ↑m 𝑥), 𝑏 ∈ (ℝ ↑m 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘𝑥 (vol‘((𝑎𝑘)[,)(𝑏𝑘))))) = (𝑎 ∈ (ℝ ↑m 𝑥), 𝑏 ∈ (ℝ ↑m 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑙𝑥 (vol‘((𝑎𝑙)[,)(𝑏𝑙)))))
6867mpteq2i 5155 . . . . . . . . . . . . 13 (𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑m 𝑥), 𝑏 ∈ (ℝ ↑m 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘𝑥 (vol‘((𝑎𝑘)[,)(𝑏𝑘)))))) = (𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑m 𝑥), 𝑏 ∈ (ℝ ↑m 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑙𝑥 (vol‘((𝑎𝑙)[,)(𝑏𝑙))))))
6925, 68eqtri 2849 . . . . . . . . . . . 12 𝐿 = (𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑m 𝑥), 𝑏 ∈ (ℝ ↑m 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑙𝑥 (vol‘((𝑎𝑙)[,)(𝑏𝑙))))))
7069, 30, 36, 40hoidmvcl 42749 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗)) ∈ (0[,)+∞))
71 eqid 2826 . . . . . . . . . . 11 (𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗))) = (𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗)))
7270, 71fmptd 6876 . . . . . . . . . 10 (𝜑 → (𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗))):ℕ⟶(0[,)+∞))
73 icossicc 12819 . . . . . . . . . . 11 (0[,)+∞) ⊆ (0[,]+∞)
7473a1i 11 . . . . . . . . . 10 (𝜑 → (0[,)+∞) ⊆ (0[,]+∞))
7572, 74fssd 6527 . . . . . . . . 9 (𝜑 → (𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗))):ℕ⟶(0[,]+∞))
7658, 75feq1dd 41307 . . . . . . . 8 (𝜑 → (𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))):ℕ⟶(0[,]+∞))
7776ad2antrr 722 . . . . . . 7 (((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) ∧ ¬ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) = +∞) → (𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))):ℕ⟶(0[,]+∞))
7824, 77sge0repnf 42553 . . . . . 6 (((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) ∧ ¬ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) = +∞) → ((Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) ∈ ℝ ↔ ¬ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) = +∞))
7922, 78mpbird 258 . . . . 5 (((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) ∧ ¬ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) = +∞) → (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) ∈ ℝ)
809ad2antrr 722 . . . . . . 7 (((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) ∈ ℝ) → (𝐴𝑍) ∈ ℝ)
817ad2antrr 722 . . . . . . 7 (((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) ∈ ℝ) → (𝐵𝑍) ∈ ℝ)
82 simplr 765 . . . . . . 7 (((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) ∈ ℝ) → (𝐴𝑍) < (𝐵𝑍))
83 eqid 2826 . . . . . . . . 9 (𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍)) = (𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍))
8446, 83fmptd 6876 . . . . . . . 8 (𝜑 → (𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍)):ℕ⟶ℝ)
8584ad2antrr 722 . . . . . . 7 (((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) ∈ ℝ) → (𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍)):ℕ⟶ℝ)
86 eqid 2826 . . . . . . . . 9 (𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍)) = (𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))
8747, 86fmptd 6876 . . . . . . . 8 (𝜑 → (𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍)):ℕ⟶ℝ)
8887ad2antrr 722 . . . . . . 7 (((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) ∈ ℝ) → (𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍)):ℕ⟶ℝ)
89 hoidmv1le.s . . . . . . . . . . . . . . . . 17 (𝜑X𝑘𝑋 ((𝐴𝑘)[,)(𝐵𝑘)) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
905eleq2i 2909 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑘𝑋𝑘 ∈ {𝑍})
9190biimpi 217 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑘𝑋𝑘 ∈ {𝑍})
92 elsni 4581 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑘 ∈ {𝑍} → 𝑘 = 𝑍)
9391, 92syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑘𝑋𝑘 = 𝑍)
9493, 53syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘𝑋 → (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) = (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))
9594rgen 3153 . . . . . . . . . . . . . . . . . . . . 21 𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) = (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))
96 ixpeq2 8469 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) = (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) → X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) = X𝑘𝑋 (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))
9795, 96ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) = X𝑘𝑋 (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))
9897a1i 11 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ ℕ → X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) = X𝑘𝑋 (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))
9998iuneq2i 4937 . . . . . . . . . . . . . . . . . 18 𝑗 ∈ ℕ X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) = 𝑗 ∈ ℕ X𝑘𝑋 (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))
10099a1i 11 . . . . . . . . . . . . . . . . 17 (𝜑 𝑗 ∈ ℕ X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) = 𝑗 ∈ ℕ X𝑘𝑋 (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))
10189, 100sseqtrd 4011 . . . . . . . . . . . . . . . 16 (𝜑X𝑘𝑋 ((𝐴𝑘)[,)(𝐵𝑘)) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))
102101adantr 481 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ ((𝐴𝑍)[,)(𝐵𝑍))) → X𝑘𝑋 ((𝐴𝑘)[,)(𝐵𝑘)) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))
103 id 22 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ((𝐴𝑍)[,)(𝐵𝑍)) → 𝑥 ∈ ((𝐴𝑍)[,)(𝐵𝑍)))
104 eqidd 2827 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ((𝐴𝑍)[,)(𝐵𝑍)) → {⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑥⟩})
105 opeq2 4803 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 = 𝑥 → ⟨𝑍, 𝑦⟩ = ⟨𝑍, 𝑥⟩)
106105sneqd 4576 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = 𝑥 → {⟨𝑍, 𝑦⟩} = {⟨𝑍, 𝑥⟩})
107106rspceeqv 3642 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ∈ ((𝐴𝑍)[,)(𝐵𝑍)) ∧ {⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑥⟩}) → ∃𝑦 ∈ ((𝐴𝑍)[,)(𝐵𝑍)){⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩})
108103, 104, 107syl2anc 584 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ((𝐴𝑍)[,)(𝐵𝑍)) → ∃𝑦 ∈ ((𝐴𝑍)[,)(𝐵𝑍)){⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩})
109108adantl 482 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ ((𝐴𝑍)[,)(𝐵𝑍))) → ∃𝑦 ∈ ((𝐴𝑍)[,)(𝐵𝑍)){⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩})
110 elixpsn 8495 . . . . . . . . . . . . . . . . . . 19 (𝑍𝑉 → ({⟨𝑍, 𝑥⟩} ∈ X𝑘 ∈ {𝑍} ((𝐴𝑍)[,)(𝐵𝑍)) ↔ ∃𝑦 ∈ ((𝐴𝑍)[,)(𝐵𝑍)){⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩}))
1112, 110syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑 → ({⟨𝑍, 𝑥⟩} ∈ X𝑘 ∈ {𝑍} ((𝐴𝑍)[,)(𝐵𝑍)) ↔ ∃𝑦 ∈ ((𝐴𝑍)[,)(𝐵𝑍)){⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩}))
112111adantr 481 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ ((𝐴𝑍)[,)(𝐵𝑍))) → ({⟨𝑍, 𝑥⟩} ∈ X𝑘 ∈ {𝑍} ((𝐴𝑍)[,)(𝐵𝑍)) ↔ ∃𝑦 ∈ ((𝐴𝑍)[,)(𝐵𝑍)){⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩}))
113109, 112mpbird 258 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ ((𝐴𝑍)[,)(𝐵𝑍))) → {⟨𝑍, 𝑥⟩} ∈ X𝑘 ∈ {𝑍} ((𝐴𝑍)[,)(𝐵𝑍)))
1145eqcomi 2835 . . . . . . . . . . . . . . . . . . . 20 {𝑍} = 𝑋
115 ixpeq1 8466 . . . . . . . . . . . . . . . . . . . 20 ({𝑍} = 𝑋X𝑘 ∈ {𝑍} ((𝐴𝑍)[,)(𝐵𝑍)) = X𝑘𝑋 ((𝐴𝑍)[,)(𝐵𝑍)))
116114, 115ax-mp 5 . . . . . . . . . . . . . . . . . . 19 X𝑘 ∈ {𝑍} ((𝐴𝑍)[,)(𝐵𝑍)) = X𝑘𝑋 ((𝐴𝑍)[,)(𝐵𝑍))
117 fveq2 6669 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑘 = 𝑍 → (𝐴𝑘) = (𝐴𝑍))
11893, 117syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑘𝑋 → (𝐴𝑘) = (𝐴𝑍))
119 fveq2 6669 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑘 = 𝑍 → (𝐵𝑘) = (𝐵𝑍))
12093, 119syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑘𝑋 → (𝐵𝑘) = (𝐵𝑍))
121118, 120oveq12d 7168 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘𝑋 → ((𝐴𝑘)[,)(𝐵𝑘)) = ((𝐴𝑍)[,)(𝐵𝑍)))
122121eqcomd 2832 . . . . . . . . . . . . . . . . . . . . 21 (𝑘𝑋 → ((𝐴𝑍)[,)(𝐵𝑍)) = ((𝐴𝑘)[,)(𝐵𝑘)))
123122rgen 3153 . . . . . . . . . . . . . . . . . . . 20 𝑘𝑋 ((𝐴𝑍)[,)(𝐵𝑍)) = ((𝐴𝑘)[,)(𝐵𝑘))
124 ixpeq2 8469 . . . . . . . . . . . . . . . . . . . 20 (∀𝑘𝑋 ((𝐴𝑍)[,)(𝐵𝑍)) = ((𝐴𝑘)[,)(𝐵𝑘)) → X𝑘𝑋 ((𝐴𝑍)[,)(𝐵𝑍)) = X𝑘𝑋 ((𝐴𝑘)[,)(𝐵𝑘)))
125123, 124ax-mp 5 . . . . . . . . . . . . . . . . . . 19 X𝑘𝑋 ((𝐴𝑍)[,)(𝐵𝑍)) = X𝑘𝑋 ((𝐴𝑘)[,)(𝐵𝑘))
126116, 125eqtri 2849 . . . . . . . . . . . . . . . . . 18 X𝑘 ∈ {𝑍} ((𝐴𝑍)[,)(𝐵𝑍)) = X𝑘𝑋 ((𝐴𝑘)[,)(𝐵𝑘))
127126a1i 11 . . . . . . . . . . . . . . . . 17 (𝜑X𝑘 ∈ {𝑍} ((𝐴𝑍)[,)(𝐵𝑍)) = X𝑘𝑋 ((𝐴𝑘)[,)(𝐵𝑘)))
128127adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ ((𝐴𝑍)[,)(𝐵𝑍))) → X𝑘 ∈ {𝑍} ((𝐴𝑍)[,)(𝐵𝑍)) = X𝑘𝑋 ((𝐴𝑘)[,)(𝐵𝑘)))
129113, 128eleqtrd 2920 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ ((𝐴𝑍)[,)(𝐵𝑍))) → {⟨𝑍, 𝑥⟩} ∈ X𝑘𝑋 ((𝐴𝑘)[,)(𝐵𝑘)))
130102, 129sseldd 3972 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ ((𝐴𝑍)[,)(𝐵𝑍))) → {⟨𝑍, 𝑥⟩} ∈ 𝑗 ∈ ℕ X𝑘𝑋 (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))
131 eliun 4921 . . . . . . . . . . . . . 14 ({⟨𝑍, 𝑥⟩} ∈ 𝑗 ∈ ℕ X𝑘𝑋 (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) ↔ ∃𝑗 ∈ ℕ {⟨𝑍, 𝑥⟩} ∈ X𝑘𝑋 (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))
132130, 131sylib 219 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ ((𝐴𝑍)[,)(𝐵𝑍))) → ∃𝑗 ∈ ℕ {⟨𝑍, 𝑥⟩} ∈ X𝑘𝑋 (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))
133 ixpeq1 8466 . . . . . . . . . . . . . . . . . . . . . 22 (𝑋 = {𝑍} → X𝑘𝑋 (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) = X𝑘 ∈ {𝑍} (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))
1345, 133ax-mp 5 . . . . . . . . . . . . . . . . . . . . 21 X𝑘𝑋 (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) = X𝑘 ∈ {𝑍} (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))
135134eleq2i 2909 . . . . . . . . . . . . . . . . . . . 20 ({⟨𝑍, 𝑥⟩} ∈ X𝑘𝑋 (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) ↔ {⟨𝑍, 𝑥⟩} ∈ X𝑘 ∈ {𝑍} (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))
136135biimpi 217 . . . . . . . . . . . . . . . . . . 19 ({⟨𝑍, 𝑥⟩} ∈ X𝑘𝑋 (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) → {⟨𝑍, 𝑥⟩} ∈ X𝑘 ∈ {𝑍} (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))
137136adantl 482 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ {⟨𝑍, 𝑥⟩} ∈ X𝑘𝑋 (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))) → {⟨𝑍, 𝑥⟩} ∈ X𝑘 ∈ {𝑍} (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))
138 elixpsn 8495 . . . . . . . . . . . . . . . . . . . 20 (𝑍𝑉 → ({⟨𝑍, 𝑥⟩} ∈ X𝑘 ∈ {𝑍} (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) ↔ ∃𝑦 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)){⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩}))
1392, 138syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ({⟨𝑍, 𝑥⟩} ∈ X𝑘 ∈ {𝑍} (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) ↔ ∃𝑦 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)){⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩}))
140139adantr 481 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ {⟨𝑍, 𝑥⟩} ∈ X𝑘𝑋 (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))) → ({⟨𝑍, 𝑥⟩} ∈ X𝑘 ∈ {𝑍} (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) ↔ ∃𝑦 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)){⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩}))
141137, 140mpbid 233 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ {⟨𝑍, 𝑥⟩} ∈ X𝑘𝑋 (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))) → ∃𝑦 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)){⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩})
142 opex 5353 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑍, 𝑥⟩ ∈ V
143142sneqr 4770 . . . . . . . . . . . . . . . . . . . . . . . . 25 ({⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩} → ⟨𝑍, 𝑥⟩ = ⟨𝑍, 𝑦⟩)
144143adantl 482 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ {⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩}) → ⟨𝑍, 𝑥⟩ = ⟨𝑍, 𝑦⟩)
145 vex 3503 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝑥 ∈ V
146145a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑𝑥 ∈ V)
147 opthg 5366 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑍𝑉𝑥 ∈ V) → (⟨𝑍, 𝑥⟩ = ⟨𝑍, 𝑦⟩ ↔ (𝑍 = 𝑍𝑥 = 𝑦)))
1482, 146, 147syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (⟨𝑍, 𝑥⟩ = ⟨𝑍, 𝑦⟩ ↔ (𝑍 = 𝑍𝑥 = 𝑦)))
149148adantr 481 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ {⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩}) → (⟨𝑍, 𝑥⟩ = ⟨𝑍, 𝑦⟩ ↔ (𝑍 = 𝑍𝑥 = 𝑦)))
150144, 149mpbid 233 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ {⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩}) → (𝑍 = 𝑍𝑥 = 𝑦))
151150simprd 496 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ {⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩}) → 𝑥 = 𝑦)
1521513adant2 1125 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑦 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) ∧ {⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩}) → 𝑥 = 𝑦)
153 simp2 1131 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑦 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) ∧ {⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩}) → 𝑦 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))
154152, 153eqeltrd 2918 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑦 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) ∧ {⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩}) → 𝑥 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))
1551543exp 1113 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑦 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) → ({⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩} → 𝑥 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))))
156155adantr 481 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ {⟨𝑍, 𝑥⟩} ∈ X𝑘𝑋 (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))) → (𝑦 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) → ({⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩} → 𝑥 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))))
157156rexlimdv 3288 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ {⟨𝑍, 𝑥⟩} ∈ X𝑘𝑋 (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))) → (∃𝑦 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)){⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩} → 𝑥 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))
158141, 157mpd 15 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ {⟨𝑍, 𝑥⟩} ∈ X𝑘𝑋 (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))) → 𝑥 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))
159158ex 413 . . . . . . . . . . . . . . 15 (𝜑 → ({⟨𝑍, 𝑥⟩} ∈ X𝑘𝑋 (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) → 𝑥 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))
160159ad2antrr 722 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ ((𝐴𝑍)[,)(𝐵𝑍))) ∧ 𝑗 ∈ ℕ) → ({⟨𝑍, 𝑥⟩} ∈ X𝑘𝑋 (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) → 𝑥 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))
161160reximdva 3279 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ ((𝐴𝑍)[,)(𝐵𝑍))) → (∃𝑗 ∈ ℕ {⟨𝑍, 𝑥⟩} ∈ X𝑘𝑋 (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) → ∃𝑗 ∈ ℕ 𝑥 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))
162132, 161mpd 15 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ ((𝐴𝑍)[,)(𝐵𝑍))) → ∃𝑗 ∈ ℕ 𝑥 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))
163 eliun 4921 . . . . . . . . . . . 12 (𝑥 𝑗 ∈ ℕ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) ↔ ∃𝑗 ∈ ℕ 𝑥 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))
164162, 163sylibr 235 . . . . . . . . . . 11 ((𝜑𝑥 ∈ ((𝐴𝑍)[,)(𝐵𝑍))) → 𝑥 𝑗 ∈ ℕ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))
165164ralrimiva 3187 . . . . . . . . . 10 (𝜑 → ∀𝑥 ∈ ((𝐴𝑍)[,)(𝐵𝑍))𝑥 𝑗 ∈ ℕ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))
166 dfss3 3960 . . . . . . . . . 10 (((𝐴𝑍)[,)(𝐵𝑍)) ⊆ 𝑗 ∈ ℕ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) ↔ ∀𝑥 ∈ ((𝐴𝑍)[,)(𝐵𝑍))𝑥 𝑗 ∈ ℕ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))
167165, 166sylibr 235 . . . . . . . . 9 (𝜑 → ((𝐴𝑍)[,)(𝐵𝑍)) ⊆ 𝑗 ∈ ℕ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))
168 eqidd 2827 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ ℕ) → (𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍)) = (𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍)))
169 fveq2 6669 . . . . . . . . . . . . . . 15 (𝑗 = 𝑖 → (𝐶𝑗) = (𝐶𝑖))
170169fveq1d 6671 . . . . . . . . . . . . . 14 (𝑗 = 𝑖 → ((𝐶𝑗)‘𝑍) = ((𝐶𝑖)‘𝑍))
171170adantl 482 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ ℕ) ∧ 𝑗 = 𝑖) → ((𝐶𝑗)‘𝑍) = ((𝐶𝑖)‘𝑍))
172 simpr 485 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ ℕ) → 𝑖 ∈ ℕ)
173 fvexd 6684 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ ℕ) → ((𝐶𝑖)‘𝑍) ∈ V)
174168, 171, 172, 173fvmptd 6773 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ ℕ) → ((𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍))‘𝑖) = ((𝐶𝑖)‘𝑍))
175 eqidd 2827 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ ℕ) → (𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍)) = (𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍)))
176 fveq2 6669 . . . . . . . . . . . . . . 15 (𝑗 = 𝑖 → (𝐷𝑗) = (𝐷𝑖))
177176fveq1d 6671 . . . . . . . . . . . . . 14 (𝑗 = 𝑖 → ((𝐷𝑗)‘𝑍) = ((𝐷𝑖)‘𝑍))
178177adantl 482 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ ℕ) ∧ 𝑗 = 𝑖) → ((𝐷𝑗)‘𝑍) = ((𝐷𝑖)‘𝑍))
179 fvexd 6684 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ ℕ) → ((𝐷𝑖)‘𝑍) ∈ V)
180175, 178, 172, 179fvmptd 6773 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ ℕ) → ((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖) = ((𝐷𝑖)‘𝑍))
181174, 180oveq12d 7168 . . . . . . . . . . 11 ((𝜑𝑖 ∈ ℕ) → (((𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍))‘𝑖)[,)((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖)) = (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)))
182181iuneq2dv 4940 . . . . . . . . . 10 (𝜑 𝑖 ∈ ℕ (((𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍))‘𝑖)[,)((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖)) = 𝑖 ∈ ℕ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)))
183170, 177oveq12d 7168 . . . . . . . . . . . . 13 (𝑗 = 𝑖 → (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) = (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)))
184183cbviunv 4962 . . . . . . . . . . . 12 𝑗 ∈ ℕ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) = 𝑖 ∈ ℕ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍))
185184eqcomi 2835 . . . . . . . . . . 11 𝑖 ∈ ℕ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)) = 𝑗 ∈ ℕ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))
186185a1i 11 . . . . . . . . . 10 (𝜑 𝑖 ∈ ℕ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)) = 𝑗 ∈ ℕ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))
187182, 186eqtr2d 2862 . . . . . . . . 9 (𝜑 𝑗 ∈ ℕ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) = 𝑖 ∈ ℕ (((𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍))‘𝑖)[,)((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖)))
188167, 187sseqtrd 4011 . . . . . . . 8 (𝜑 → ((𝐴𝑍)[,)(𝐵𝑍)) ⊆ 𝑖 ∈ ℕ (((𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍))‘𝑖)[,)((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖)))
189188ad2antrr 722 . . . . . . 7 (((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) ∈ ℝ) → ((𝐴𝑍)[,)(𝐵𝑍)) ⊆ 𝑖 ∈ ℕ (((𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍))‘𝑖)[,)((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖)))
190 fvex 6682 . . . . . . . . . . . . . . 15 ((𝐶𝑖)‘𝑍) ∈ V
191170, 83, 190fvmpt 6767 . . . . . . . . . . . . . 14 (𝑖 ∈ ℕ → ((𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍))‘𝑖) = ((𝐶𝑖)‘𝑍))
192 fvex 6682 . . . . . . . . . . . . . . 15 ((𝐷𝑖)‘𝑍) ∈ V
193177, 86, 192fvmpt 6767 . . . . . . . . . . . . . 14 (𝑖 ∈ ℕ → ((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖) = ((𝐷𝑖)‘𝑍))
194191, 193oveq12d 7168 . . . . . . . . . . . . 13 (𝑖 ∈ ℕ → (((𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍))‘𝑖)[,)((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖)) = (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)))
195194fveq2d 6673 . . . . . . . . . . . 12 (𝑖 ∈ ℕ → (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍))‘𝑖)[,)((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖))) = (vol‘(((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍))))
196195mpteq2ia 5154 . . . . . . . . . . 11 (𝑖 ∈ ℕ ↦ (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍))‘𝑖)[,)((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖)))) = (𝑖 ∈ ℕ ↦ (vol‘(((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍))))
197 eqcom 2833 . . . . . . . . . . . . . . . 16 (𝑗 = 𝑖𝑖 = 𝑗)
198197imbi1i 351 . . . . . . . . . . . . . . 15 ((𝑗 = 𝑖 → (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) = (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍))) ↔ (𝑖 = 𝑗 → (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) = (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍))))
199 eqcom 2833 . . . . . . . . . . . . . . . 16 ((((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) = (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)) ↔ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)) = (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))
200199imbi2i 337 . . . . . . . . . . . . . . 15 ((𝑖 = 𝑗 → (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) = (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍))) ↔ (𝑖 = 𝑗 → (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)) = (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))
201198, 200bitri 276 . . . . . . . . . . . . . 14 ((𝑗 = 𝑖 → (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) = (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍))) ↔ (𝑖 = 𝑗 → (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)) = (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))
202183, 201mpbi 231 . . . . . . . . . . . . 13 (𝑖 = 𝑗 → (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)) = (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))
203202fveq2d 6673 . . . . . . . . . . . 12 (𝑖 = 𝑗 → (vol‘(((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍))) = (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))
204203cbvmptv 5166 . . . . . . . . . . 11 (𝑖 ∈ ℕ ↦ (vol‘(((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)))) = (𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))
205196, 204eqtri 2849 . . . . . . . . . 10 (𝑖 ∈ ℕ ↦ (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍))‘𝑖)[,)((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖)))) = (𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))
206205fveq2i 6672 . . . . . . . . 9 ^‘(𝑖 ∈ ℕ ↦ (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍))‘𝑖)[,)((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖))))) = (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))))
207206a1i 11 . . . . . . . 8 (((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) ∈ ℝ) → (Σ^‘(𝑖 ∈ ℕ ↦ (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍))‘𝑖)[,)((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖))))) = (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))))
208 simpr 485 . . . . . . . 8 (((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) ∈ ℝ) → (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) ∈ ℝ)
209207, 208eqeltrd 2918 . . . . . . 7 (((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) ∈ ℝ) → (Σ^‘(𝑖 ∈ ℕ ↦ (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍))‘𝑖)[,)((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖))))) ∈ ℝ)
210 oveq1 7157 . . . . . . . . 9 (𝑤 = 𝑧 → (𝑤 − (𝐴𝑍)) = (𝑧 − (𝐴𝑍)))
211193breq1d 5073 . . . . . . . . . . . . . . . . 17 (𝑖 ∈ ℕ → (((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖) ≤ 𝑧 ↔ ((𝐷𝑖)‘𝑍) ≤ 𝑧))
212211, 193ifbieq1d 4493 . . . . . . . . . . . . . . . 16 (𝑖 ∈ ℕ → if(((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖) ≤ 𝑧, ((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖), 𝑧) = if(((𝐷𝑖)‘𝑍) ≤ 𝑧, ((𝐷𝑖)‘𝑍), 𝑧))
213191, 212oveq12d 7168 . . . . . . . . . . . . . . 15 (𝑖 ∈ ℕ → (((𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍))‘𝑖)[,)if(((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖) ≤ 𝑧, ((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖), 𝑧)) = (((𝐶𝑖)‘𝑍)[,)if(((𝐷𝑖)‘𝑍) ≤ 𝑧, ((𝐷𝑖)‘𝑍), 𝑧)))
214213fveq2d 6673 . . . . . . . . . . . . . 14 (𝑖 ∈ ℕ → (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍))‘𝑖)[,)if(((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖) ≤ 𝑧, ((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖), 𝑧))) = (vol‘(((𝐶𝑖)‘𝑍)[,)if(((𝐷𝑖)‘𝑍) ≤ 𝑧, ((𝐷𝑖)‘𝑍), 𝑧))))
215214mpteq2ia 5154 . . . . . . . . . . . . 13 (𝑖 ∈ ℕ ↦ (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍))‘𝑖)[,)if(((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖) ≤ 𝑧, ((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖), 𝑧)))) = (𝑖 ∈ ℕ ↦ (vol‘(((𝐶𝑖)‘𝑍)[,)if(((𝐷𝑖)‘𝑍) ≤ 𝑧, ((𝐷𝑖)‘𝑍), 𝑧))))
216 fveq2 6669 . . . . . . . . . . . . . . . . 17 (𝑖 = → (𝐶𝑖) = (𝐶))
217216fveq1d 6671 . . . . . . . . . . . . . . . 16 (𝑖 = → ((𝐶𝑖)‘𝑍) = ((𝐶)‘𝑍))
218 fveq2 6669 . . . . . . . . . . . . . . . . . . 19 (𝑖 = → (𝐷𝑖) = (𝐷))
219218fveq1d 6671 . . . . . . . . . . . . . . . . . 18 (𝑖 = → ((𝐷𝑖)‘𝑍) = ((𝐷)‘𝑍))
220219breq1d 5073 . . . . . . . . . . . . . . . . 17 (𝑖 = → (((𝐷𝑖)‘𝑍) ≤ 𝑧 ↔ ((𝐷)‘𝑍) ≤ 𝑧))
221220, 219ifbieq1d 4493 . . . . . . . . . . . . . . . 16 (𝑖 = → if(((𝐷𝑖)‘𝑍) ≤ 𝑧, ((𝐷𝑖)‘𝑍), 𝑧) = if(((𝐷)‘𝑍) ≤ 𝑧, ((𝐷)‘𝑍), 𝑧))
222217, 221oveq12d 7168 . . . . . . . . . . . . . . 15 (𝑖 = → (((𝐶𝑖)‘𝑍)[,)if(((𝐷𝑖)‘𝑍) ≤ 𝑧, ((𝐷𝑖)‘𝑍), 𝑧)) = (((𝐶)‘𝑍)[,)if(((𝐷)‘𝑍) ≤ 𝑧, ((𝐷)‘𝑍), 𝑧)))
223222fveq2d 6673 . . . . . . . . . . . . . 14 (𝑖 = → (vol‘(((𝐶𝑖)‘𝑍)[,)if(((𝐷𝑖)‘𝑍) ≤ 𝑧, ((𝐷𝑖)‘𝑍), 𝑧))) = (vol‘(((𝐶)‘𝑍)[,)if(((𝐷)‘𝑍) ≤ 𝑧, ((𝐷)‘𝑍), 𝑧))))
224223cbvmptv 5166 . . . . . . . . . . . . 13 (𝑖 ∈ ℕ ↦ (vol‘(((𝐶𝑖)‘𝑍)[,)if(((𝐷𝑖)‘𝑍) ≤ 𝑧, ((𝐷𝑖)‘𝑍), 𝑧)))) = ( ∈ ℕ ↦ (vol‘(((𝐶)‘𝑍)[,)if(((𝐷)‘𝑍) ≤ 𝑧, ((𝐷)‘𝑍), 𝑧))))
225215, 224eqtri 2849 . . . . . . . . . . . 12 (𝑖 ∈ ℕ ↦ (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍))‘𝑖)[,)if(((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖) ≤ 𝑧, ((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖), 𝑧)))) = ( ∈ ℕ ↦ (vol‘(((𝐶)‘𝑍)[,)if(((𝐷)‘𝑍) ≤ 𝑧, ((𝐷)‘𝑍), 𝑧))))
226225a1i 11 . . . . . . . . . . 11 (𝑤 = 𝑧 → (𝑖 ∈ ℕ ↦ (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍))‘𝑖)[,)if(((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖) ≤ 𝑧, ((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖), 𝑧)))) = ( ∈ ℕ ↦ (vol‘(((𝐶)‘𝑍)[,)if(((𝐷)‘𝑍) ≤ 𝑧, ((𝐷)‘𝑍), 𝑧)))))
227 breq2 5067 . . . . . . . . . . . . . . . 16 (𝑤 = 𝑧 → (((𝐷)‘𝑍) ≤ 𝑤 ↔ ((𝐷)‘𝑍) ≤ 𝑧))
228 id 22 . . . . . . . . . . . . . . . 16 (𝑤 = 𝑧𝑤 = 𝑧)
229227, 228ifbieq2d 4495 . . . . . . . . . . . . . . 15 (𝑤 = 𝑧 → if(((𝐷)‘𝑍) ≤ 𝑤, ((𝐷)‘𝑍), 𝑤) = if(((𝐷)‘𝑍) ≤ 𝑧, ((𝐷)‘𝑍), 𝑧))
230229eqcomd 2832 . . . . . . . . . . . . . 14 (𝑤 = 𝑧 → if(((𝐷)‘𝑍) ≤ 𝑧, ((𝐷)‘𝑍), 𝑧) = if(((𝐷)‘𝑍) ≤ 𝑤, ((𝐷)‘𝑍), 𝑤))
231230oveq2d 7166 . . . . . . . . . . . . 13 (𝑤 = 𝑧 → (((𝐶)‘𝑍)[,)if(((𝐷)‘𝑍) ≤ 𝑧, ((𝐷)‘𝑍), 𝑧)) = (((𝐶)‘𝑍)[,)if(((𝐷)‘𝑍) ≤ 𝑤, ((𝐷)‘𝑍), 𝑤)))
232231fveq2d 6673 . . . . . . . . . . . 12 (𝑤 = 𝑧 → (vol‘(((𝐶)‘𝑍)[,)if(((𝐷)‘𝑍) ≤ 𝑧, ((𝐷)‘𝑍), 𝑧))) = (vol‘(((𝐶)‘𝑍)[,)if(((𝐷)‘𝑍) ≤ 𝑤, ((𝐷)‘𝑍), 𝑤))))
233232mpteq2dv 5159 . . . . . . . . . . 11 (𝑤 = 𝑧 → ( ∈ ℕ ↦ (vol‘(((𝐶)‘𝑍)[,)if(((𝐷)‘𝑍) ≤ 𝑧, ((𝐷)‘𝑍), 𝑧)))) = ( ∈ ℕ ↦ (vol‘(((𝐶)‘𝑍)[,)if(((𝐷)‘𝑍) ≤ 𝑤, ((𝐷)‘𝑍), 𝑤)))))
234226, 233eqtr2d 2862 . . . . . . . . . 10 (𝑤 = 𝑧 → ( ∈ ℕ ↦ (vol‘(((𝐶)‘𝑍)[,)if(((𝐷)‘𝑍) ≤ 𝑤, ((𝐷)‘𝑍), 𝑤)))) = (𝑖 ∈ ℕ ↦ (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍))‘𝑖)[,)if(((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖) ≤ 𝑧, ((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖), 𝑧)))))
235234fveq2d 6673 . . . . . . . . 9 (𝑤 = 𝑧 → (Σ^‘( ∈ ℕ ↦ (vol‘(((𝐶)‘𝑍)[,)if(((𝐷)‘𝑍) ≤ 𝑤, ((𝐷)‘𝑍), 𝑤))))) = (Σ^‘(𝑖 ∈ ℕ ↦ (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍))‘𝑖)[,)if(((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖) ≤ 𝑧, ((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖), 𝑧))))))
236210, 235breq12d 5076 . . . . . . . 8 (𝑤 = 𝑧 → ((𝑤 − (𝐴𝑍)) ≤ (Σ^‘( ∈ ℕ ↦ (vol‘(((𝐶)‘𝑍)[,)if(((𝐷)‘𝑍) ≤ 𝑤, ((𝐷)‘𝑍), 𝑤))))) ↔ (𝑧 − (𝐴𝑍)) ≤ (Σ^‘(𝑖 ∈ ℕ ↦ (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍))‘𝑖)[,)if(((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖) ≤ 𝑧, ((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖), 𝑧)))))))
237236cbvrabv 3497 . . . . . . 7 {𝑤 ∈ ((𝐴𝑍)[,](𝐵𝑍)) ∣ (𝑤 − (𝐴𝑍)) ≤ (Σ^‘( ∈ ℕ ↦ (vol‘(((𝐶)‘𝑍)[,)if(((𝐷)‘𝑍) ≤ 𝑤, ((𝐷)‘𝑍), 𝑤)))))} = {𝑧 ∈ ((𝐴𝑍)[,](𝐵𝑍)) ∣ (𝑧 − (𝐴𝑍)) ≤ (Σ^‘(𝑖 ∈ ℕ ↦ (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍))‘𝑖)[,)if(((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖) ≤ 𝑧, ((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖), 𝑧)))))}
238 eqid 2826 . . . . . . 7 sup({𝑤 ∈ ((𝐴𝑍)[,](𝐵𝑍)) ∣ (𝑤 − (𝐴𝑍)) ≤ (Σ^‘( ∈ ℕ ↦ (vol‘(((𝐶)‘𝑍)[,)if(((𝐷)‘𝑍) ≤ 𝑤, ((𝐷)‘𝑍), 𝑤)))))}, ℝ, < ) = sup({𝑤 ∈ ((𝐴𝑍)[,](𝐵𝑍)) ∣ (𝑤 − (𝐴𝑍)) ≤ (Σ^‘( ∈ ℕ ↦ (vol‘(((𝐶)‘𝑍)[,)if(((𝐷)‘𝑍) ≤ 𝑤, ((𝐷)‘𝑍), 𝑤)))))}, ℝ, < )
23980, 81, 82, 85, 88, 189, 209, 237, 238hoidmv1lelem3 42760 . . . . . 6 (((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) ∈ ℝ) → ((𝐵𝑍) − (𝐴𝑍)) ≤ (Σ^‘(𝑖 ∈ ℕ ↦ (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍))‘𝑖)[,)((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖))))))
240239, 207breqtrd 5089 . . . . 5 (((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) ∈ ℝ) → ((𝐵𝑍) − (𝐴𝑍)) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))))
24121, 79, 240syl2anc 584 . . . 4 (((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) ∧ ¬ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) = +∞) → ((𝐵𝑍) − (𝐴𝑍)) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))))
24220, 241pm2.61dan 809 . . 3 ((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) → ((𝐵𝑍) − (𝐴𝑍)) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))))
24325, 29, 31, 8, 1hoidmvn0val 42751 . . . . . . 7 (𝜑 → (𝐴(𝐿𝑋)𝐵) = ∏𝑘𝑋 (vol‘((𝐴𝑘)[,)(𝐵𝑘))))
24426prodeq1d 15270 . . . . . . 7 (𝜑 → ∏𝑘𝑋 (vol‘((𝐴𝑘)[,)(𝐵𝑘))) = ∏𝑘 ∈ {𝑍} (vol‘((𝐴𝑘)[,)(𝐵𝑘))))
245 volicore 42748 . . . . . . . . . 10 (((𝐴𝑍) ∈ ℝ ∧ (𝐵𝑍) ∈ ℝ) → (vol‘((𝐴𝑍)[,)(𝐵𝑍))) ∈ ℝ)
2469, 7, 245syl2anc 584 . . . . . . . . 9 (𝜑 → (vol‘((𝐴𝑍)[,)(𝐵𝑍))) ∈ ℝ)
247246recnd 10663 . . . . . . . 8 (𝜑 → (vol‘((𝐴𝑍)[,)(𝐵𝑍))) ∈ ℂ)
248117, 119oveq12d 7168 . . . . . . . . . 10 (𝑘 = 𝑍 → ((𝐴𝑘)[,)(𝐵𝑘)) = ((𝐴𝑍)[,)(𝐵𝑍)))
249248fveq2d 6673 . . . . . . . . 9 (𝑘 = 𝑍 → (vol‘((𝐴𝑘)[,)(𝐵𝑘))) = (vol‘((𝐴𝑍)[,)(𝐵𝑍))))
250249prodsn 15311 . . . . . . . 8 ((𝑍𝑉 ∧ (vol‘((𝐴𝑍)[,)(𝐵𝑍))) ∈ ℂ) → ∏𝑘 ∈ {𝑍} (vol‘((𝐴𝑘)[,)(𝐵𝑘))) = (vol‘((𝐴𝑍)[,)(𝐵𝑍))))
2512, 247, 250syl2anc 584 . . . . . . 7 (𝜑 → ∏𝑘 ∈ {𝑍} (vol‘((𝐴𝑘)[,)(𝐵𝑘))) = (vol‘((𝐴𝑍)[,)(𝐵𝑍))))
252243, 244, 2513eqtrd 2865 . . . . . 6 (𝜑 → (𝐴(𝐿𝑋)𝐵) = (vol‘((𝐴𝑍)[,)(𝐵𝑍))))
253252adantr 481 . . . . 5 ((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) → (𝐴(𝐿𝑋)𝐵) = (vol‘((𝐴𝑍)[,)(𝐵𝑍))))
254 volico 42153 . . . . . . 7 (((𝐴𝑍) ∈ ℝ ∧ (𝐵𝑍) ∈ ℝ) → (vol‘((𝐴𝑍)[,)(𝐵𝑍))) = if((𝐴𝑍) < (𝐵𝑍), ((𝐵𝑍) − (𝐴𝑍)), 0))
2559, 7, 254syl2anc 584 . . . . . 6 (𝜑 → (vol‘((𝐴𝑍)[,)(𝐵𝑍))) = if((𝐴𝑍) < (𝐵𝑍), ((𝐵𝑍) − (𝐴𝑍)), 0))
256255adantr 481 . . . . 5 ((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) → (vol‘((𝐴𝑍)[,)(𝐵𝑍))) = if((𝐴𝑍) < (𝐵𝑍), ((𝐵𝑍) − (𝐴𝑍)), 0))
257 iftrue 4476 . . . . . 6 ((𝐴𝑍) < (𝐵𝑍) → if((𝐴𝑍) < (𝐵𝑍), ((𝐵𝑍) − (𝐴𝑍)), 0) = ((𝐵𝑍) − (𝐴𝑍)))
258257adantl 482 . . . . 5 ((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) → if((𝐴𝑍) < (𝐵𝑍), ((𝐵𝑍) − (𝐴𝑍)), 0) = ((𝐵𝑍) − (𝐴𝑍)))
259253, 256, 2583eqtrd 2865 . . . 4 ((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) → (𝐴(𝐿𝑋)𝐵) = ((𝐵𝑍) − (𝐴𝑍)))
26058fveq2d 6673 . . . . 5 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗)))) = (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))))
261260adantr 481 . . . 4 ((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗)))) = (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))))
262259, 261breq12d 5076 . . 3 ((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) → ((𝐴(𝐿𝑋)𝐵) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗)))) ↔ ((𝐵𝑍) − (𝐴𝑍)) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))))))
263242, 262mpbird 258 . 2 ((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) → (𝐴(𝐿𝑋)𝐵) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗)))))
264243adantr 481 . . . 4 ((𝜑 ∧ ¬ (𝐴𝑍) < (𝐵𝑍)) → (𝐴(𝐿𝑋)𝐵) = ∏𝑘𝑋 (vol‘((𝐴𝑘)[,)(𝐵𝑘))))
265244adantr 481 . . . 4 ((𝜑 ∧ ¬ (𝐴𝑍) < (𝐵𝑍)) → ∏𝑘𝑋 (vol‘((𝐴𝑘)[,)(𝐵𝑘))) = ∏𝑘 ∈ {𝑍} (vol‘((𝐴𝑘)[,)(𝐵𝑘))))
266251adantr 481 . . . . 5 ((𝜑 ∧ ¬ (𝐴𝑍) < (𝐵𝑍)) → ∏𝑘 ∈ {𝑍} (vol‘((𝐴𝑘)[,)(𝐵𝑘))) = (vol‘((𝐴𝑍)[,)(𝐵𝑍))))
267255adantr 481 . . . . 5 ((𝜑 ∧ ¬ (𝐴𝑍) < (𝐵𝑍)) → (vol‘((𝐴𝑍)[,)(𝐵𝑍))) = if((𝐴𝑍) < (𝐵𝑍), ((𝐵𝑍) − (𝐴𝑍)), 0))
268 iffalse 4479 . . . . . 6 (¬ (𝐴𝑍) < (𝐵𝑍) → if((𝐴𝑍) < (𝐵𝑍), ((𝐵𝑍) − (𝐴𝑍)), 0) = 0)
269268adantl 482 . . . . 5 ((𝜑 ∧ ¬ (𝐴𝑍) < (𝐵𝑍)) → if((𝐴𝑍) < (𝐵𝑍), ((𝐵𝑍) − (𝐴𝑍)), 0) = 0)
270266, 267, 2693eqtrd 2865 . . . 4 ((𝜑 ∧ ¬ (𝐴𝑍) < (𝐵𝑍)) → ∏𝑘 ∈ {𝑍} (vol‘((𝐴𝑘)[,)(𝐵𝑘))) = 0)
271264, 265, 2703eqtrd 2865 . . 3 ((𝜑 ∧ ¬ (𝐴𝑍) < (𝐵𝑍)) → (𝐴(𝐿𝑋)𝐵) = 0)
27223a1i 11 . . . . 5 (𝜑 → ℕ ∈ V)
273272, 75sge0ge0 42551 . . . 4 (𝜑 → 0 ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗)))))
274273adantr 481 . . 3 ((𝜑 ∧ ¬ (𝐴𝑍) < (𝐵𝑍)) → 0 ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗)))))
275271, 274eqbrtrd 5085 . 2 ((𝜑 ∧ ¬ (𝐴𝑍) < (𝐵𝑍)) → (𝐴(𝐿𝑋)𝐵) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗)))))
276263, 275pm2.61dan 809 1 (𝜑 → (𝐴(𝐿𝑋)𝐵) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗)))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207  wa 396  w3a 1081   = wceq 1530  wcel 2107  wne 3021  wral 3143  wrex 3144  {crab 3147  Vcvv 3500  wss 3940  c0 4295  ifcif 4470  {csn 4564  cop 4570   ciun 4917   class class class wbr 5063  cmpt 5143  wf 6350  cfv 6354  (class class class)co 7150  cmpo 7152  m cmap 8401  Xcixp 8455  Fincfn 8503  supcsup 8898  cc 10529  cr 10530  0cc0 10531  +∞cpnf 10666  *cxr 10668   < clt 10669  cle 10670  cmin 10864  cn 11632  [,)cico 12735  [,]cicc 12736  cprod 15254  volcvol 23998  Σ^csumge0 42529
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-13 2385  ax-ext 2798  ax-rep 5187  ax-sep 5200  ax-nul 5207  ax-pow 5263  ax-pr 5326  ax-un 7455  ax-inf2 9098  ax-cnex 10587  ax-resscn 10588  ax-1cn 10589  ax-icn 10590  ax-addcl 10591  ax-addrcl 10592  ax-mulcl 10593  ax-mulrcl 10594  ax-mulcom 10595  ax-addass 10596  ax-mulass 10597  ax-distr 10598  ax-i2m1 10599  ax-1ne0 10600  ax-1rid 10601  ax-rnegex 10602  ax-rrecex 10603  ax-cnre 10604  ax-pre-lttri 10605  ax-pre-lttrn 10606  ax-pre-ltadd 10607  ax-pre-mulgt0 10608  ax-pre-sup 10609
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3or 1082  df-3an 1083  df-tru 1533  df-fal 1543  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2620  df-eu 2652  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-ne 3022  df-nel 3129  df-ral 3148  df-rex 3149  df-reu 3150  df-rmo 3151  df-rab 3152  df-v 3502  df-sbc 3777  df-csb 3888  df-dif 3943  df-un 3945  df-in 3947  df-ss 3956  df-pss 3958  df-nul 4296  df-if 4471  df-pw 4544  df-sn 4565  df-pr 4567  df-tp 4569  df-op 4571  df-uni 4838  df-int 4875  df-iun 4919  df-br 5064  df-opab 5126  df-mpt 5144  df-tr 5170  df-id 5459  df-eprel 5464  df-po 5473  df-so 5474  df-fr 5513  df-se 5514  df-we 5515  df-xp 5560  df-rel 5561  df-cnv 5562  df-co 5563  df-dm 5564  df-rn 5565  df-res 5566  df-ima 5567  df-pred 6147  df-ord 6193  df-on 6194  df-lim 6195  df-suc 6196  df-iota 6313  df-fun 6356  df-fn 6357  df-f 6358  df-f1 6359  df-fo 6360  df-f1o 6361  df-fv 6362  df-isom 6363  df-riota 7108  df-ov 7153  df-oprab 7154  df-mpo 7155  df-of 7403  df-om 7574  df-1st 7685  df-2nd 7686  df-wrecs 7943  df-recs 8004  df-rdg 8042  df-1o 8098  df-2o 8099  df-oadd 8102  df-er 8284  df-map 8403  df-pm 8404  df-ixp 8456  df-en 8504  df-dom 8505  df-sdom 8506  df-fin 8507  df-fi 8869  df-sup 8900  df-inf 8901  df-oi 8968  df-dju 9324  df-card 9362  df-pnf 10671  df-mnf 10672  df-xr 10673  df-ltxr 10674  df-le 10675  df-sub 10866  df-neg 10867  df-div 11292  df-nn 11633  df-2 11694  df-3 11695  df-n0 11892  df-z 11976  df-uz 12238  df-q 12343  df-rp 12385  df-xneg 12502  df-xadd 12503  df-xmul 12504  df-ioo 12737  df-ico 12739  df-icc 12740  df-fz 12888  df-fzo 13029  df-fl 13157  df-seq 13365  df-exp 13425  df-hash 13686  df-cj 14453  df-re 14454  df-im 14455  df-sqrt 14589  df-abs 14590  df-clim 14840  df-rlim 14841  df-sum 15038  df-prod 15255  df-rest 16691  df-topgen 16712  df-psmet 20472  df-xmet 20473  df-met 20474  df-bl 20475  df-mopn 20476  df-top 21437  df-topon 21454  df-bases 21489  df-cmp 21930  df-ovol 23999  df-vol 24000  df-sumge0 42530
This theorem is referenced by:  hoidmvle  42767
  Copyright terms: Public domain W3C validator