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 41380
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 4364 . . . . . . . . . . . 12 (𝑍𝑉𝑍 ∈ {𝑍})
42, 3syl 17 . . . . . . . . . . 11 (𝜑𝑍 ∈ {𝑍})
5 hoidmv1le.x . . . . . . . . . . 11 𝑋 = {𝑍}
64, 5syl6eleqr 2855 . . . . . . . . . 10 (𝜑𝑍𝑋)
71, 6ffvelrnd 6550 . . . . . . . . 9 (𝜑 → (𝐵𝑍) ∈ ℝ)
8 hoidmv1le.a . . . . . . . . . 10 (𝜑𝐴:𝑋⟶ℝ)
98, 6ffvelrnd 6550 . . . . . . . . 9 (𝜑 → (𝐴𝑍) ∈ ℝ)
107, 9resubcld 10712 . . . . . . . 8 (𝜑 → ((𝐵𝑍) − (𝐴𝑍)) ∈ ℝ)
1110rexrd 10343 . . . . . . 7 (𝜑 → ((𝐵𝑍) − (𝐴𝑍)) ∈ ℝ*)
12 pnfxr 10346 . . . . . . . 8 +∞ ∈ ℝ*
1312a1i 11 . . . . . . 7 (𝜑 → +∞ ∈ ℝ*)
1410ltpnfd 12155 . . . . . . 7 (𝜑 → ((𝐵𝑍) − (𝐴𝑍)) < +∞)
1511, 13, 14xrltled 12183 . . . . . 6 (𝜑 → ((𝐵𝑍) − (𝐴𝑍)) ≤ +∞)
1615ad2antrr 717 . . . . 5 (((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) = +∞) → ((𝐵𝑍) − (𝐴𝑍)) ≤ +∞)
17 id 22 . . . . . . 7 ((Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) = +∞ → (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) = +∞)
1817eqcomd 2771 . . . . . 6 ((Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) = +∞ → +∞ = (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))))
1918adantl 473 . . . . 5 (((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) = +∞) → +∞ = (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))))
2016, 19breqtrd 4835 . . . 4 (((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) = +∞) → ((𝐵𝑍) − (𝐴𝑍)) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))))
21 simpl 474 . . . . 5 (((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) ∧ ¬ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) = +∞) → (𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)))
22 simpr 477 . . . . . 6 (((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) ∧ ¬ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) = +∞) → ¬ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) = +∞)
23 nnex 11281 . . . . . . . 8 ℕ ∈ V
2423a1i 11 . . . . . . 7 (((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) ∧ ¬ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) = +∞) → ℕ ∈ V)
25 hoidmv1le.l . . . . . . . . . . . 12 𝐿 = (𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑𝑚 𝑥), 𝑏 ∈ (ℝ ↑𝑚 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘𝑥 (vol‘((𝑎𝑘)[,)(𝑏𝑘))))))
265a1i 11 . . . . . . . . . . . . . 14 (𝜑𝑋 = {𝑍})
27 snfi 8245 . . . . . . . . . . . . . . 15 {𝑍} ∈ Fin
2827a1i 11 . . . . . . . . . . . . . 14 (𝜑 → {𝑍} ∈ Fin)
2926, 28eqeltrd 2844 . . . . . . . . . . . . 13 (𝜑𝑋 ∈ Fin)
3029adantr 472 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ) → 𝑋 ∈ Fin)
316ne0d 4086 . . . . . . . . . . . . 13 (𝜑𝑋 ≠ ∅)
3231adantr 472 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ) → 𝑋 ≠ ∅)
33 hoidmv1le.c . . . . . . . . . . . . . 14 (𝜑𝐶:ℕ⟶(ℝ ↑𝑚 𝑋))
3433ffvelrnda 6549 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ ℕ) → (𝐶𝑗) ∈ (ℝ ↑𝑚 𝑋))
35 elmapi 8082 . . . . . . . . . . . . 13 ((𝐶𝑗) ∈ (ℝ ↑𝑚 𝑋) → (𝐶𝑗):𝑋⟶ℝ)
3634, 35syl 17 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ) → (𝐶𝑗):𝑋⟶ℝ)
37 hoidmv1le.d . . . . . . . . . . . . . 14 (𝜑𝐷:ℕ⟶(ℝ ↑𝑚 𝑋))
3837ffvelrnda 6549 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ ℕ) → (𝐷𝑗) ∈ (ℝ ↑𝑚 𝑋))
39 elmapi 8082 . . . . . . . . . . . . 13 ((𝐷𝑗) ∈ (ℝ ↑𝑚 𝑋) → (𝐷𝑗):𝑋⟶ℝ)
4038, 39syl 17 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ) → (𝐷𝑗):𝑋⟶ℝ)
4125, 30, 32, 36, 40hoidmvn0val 41370 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗)) = ∏𝑘𝑋 (vol‘(((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))))
425prodeq1i 14933 . . . . . . . . . . . 12 𝑘𝑋 (vol‘(((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) = ∏𝑘 ∈ {𝑍} (vol‘(((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
4342a1i 11 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ℕ) → ∏𝑘𝑋 (vol‘(((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) = ∏𝑘 ∈ {𝑍} (vol‘(((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))))
442adantr 472 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ) → 𝑍𝑉)
456adantr 472 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ ℕ) → 𝑍𝑋)
4636, 45ffvelrnd 6550 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗)‘𝑍) ∈ ℝ)
4740, 45ffvelrnd 6550 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ ℕ) → ((𝐷𝑗)‘𝑍) ∈ ℝ)
48 volicore 41367 . . . . . . . . . . . . . 14 ((((𝐶𝑗)‘𝑍) ∈ ℝ ∧ ((𝐷𝑗)‘𝑍) ∈ ℝ) → (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))) ∈ ℝ)
4946, 47, 48syl2anc 579 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ ℕ) → (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))) ∈ ℝ)
5049recnd 10322 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ) → (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))) ∈ ℂ)
51 fveq2 6375 . . . . . . . . . . . . . . 15 (𝑘 = 𝑍 → ((𝐶𝑗)‘𝑘) = ((𝐶𝑗)‘𝑍))
52 fveq2 6375 . . . . . . . . . . . . . . 15 (𝑘 = 𝑍 → ((𝐷𝑗)‘𝑘) = ((𝐷𝑗)‘𝑍))
5351, 52oveq12d 6860 . . . . . . . . . . . . . 14 (𝑘 = 𝑍 → (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) = (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))
5453fveq2d 6379 . . . . . . . . . . . . 13 (𝑘 = 𝑍 → (vol‘(((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) = (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))
5554prodsn 14977 . . . . . . . . . . . 12 ((𝑍𝑉 ∧ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))) ∈ ℂ) → ∏𝑘 ∈ {𝑍} (vol‘(((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) = (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))
5644, 50, 55syl2anc 579 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ℕ) → ∏𝑘 ∈ {𝑍} (vol‘(((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘))) = (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))
5741, 43, 563eqtrd 2803 . . . . . . . . . 10 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗)) = (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))
5857mpteq2dva 4903 . . . . . . . . 9 (𝜑 → (𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗))) = (𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))))
59 fveq2 6375 . . . . . . . . . . . . . . . . . . . 20 (𝑘 = 𝑙 → (𝑎𝑘) = (𝑎𝑙))
60 fveq2 6375 . . . . . . . . . . . . . . . . . . . 20 (𝑘 = 𝑙 → (𝑏𝑘) = (𝑏𝑙))
6159, 60oveq12d 6860 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 𝑙 → ((𝑎𝑘)[,)(𝑏𝑘)) = ((𝑎𝑙)[,)(𝑏𝑙)))
6261fveq2d 6379 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑙 → (vol‘((𝑎𝑘)[,)(𝑏𝑘))) = (vol‘((𝑎𝑙)[,)(𝑏𝑙))))
6362cbvprodv 14931 . . . . . . . . . . . . . . . . 17 𝑘𝑥 (vol‘((𝑎𝑘)[,)(𝑏𝑘))) = ∏𝑙𝑥 (vol‘((𝑎𝑙)[,)(𝑏𝑙)))
64 ifeq2 4248 . . . . . . . . . . . . . . . . 17 (∏𝑘𝑥 (vol‘((𝑎𝑘)[,)(𝑏𝑘))) = ∏𝑙𝑥 (vol‘((𝑎𝑙)[,)(𝑏𝑙))) → if(𝑥 = ∅, 0, ∏𝑘𝑥 (vol‘((𝑎𝑘)[,)(𝑏𝑘)))) = if(𝑥 = ∅, 0, ∏𝑙𝑥 (vol‘((𝑎𝑙)[,)(𝑏𝑙)))))
6563, 64ax-mp 5 . . . . . . . . . . . . . . . 16 if(𝑥 = ∅, 0, ∏𝑘𝑥 (vol‘((𝑎𝑘)[,)(𝑏𝑘)))) = if(𝑥 = ∅, 0, ∏𝑙𝑥 (vol‘((𝑎𝑙)[,)(𝑏𝑙))))
6665a1i 11 . . . . . . . . . . . . . . 15 ((𝑎 ∈ (ℝ ↑𝑚 𝑥) ∧ 𝑏 ∈ (ℝ ↑𝑚 𝑥)) → if(𝑥 = ∅, 0, ∏𝑘𝑥 (vol‘((𝑎𝑘)[,)(𝑏𝑘)))) = if(𝑥 = ∅, 0, ∏𝑙𝑥 (vol‘((𝑎𝑙)[,)(𝑏𝑙)))))
6766mpt2eq3ia 6918 . . . . . . . . . . . . . 14 (𝑎 ∈ (ℝ ↑𝑚 𝑥), 𝑏 ∈ (ℝ ↑𝑚 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘𝑥 (vol‘((𝑎𝑘)[,)(𝑏𝑘))))) = (𝑎 ∈ (ℝ ↑𝑚 𝑥), 𝑏 ∈ (ℝ ↑𝑚 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑙𝑥 (vol‘((𝑎𝑙)[,)(𝑏𝑙)))))
6867mpteq2i 4900 . . . . . . . . . . . . 13 (𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑𝑚 𝑥), 𝑏 ∈ (ℝ ↑𝑚 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘𝑥 (vol‘((𝑎𝑘)[,)(𝑏𝑘)))))) = (𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑𝑚 𝑥), 𝑏 ∈ (ℝ ↑𝑚 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑙𝑥 (vol‘((𝑎𝑙)[,)(𝑏𝑙))))))
6925, 68eqtri 2787 . . . . . . . . . . . 12 𝐿 = (𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑𝑚 𝑥), 𝑏 ∈ (ℝ ↑𝑚 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑙𝑥 (vol‘((𝑎𝑙)[,)(𝑏𝑙))))))
7069, 30, 36, 40hoidmvcl 41368 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ℕ) → ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗)) ∈ (0[,)+∞))
71 eqid 2765 . . . . . . . . . . 11 (𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗))) = (𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗)))
7270, 71fmptd 6574 . . . . . . . . . 10 (𝜑 → (𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗))):ℕ⟶(0[,)+∞))
73 icossicc 12463 . . . . . . . . . . 11 (0[,)+∞) ⊆ (0[,]+∞)
7473a1i 11 . . . . . . . . . 10 (𝜑 → (0[,)+∞) ⊆ (0[,]+∞))
7572, 74fssd 6237 . . . . . . . . 9 (𝜑 → (𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗))):ℕ⟶(0[,]+∞))
7658, 75feq1dd 39926 . . . . . . . 8 (𝜑 → (𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))):ℕ⟶(0[,]+∞))
7776ad2antrr 717 . . . . . . 7 (((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) ∧ ¬ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) = +∞) → (𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))):ℕ⟶(0[,]+∞))
7824, 77sge0repnf 41172 . . . . . 6 (((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) ∧ ¬ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) = +∞) → ((Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) ∈ ℝ ↔ ¬ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) = +∞))
7922, 78mpbird 248 . . . . 5 (((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) ∧ ¬ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) = +∞) → (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) ∈ ℝ)
809ad2antrr 717 . . . . . . 7 (((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) ∈ ℝ) → (𝐴𝑍) ∈ ℝ)
817ad2antrr 717 . . . . . . 7 (((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) ∈ ℝ) → (𝐵𝑍) ∈ ℝ)
82 simplr 785 . . . . . . 7 (((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) ∈ ℝ) → (𝐴𝑍) < (𝐵𝑍))
83 eqid 2765 . . . . . . . . 9 (𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍)) = (𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍))
8446, 83fmptd 6574 . . . . . . . 8 (𝜑 → (𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍)):ℕ⟶ℝ)
8584ad2antrr 717 . . . . . . 7 (((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) ∈ ℝ) → (𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍)):ℕ⟶ℝ)
86 eqid 2765 . . . . . . . . 9 (𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍)) = (𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))
8747, 86fmptd 6574 . . . . . . . 8 (𝜑 → (𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍)):ℕ⟶ℝ)
8887ad2antrr 717 . . . . . . 7 (((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) ∈ ℝ) → (𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍)):ℕ⟶ℝ)
89 hoidmv1le.s . . . . . . . . . . . . . . . . 17 (𝜑X𝑘𝑋 ((𝐴𝑘)[,)(𝐵𝑘)) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)))
905eleq2i 2836 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑘𝑋𝑘 ∈ {𝑍})
9190biimpi 207 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑘𝑋𝑘 ∈ {𝑍})
92 elsni 4351 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑘 ∈ {𝑍} → 𝑘 = 𝑍)
9391, 92syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑘𝑋𝑘 = 𝑍)
9493, 53syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘𝑋 → (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) = (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))
9594rgen 3069 . . . . . . . . . . . . . . . . . . . . 21 𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) = (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))
96 ixpeq2 8127 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) = (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) → X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) = X𝑘𝑋 (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))
9795, 96ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) = X𝑘𝑋 (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))
9897a1i 11 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ ℕ → X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) = X𝑘𝑋 (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))
9998iuneq2i 4695 . . . . . . . . . . . . . . . . . 18 𝑗 ∈ ℕ X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) = 𝑗 ∈ ℕ X𝑘𝑋 (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))
10099a1i 11 . . . . . . . . . . . . . . . . 17 (𝜑 𝑗 ∈ ℕ X𝑘𝑋 (((𝐶𝑗)‘𝑘)[,)((𝐷𝑗)‘𝑘)) = 𝑗 ∈ ℕ X𝑘𝑋 (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))
10189, 100sseqtrd 3801 . . . . . . . . . . . . . . . 16 (𝜑X𝑘𝑋 ((𝐴𝑘)[,)(𝐵𝑘)) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))
102101adantr 472 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ ((𝐴𝑍)[,)(𝐵𝑍))) → X𝑘𝑋 ((𝐴𝑘)[,)(𝐵𝑘)) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))
103 id 22 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ((𝐴𝑍)[,)(𝐵𝑍)) → 𝑥 ∈ ((𝐴𝑍)[,)(𝐵𝑍)))
104 eqidd 2766 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ((𝐴𝑍)[,)(𝐵𝑍)) → {⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑥⟩})
105 opeq2 4560 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 = 𝑥 → ⟨𝑍, 𝑦⟩ = ⟨𝑍, 𝑥⟩)
106105sneqd 4346 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = 𝑥 → {⟨𝑍, 𝑦⟩} = {⟨𝑍, 𝑥⟩})
107106rspceeqv 3479 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ∈ ((𝐴𝑍)[,)(𝐵𝑍)) ∧ {⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑥⟩}) → ∃𝑦 ∈ ((𝐴𝑍)[,)(𝐵𝑍)){⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩})
108103, 104, 107syl2anc 579 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ((𝐴𝑍)[,)(𝐵𝑍)) → ∃𝑦 ∈ ((𝐴𝑍)[,)(𝐵𝑍)){⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩})
109108adantl 473 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ ((𝐴𝑍)[,)(𝐵𝑍))) → ∃𝑦 ∈ ((𝐴𝑍)[,)(𝐵𝑍)){⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩})
110 elixpsn 8152 . . . . . . . . . . . . . . . . . . 19 (𝑍𝑉 → ({⟨𝑍, 𝑥⟩} ∈ X𝑘 ∈ {𝑍} ((𝐴𝑍)[,)(𝐵𝑍)) ↔ ∃𝑦 ∈ ((𝐴𝑍)[,)(𝐵𝑍)){⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩}))
1112, 110syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑 → ({⟨𝑍, 𝑥⟩} ∈ X𝑘 ∈ {𝑍} ((𝐴𝑍)[,)(𝐵𝑍)) ↔ ∃𝑦 ∈ ((𝐴𝑍)[,)(𝐵𝑍)){⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩}))
112111adantr 472 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ ((𝐴𝑍)[,)(𝐵𝑍))) → ({⟨𝑍, 𝑥⟩} ∈ X𝑘 ∈ {𝑍} ((𝐴𝑍)[,)(𝐵𝑍)) ↔ ∃𝑦 ∈ ((𝐴𝑍)[,)(𝐵𝑍)){⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩}))
113109, 112mpbird 248 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ ((𝐴𝑍)[,)(𝐵𝑍))) → {⟨𝑍, 𝑥⟩} ∈ X𝑘 ∈ {𝑍} ((𝐴𝑍)[,)(𝐵𝑍)))
1145eqcomi 2774 . . . . . . . . . . . . . . . . . . . 20 {𝑍} = 𝑋
115 ixpeq1 8124 . . . . . . . . . . . . . . . . . . . 20 ({𝑍} = 𝑋X𝑘 ∈ {𝑍} ((𝐴𝑍)[,)(𝐵𝑍)) = X𝑘𝑋 ((𝐴𝑍)[,)(𝐵𝑍)))
116114, 115ax-mp 5 . . . . . . . . . . . . . . . . . . 19 X𝑘 ∈ {𝑍} ((𝐴𝑍)[,)(𝐵𝑍)) = X𝑘𝑋 ((𝐴𝑍)[,)(𝐵𝑍))
117 fveq2 6375 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑘 = 𝑍 → (𝐴𝑘) = (𝐴𝑍))
11893, 117syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑘𝑋 → (𝐴𝑘) = (𝐴𝑍))
119 fveq2 6375 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑘 = 𝑍 → (𝐵𝑘) = (𝐵𝑍))
12093, 119syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑘𝑋 → (𝐵𝑘) = (𝐵𝑍))
121118, 120oveq12d 6860 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘𝑋 → ((𝐴𝑘)[,)(𝐵𝑘)) = ((𝐴𝑍)[,)(𝐵𝑍)))
122121eqcomd 2771 . . . . . . . . . . . . . . . . . . . . 21 (𝑘𝑋 → ((𝐴𝑍)[,)(𝐵𝑍)) = ((𝐴𝑘)[,)(𝐵𝑘)))
123122rgen 3069 . . . . . . . . . . . . . . . . . . . 20 𝑘𝑋 ((𝐴𝑍)[,)(𝐵𝑍)) = ((𝐴𝑘)[,)(𝐵𝑘))
124 ixpeq2 8127 . . . . . . . . . . . . . . . . . . . 20 (∀𝑘𝑋 ((𝐴𝑍)[,)(𝐵𝑍)) = ((𝐴𝑘)[,)(𝐵𝑘)) → X𝑘𝑋 ((𝐴𝑍)[,)(𝐵𝑍)) = X𝑘𝑋 ((𝐴𝑘)[,)(𝐵𝑘)))
125123, 124ax-mp 5 . . . . . . . . . . . . . . . . . . 19 X𝑘𝑋 ((𝐴𝑍)[,)(𝐵𝑍)) = X𝑘𝑋 ((𝐴𝑘)[,)(𝐵𝑘))
126116, 125eqtri 2787 . . . . . . . . . . . . . . . . . 18 X𝑘 ∈ {𝑍} ((𝐴𝑍)[,)(𝐵𝑍)) = X𝑘𝑋 ((𝐴𝑘)[,)(𝐵𝑘))
127126a1i 11 . . . . . . . . . . . . . . . . 17 (𝜑X𝑘 ∈ {𝑍} ((𝐴𝑍)[,)(𝐵𝑍)) = X𝑘𝑋 ((𝐴𝑘)[,)(𝐵𝑘)))
128127adantr 472 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ ((𝐴𝑍)[,)(𝐵𝑍))) → X𝑘 ∈ {𝑍} ((𝐴𝑍)[,)(𝐵𝑍)) = X𝑘𝑋 ((𝐴𝑘)[,)(𝐵𝑘)))
129113, 128eleqtrd 2846 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ ((𝐴𝑍)[,)(𝐵𝑍))) → {⟨𝑍, 𝑥⟩} ∈ X𝑘𝑋 ((𝐴𝑘)[,)(𝐵𝑘)))
130102, 129sseldd 3762 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ ((𝐴𝑍)[,)(𝐵𝑍))) → {⟨𝑍, 𝑥⟩} ∈ 𝑗 ∈ ℕ X𝑘𝑋 (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))
131 eliun 4680 . . . . . . . . . . . . . 14 ({⟨𝑍, 𝑥⟩} ∈ 𝑗 ∈ ℕ X𝑘𝑋 (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) ↔ ∃𝑗 ∈ ℕ {⟨𝑍, 𝑥⟩} ∈ X𝑘𝑋 (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))
132130, 131sylib 209 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ ((𝐴𝑍)[,)(𝐵𝑍))) → ∃𝑗 ∈ ℕ {⟨𝑍, 𝑥⟩} ∈ X𝑘𝑋 (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))
133 ixpeq1 8124 . . . . . . . . . . . . . . . . . . . . . 22 (𝑋 = {𝑍} → X𝑘𝑋 (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) = X𝑘 ∈ {𝑍} (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))
1345, 133ax-mp 5 . . . . . . . . . . . . . . . . . . . . 21 X𝑘𝑋 (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) = X𝑘 ∈ {𝑍} (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))
135134eleq2i 2836 . . . . . . . . . . . . . . . . . . . 20 ({⟨𝑍, 𝑥⟩} ∈ X𝑘𝑋 (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) ↔ {⟨𝑍, 𝑥⟩} ∈ X𝑘 ∈ {𝑍} (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))
136135biimpi 207 . . . . . . . . . . . . . . . . . . 19 ({⟨𝑍, 𝑥⟩} ∈ X𝑘𝑋 (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) → {⟨𝑍, 𝑥⟩} ∈ X𝑘 ∈ {𝑍} (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))
137136adantl 473 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ {⟨𝑍, 𝑥⟩} ∈ X𝑘𝑋 (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))) → {⟨𝑍, 𝑥⟩} ∈ X𝑘 ∈ {𝑍} (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))
138 elixpsn 8152 . . . . . . . . . . . . . . . . . . . 20 (𝑍𝑉 → ({⟨𝑍, 𝑥⟩} ∈ X𝑘 ∈ {𝑍} (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) ↔ ∃𝑦 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)){⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩}))
1392, 138syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ({⟨𝑍, 𝑥⟩} ∈ X𝑘 ∈ {𝑍} (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) ↔ ∃𝑦 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)){⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩}))
140139adantr 472 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ {⟨𝑍, 𝑥⟩} ∈ X𝑘𝑋 (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))) → ({⟨𝑍, 𝑥⟩} ∈ X𝑘 ∈ {𝑍} (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) ↔ ∃𝑦 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)){⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩}))
141137, 140mpbid 223 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ {⟨𝑍, 𝑥⟩} ∈ X𝑘𝑋 (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))) → ∃𝑦 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)){⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩})
142 opex 5088 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑍, 𝑥⟩ ∈ V
143142sneqr 4523 . . . . . . . . . . . . . . . . . . . . . . . . 25 ({⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩} → ⟨𝑍, 𝑥⟩ = ⟨𝑍, 𝑦⟩)
144143adantl 473 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ {⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩}) → ⟨𝑍, 𝑥⟩ = ⟨𝑍, 𝑦⟩)
145 vex 3353 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝑥 ∈ V
146145a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑𝑥 ∈ V)
147 opthg 5101 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑍𝑉𝑥 ∈ V) → (⟨𝑍, 𝑥⟩ = ⟨𝑍, 𝑦⟩ ↔ (𝑍 = 𝑍𝑥 = 𝑦)))
1482, 146, 147syl2anc 579 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (⟨𝑍, 𝑥⟩ = ⟨𝑍, 𝑦⟩ ↔ (𝑍 = 𝑍𝑥 = 𝑦)))
149148adantr 472 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ {⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩}) → (⟨𝑍, 𝑥⟩ = ⟨𝑍, 𝑦⟩ ↔ (𝑍 = 𝑍𝑥 = 𝑦)))
150144, 149mpbid 223 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ {⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩}) → (𝑍 = 𝑍𝑥 = 𝑦))
151150simprd 489 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ {⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩}) → 𝑥 = 𝑦)
1521513adant2 1161 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑦 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) ∧ {⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩}) → 𝑥 = 𝑦)
153 simp2 1167 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑦 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) ∧ {⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩}) → 𝑦 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))
154152, 153eqeltrd 2844 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑦 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) ∧ {⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩}) → 𝑥 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))
1551543exp 1148 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑦 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) → ({⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩} → 𝑥 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))))
156155adantr 472 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ {⟨𝑍, 𝑥⟩} ∈ X𝑘𝑋 (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))) → (𝑦 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) → ({⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩} → 𝑥 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))))
157156rexlimdv 3177 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ {⟨𝑍, 𝑥⟩} ∈ X𝑘𝑋 (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))) → (∃𝑦 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)){⟨𝑍, 𝑥⟩} = {⟨𝑍, 𝑦⟩} → 𝑥 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))
158141, 157mpd 15 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ {⟨𝑍, 𝑥⟩} ∈ X𝑘𝑋 (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))) → 𝑥 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))
159158ex 401 . . . . . . . . . . . . . . 15 (𝜑 → ({⟨𝑍, 𝑥⟩} ∈ X𝑘𝑋 (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) → 𝑥 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))
160159ad2antrr 717 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ ((𝐴𝑍)[,)(𝐵𝑍))) ∧ 𝑗 ∈ ℕ) → ({⟨𝑍, 𝑥⟩} ∈ X𝑘𝑋 (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) → 𝑥 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))
161160reximdva 3163 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ ((𝐴𝑍)[,)(𝐵𝑍))) → (∃𝑗 ∈ ℕ {⟨𝑍, 𝑥⟩} ∈ X𝑘𝑋 (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) → ∃𝑗 ∈ ℕ 𝑥 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))
162132, 161mpd 15 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ ((𝐴𝑍)[,)(𝐵𝑍))) → ∃𝑗 ∈ ℕ 𝑥 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))
163 eliun 4680 . . . . . . . . . . . 12 (𝑥 𝑗 ∈ ℕ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) ↔ ∃𝑗 ∈ ℕ 𝑥 ∈ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))
164162, 163sylibr 225 . . . . . . . . . . 11 ((𝜑𝑥 ∈ ((𝐴𝑍)[,)(𝐵𝑍))) → 𝑥 𝑗 ∈ ℕ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))
165164ralrimiva 3113 . . . . . . . . . 10 (𝜑 → ∀𝑥 ∈ ((𝐴𝑍)[,)(𝐵𝑍))𝑥 𝑗 ∈ ℕ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))
166 dfss3 3750 . . . . . . . . . 10 (((𝐴𝑍)[,)(𝐵𝑍)) ⊆ 𝑗 ∈ ℕ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) ↔ ∀𝑥 ∈ ((𝐴𝑍)[,)(𝐵𝑍))𝑥 𝑗 ∈ ℕ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))
167165, 166sylibr 225 . . . . . . . . 9 (𝜑 → ((𝐴𝑍)[,)(𝐵𝑍)) ⊆ 𝑗 ∈ ℕ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))
168 eqidd 2766 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ ℕ) → (𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍)) = (𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍)))
169 fveq2 6375 . . . . . . . . . . . . . . 15 (𝑗 = 𝑖 → (𝐶𝑗) = (𝐶𝑖))
170169fveq1d 6377 . . . . . . . . . . . . . 14 (𝑗 = 𝑖 → ((𝐶𝑗)‘𝑍) = ((𝐶𝑖)‘𝑍))
171170adantl 473 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ ℕ) ∧ 𝑗 = 𝑖) → ((𝐶𝑗)‘𝑍) = ((𝐶𝑖)‘𝑍))
172 simpr 477 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ ℕ) → 𝑖 ∈ ℕ)
173 fvexd 6390 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ ℕ) → ((𝐶𝑖)‘𝑍) ∈ V)
174168, 171, 172, 173fvmptd 6477 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ ℕ) → ((𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍))‘𝑖) = ((𝐶𝑖)‘𝑍))
175 eqidd 2766 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ ℕ) → (𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍)) = (𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍)))
176 fveq2 6375 . . . . . . . . . . . . . . 15 (𝑗 = 𝑖 → (𝐷𝑗) = (𝐷𝑖))
177176fveq1d 6377 . . . . . . . . . . . . . 14 (𝑗 = 𝑖 → ((𝐷𝑗)‘𝑍) = ((𝐷𝑖)‘𝑍))
178177adantl 473 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ ℕ) ∧ 𝑗 = 𝑖) → ((𝐷𝑗)‘𝑍) = ((𝐷𝑖)‘𝑍))
179 fvexd 6390 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ ℕ) → ((𝐷𝑖)‘𝑍) ∈ V)
180175, 178, 172, 179fvmptd 6477 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ ℕ) → ((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖) = ((𝐷𝑖)‘𝑍))
181174, 180oveq12d 6860 . . . . . . . . . . 11 ((𝜑𝑖 ∈ ℕ) → (((𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍))‘𝑖)[,)((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖)) = (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)))
182181iuneq2dv 4698 . . . . . . . . . 10 (𝜑 𝑖 ∈ ℕ (((𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍))‘𝑖)[,)((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖)) = 𝑖 ∈ ℕ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)))
183170, 177oveq12d 6860 . . . . . . . . . . . . 13 (𝑗 = 𝑖 → (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) = (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)))
184183cbviunv 4715 . . . . . . . . . . . 12 𝑗 ∈ ℕ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) = 𝑖 ∈ ℕ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍))
185184eqcomi 2774 . . . . . . . . . . 11 𝑖 ∈ ℕ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)) = 𝑗 ∈ ℕ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))
186185a1i 11 . . . . . . . . . 10 (𝜑 𝑖 ∈ ℕ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)) = 𝑗 ∈ ℕ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))
187182, 186eqtr2d 2800 . . . . . . . . 9 (𝜑 𝑗 ∈ ℕ (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) = 𝑖 ∈ ℕ (((𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍))‘𝑖)[,)((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖)))
188167, 187sseqtrd 3801 . . . . . . . 8 (𝜑 → ((𝐴𝑍)[,)(𝐵𝑍)) ⊆ 𝑖 ∈ ℕ (((𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍))‘𝑖)[,)((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖)))
189188ad2antrr 717 . . . . . . 7 (((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) ∈ ℝ) → ((𝐴𝑍)[,)(𝐵𝑍)) ⊆ 𝑖 ∈ ℕ (((𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍))‘𝑖)[,)((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖)))
190 fvex 6388 . . . . . . . . . . . . . . 15 ((𝐶𝑖)‘𝑍) ∈ V
191170, 83, 190fvmpt 6471 . . . . . . . . . . . . . 14 (𝑖 ∈ ℕ → ((𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍))‘𝑖) = ((𝐶𝑖)‘𝑍))
192 fvex 6388 . . . . . . . . . . . . . . 15 ((𝐷𝑖)‘𝑍) ∈ V
193177, 86, 192fvmpt 6471 . . . . . . . . . . . . . 14 (𝑖 ∈ ℕ → ((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖) = ((𝐷𝑖)‘𝑍))
194191, 193oveq12d 6860 . . . . . . . . . . . . 13 (𝑖 ∈ ℕ → (((𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍))‘𝑖)[,)((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖)) = (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)))
195194fveq2d 6379 . . . . . . . . . . . 12 (𝑖 ∈ ℕ → (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍))‘𝑖)[,)((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖))) = (vol‘(((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍))))
196195mpteq2ia 4899 . . . . . . . . . . 11 (𝑖 ∈ ℕ ↦ (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍))‘𝑖)[,)((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖)))) = (𝑖 ∈ ℕ ↦ (vol‘(((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍))))
197 eqcom 2772 . . . . . . . . . . . . . . . 16 (𝑗 = 𝑖𝑖 = 𝑗)
198197imbi1i 340 . . . . . . . . . . . . . . 15 ((𝑗 = 𝑖 → (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) = (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍))) ↔ (𝑖 = 𝑗 → (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) = (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍))))
199 eqcom 2772 . . . . . . . . . . . . . . . 16 ((((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) = (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)) ↔ (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)) = (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))
200199imbi2i 327 . . . . . . . . . . . . . . 15 ((𝑖 = 𝑗 → (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) = (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍))) ↔ (𝑖 = 𝑗 → (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)) = (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))
201198, 200bitri 266 . . . . . . . . . . . . . 14 ((𝑗 = 𝑖 → (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)) = (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍))) ↔ (𝑖 = 𝑗 → (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)) = (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))
202183, 201mpbi 221 . . . . . . . . . . . . 13 (𝑖 = 𝑗 → (((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)) = (((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))
203202fveq2d 6379 . . . . . . . . . . . 12 (𝑖 = 𝑗 → (vol‘(((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍))) = (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))
204203cbvmptv 4909 . . . . . . . . . . 11 (𝑖 ∈ ℕ ↦ (vol‘(((𝐶𝑖)‘𝑍)[,)((𝐷𝑖)‘𝑍)))) = (𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))
205196, 204eqtri 2787 . . . . . . . . . 10 (𝑖 ∈ ℕ ↦ (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍))‘𝑖)[,)((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖)))) = (𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))
206205fveq2i 6378 . . . . . . . . 9 ^‘(𝑖 ∈ ℕ ↦ (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍))‘𝑖)[,)((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖))))) = (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))))
207206a1i 11 . . . . . . . 8 (((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) ∈ ℝ) → (Σ^‘(𝑖 ∈ ℕ ↦ (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍))‘𝑖)[,)((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖))))) = (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))))
208 simpr 477 . . . . . . . 8 (((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) ∈ ℝ) → (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) ∈ ℝ)
209207, 208eqeltrd 2844 . . . . . . 7 (((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) ∈ ℝ) → (Σ^‘(𝑖 ∈ ℕ ↦ (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍))‘𝑖)[,)((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖))))) ∈ ℝ)
210 oveq1 6849 . . . . . . . . 9 (𝑤 = 𝑧 → (𝑤 − (𝐴𝑍)) = (𝑧 − (𝐴𝑍)))
211193breq1d 4819 . . . . . . . . . . . . . . . . 17 (𝑖 ∈ ℕ → (((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖) ≤ 𝑧 ↔ ((𝐷𝑖)‘𝑍) ≤ 𝑧))
212211, 193ifbieq1d 4266 . . . . . . . . . . . . . . . 16 (𝑖 ∈ ℕ → if(((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖) ≤ 𝑧, ((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖), 𝑧) = if(((𝐷𝑖)‘𝑍) ≤ 𝑧, ((𝐷𝑖)‘𝑍), 𝑧))
213191, 212oveq12d 6860 . . . . . . . . . . . . . . 15 (𝑖 ∈ ℕ → (((𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍))‘𝑖)[,)if(((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖) ≤ 𝑧, ((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖), 𝑧)) = (((𝐶𝑖)‘𝑍)[,)if(((𝐷𝑖)‘𝑍) ≤ 𝑧, ((𝐷𝑖)‘𝑍), 𝑧)))
214213fveq2d 6379 . . . . . . . . . . . . . 14 (𝑖 ∈ ℕ → (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍))‘𝑖)[,)if(((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖) ≤ 𝑧, ((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖), 𝑧))) = (vol‘(((𝐶𝑖)‘𝑍)[,)if(((𝐷𝑖)‘𝑍) ≤ 𝑧, ((𝐷𝑖)‘𝑍), 𝑧))))
215214mpteq2ia 4899 . . . . . . . . . . . . 13 (𝑖 ∈ ℕ ↦ (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍))‘𝑖)[,)if(((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖) ≤ 𝑧, ((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖), 𝑧)))) = (𝑖 ∈ ℕ ↦ (vol‘(((𝐶𝑖)‘𝑍)[,)if(((𝐷𝑖)‘𝑍) ≤ 𝑧, ((𝐷𝑖)‘𝑍), 𝑧))))
216 fveq2 6375 . . . . . . . . . . . . . . . . 17 (𝑖 = → (𝐶𝑖) = (𝐶))
217216fveq1d 6377 . . . . . . . . . . . . . . . 16 (𝑖 = → ((𝐶𝑖)‘𝑍) = ((𝐶)‘𝑍))
218 fveq2 6375 . . . . . . . . . . . . . . . . . . 19 (𝑖 = → (𝐷𝑖) = (𝐷))
219218fveq1d 6377 . . . . . . . . . . . . . . . . . 18 (𝑖 = → ((𝐷𝑖)‘𝑍) = ((𝐷)‘𝑍))
220219breq1d 4819 . . . . . . . . . . . . . . . . 17 (𝑖 = → (((𝐷𝑖)‘𝑍) ≤ 𝑧 ↔ ((𝐷)‘𝑍) ≤ 𝑧))
221220, 219ifbieq1d 4266 . . . . . . . . . . . . . . . 16 (𝑖 = → if(((𝐷𝑖)‘𝑍) ≤ 𝑧, ((𝐷𝑖)‘𝑍), 𝑧) = if(((𝐷)‘𝑍) ≤ 𝑧, ((𝐷)‘𝑍), 𝑧))
222217, 221oveq12d 6860 . . . . . . . . . . . . . . 15 (𝑖 = → (((𝐶𝑖)‘𝑍)[,)if(((𝐷𝑖)‘𝑍) ≤ 𝑧, ((𝐷𝑖)‘𝑍), 𝑧)) = (((𝐶)‘𝑍)[,)if(((𝐷)‘𝑍) ≤ 𝑧, ((𝐷)‘𝑍), 𝑧)))
223222fveq2d 6379 . . . . . . . . . . . . . 14 (𝑖 = → (vol‘(((𝐶𝑖)‘𝑍)[,)if(((𝐷𝑖)‘𝑍) ≤ 𝑧, ((𝐷𝑖)‘𝑍), 𝑧))) = (vol‘(((𝐶)‘𝑍)[,)if(((𝐷)‘𝑍) ≤ 𝑧, ((𝐷)‘𝑍), 𝑧))))
224223cbvmptv 4909 . . . . . . . . . . . . 13 (𝑖 ∈ ℕ ↦ (vol‘(((𝐶𝑖)‘𝑍)[,)if(((𝐷𝑖)‘𝑍) ≤ 𝑧, ((𝐷𝑖)‘𝑍), 𝑧)))) = ( ∈ ℕ ↦ (vol‘(((𝐶)‘𝑍)[,)if(((𝐷)‘𝑍) ≤ 𝑧, ((𝐷)‘𝑍), 𝑧))))
225215, 224eqtri 2787 . . . . . . . . . . . 12 (𝑖 ∈ ℕ ↦ (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍))‘𝑖)[,)if(((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖) ≤ 𝑧, ((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖), 𝑧)))) = ( ∈ ℕ ↦ (vol‘(((𝐶)‘𝑍)[,)if(((𝐷)‘𝑍) ≤ 𝑧, ((𝐷)‘𝑍), 𝑧))))
226225a1i 11 . . . . . . . . . . 11 (𝑤 = 𝑧 → (𝑖 ∈ ℕ ↦ (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍))‘𝑖)[,)if(((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖) ≤ 𝑧, ((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖), 𝑧)))) = ( ∈ ℕ ↦ (vol‘(((𝐶)‘𝑍)[,)if(((𝐷)‘𝑍) ≤ 𝑧, ((𝐷)‘𝑍), 𝑧)))))
227 breq2 4813 . . . . . . . . . . . . . . . 16 (𝑤 = 𝑧 → (((𝐷)‘𝑍) ≤ 𝑤 ↔ ((𝐷)‘𝑍) ≤ 𝑧))
228 id 22 . . . . . . . . . . . . . . . 16 (𝑤 = 𝑧𝑤 = 𝑧)
229227, 228ifbieq2d 4268 . . . . . . . . . . . . . . 15 (𝑤 = 𝑧 → if(((𝐷)‘𝑍) ≤ 𝑤, ((𝐷)‘𝑍), 𝑤) = if(((𝐷)‘𝑍) ≤ 𝑧, ((𝐷)‘𝑍), 𝑧))
230229eqcomd 2771 . . . . . . . . . . . . . 14 (𝑤 = 𝑧 → if(((𝐷)‘𝑍) ≤ 𝑧, ((𝐷)‘𝑍), 𝑧) = if(((𝐷)‘𝑍) ≤ 𝑤, ((𝐷)‘𝑍), 𝑤))
231230oveq2d 6858 . . . . . . . . . . . . 13 (𝑤 = 𝑧 → (((𝐶)‘𝑍)[,)if(((𝐷)‘𝑍) ≤ 𝑧, ((𝐷)‘𝑍), 𝑧)) = (((𝐶)‘𝑍)[,)if(((𝐷)‘𝑍) ≤ 𝑤, ((𝐷)‘𝑍), 𝑤)))
232231fveq2d 6379 . . . . . . . . . . . 12 (𝑤 = 𝑧 → (vol‘(((𝐶)‘𝑍)[,)if(((𝐷)‘𝑍) ≤ 𝑧, ((𝐷)‘𝑍), 𝑧))) = (vol‘(((𝐶)‘𝑍)[,)if(((𝐷)‘𝑍) ≤ 𝑤, ((𝐷)‘𝑍), 𝑤))))
233232mpteq2dv 4904 . . . . . . . . . . 11 (𝑤 = 𝑧 → ( ∈ ℕ ↦ (vol‘(((𝐶)‘𝑍)[,)if(((𝐷)‘𝑍) ≤ 𝑧, ((𝐷)‘𝑍), 𝑧)))) = ( ∈ ℕ ↦ (vol‘(((𝐶)‘𝑍)[,)if(((𝐷)‘𝑍) ≤ 𝑤, ((𝐷)‘𝑍), 𝑤)))))
234226, 233eqtr2d 2800 . . . . . . . . . 10 (𝑤 = 𝑧 → ( ∈ ℕ ↦ (vol‘(((𝐶)‘𝑍)[,)if(((𝐷)‘𝑍) ≤ 𝑤, ((𝐷)‘𝑍), 𝑤)))) = (𝑖 ∈ ℕ ↦ (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍))‘𝑖)[,)if(((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖) ≤ 𝑧, ((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖), 𝑧)))))
235234fveq2d 6379 . . . . . . . . 9 (𝑤 = 𝑧 → (Σ^‘( ∈ ℕ ↦ (vol‘(((𝐶)‘𝑍)[,)if(((𝐷)‘𝑍) ≤ 𝑤, ((𝐷)‘𝑍), 𝑤))))) = (Σ^‘(𝑖 ∈ ℕ ↦ (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍))‘𝑖)[,)if(((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖) ≤ 𝑧, ((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖), 𝑧))))))
236210, 235breq12d 4822 . . . . . . . 8 (𝑤 = 𝑧 → ((𝑤 − (𝐴𝑍)) ≤ (Σ^‘( ∈ ℕ ↦ (vol‘(((𝐶)‘𝑍)[,)if(((𝐷)‘𝑍) ≤ 𝑤, ((𝐷)‘𝑍), 𝑤))))) ↔ (𝑧 − (𝐴𝑍)) ≤ (Σ^‘(𝑖 ∈ ℕ ↦ (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍))‘𝑖)[,)if(((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖) ≤ 𝑧, ((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖), 𝑧)))))))
237236cbvrabv 3348 . . . . . . 7 {𝑤 ∈ ((𝐴𝑍)[,](𝐵𝑍)) ∣ (𝑤 − (𝐴𝑍)) ≤ (Σ^‘( ∈ ℕ ↦ (vol‘(((𝐶)‘𝑍)[,)if(((𝐷)‘𝑍) ≤ 𝑤, ((𝐷)‘𝑍), 𝑤)))))} = {𝑧 ∈ ((𝐴𝑍)[,](𝐵𝑍)) ∣ (𝑧 − (𝐴𝑍)) ≤ (Σ^‘(𝑖 ∈ ℕ ↦ (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍))‘𝑖)[,)if(((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖) ≤ 𝑧, ((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖), 𝑧)))))}
238 eqid 2765 . . . . . . 7 sup({𝑤 ∈ ((𝐴𝑍)[,](𝐵𝑍)) ∣ (𝑤 − (𝐴𝑍)) ≤ (Σ^‘( ∈ ℕ ↦ (vol‘(((𝐶)‘𝑍)[,)if(((𝐷)‘𝑍) ≤ 𝑤, ((𝐷)‘𝑍), 𝑤)))))}, ℝ, < ) = sup({𝑤 ∈ ((𝐴𝑍)[,](𝐵𝑍)) ∣ (𝑤 − (𝐴𝑍)) ≤ (Σ^‘( ∈ ℕ ↦ (vol‘(((𝐶)‘𝑍)[,)if(((𝐷)‘𝑍) ≤ 𝑤, ((𝐷)‘𝑍), 𝑤)))))}, ℝ, < )
23980, 81, 82, 85, 88, 189, 209, 237, 238hoidmv1lelem3 41379 . . . . . 6 (((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) ∈ ℝ) → ((𝐵𝑍) − (𝐴𝑍)) ≤ (Σ^‘(𝑖 ∈ ℕ ↦ (vol‘(((𝑗 ∈ ℕ ↦ ((𝐶𝑗)‘𝑍))‘𝑖)[,)((𝑗 ∈ ℕ ↦ ((𝐷𝑗)‘𝑍))‘𝑖))))))
240239, 207breqtrd 4835 . . . . 5 (((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) ∈ ℝ) → ((𝐵𝑍) − (𝐴𝑍)) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))))
24121, 79, 240syl2anc 579 . . . 4 (((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) ∧ ¬ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))) = +∞) → ((𝐵𝑍) − (𝐴𝑍)) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))))
24220, 241pm2.61dan 847 . . 3 ((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) → ((𝐵𝑍) − (𝐴𝑍)) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))))
24325, 29, 31, 8, 1hoidmvn0val 41370 . . . . . . 7 (𝜑 → (𝐴(𝐿𝑋)𝐵) = ∏𝑘𝑋 (vol‘((𝐴𝑘)[,)(𝐵𝑘))))
24426prodeq1d 14936 . . . . . . 7 (𝜑 → ∏𝑘𝑋 (vol‘((𝐴𝑘)[,)(𝐵𝑘))) = ∏𝑘 ∈ {𝑍} (vol‘((𝐴𝑘)[,)(𝐵𝑘))))
245 volicore 41367 . . . . . . . . . 10 (((𝐴𝑍) ∈ ℝ ∧ (𝐵𝑍) ∈ ℝ) → (vol‘((𝐴𝑍)[,)(𝐵𝑍))) ∈ ℝ)
2469, 7, 245syl2anc 579 . . . . . . . . 9 (𝜑 → (vol‘((𝐴𝑍)[,)(𝐵𝑍))) ∈ ℝ)
247246recnd 10322 . . . . . . . 8 (𝜑 → (vol‘((𝐴𝑍)[,)(𝐵𝑍))) ∈ ℂ)
248117, 119oveq12d 6860 . . . . . . . . . 10 (𝑘 = 𝑍 → ((𝐴𝑘)[,)(𝐵𝑘)) = ((𝐴𝑍)[,)(𝐵𝑍)))
249248fveq2d 6379 . . . . . . . . 9 (𝑘 = 𝑍 → (vol‘((𝐴𝑘)[,)(𝐵𝑘))) = (vol‘((𝐴𝑍)[,)(𝐵𝑍))))
250249prodsn 14977 . . . . . . . 8 ((𝑍𝑉 ∧ (vol‘((𝐴𝑍)[,)(𝐵𝑍))) ∈ ℂ) → ∏𝑘 ∈ {𝑍} (vol‘((𝐴𝑘)[,)(𝐵𝑘))) = (vol‘((𝐴𝑍)[,)(𝐵𝑍))))
2512, 247, 250syl2anc 579 . . . . . . 7 (𝜑 → ∏𝑘 ∈ {𝑍} (vol‘((𝐴𝑘)[,)(𝐵𝑘))) = (vol‘((𝐴𝑍)[,)(𝐵𝑍))))
252243, 244, 2513eqtrd 2803 . . . . . 6 (𝜑 → (𝐴(𝐿𝑋)𝐵) = (vol‘((𝐴𝑍)[,)(𝐵𝑍))))
253252adantr 472 . . . . 5 ((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) → (𝐴(𝐿𝑋)𝐵) = (vol‘((𝐴𝑍)[,)(𝐵𝑍))))
254 volico 40769 . . . . . . 7 (((𝐴𝑍) ∈ ℝ ∧ (𝐵𝑍) ∈ ℝ) → (vol‘((𝐴𝑍)[,)(𝐵𝑍))) = if((𝐴𝑍) < (𝐵𝑍), ((𝐵𝑍) − (𝐴𝑍)), 0))
2559, 7, 254syl2anc 579 . . . . . 6 (𝜑 → (vol‘((𝐴𝑍)[,)(𝐵𝑍))) = if((𝐴𝑍) < (𝐵𝑍), ((𝐵𝑍) − (𝐴𝑍)), 0))
256255adantr 472 . . . . 5 ((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) → (vol‘((𝐴𝑍)[,)(𝐵𝑍))) = if((𝐴𝑍) < (𝐵𝑍), ((𝐵𝑍) − (𝐴𝑍)), 0))
257 iftrue 4249 . . . . . 6 ((𝐴𝑍) < (𝐵𝑍) → if((𝐴𝑍) < (𝐵𝑍), ((𝐵𝑍) − (𝐴𝑍)), 0) = ((𝐵𝑍) − (𝐴𝑍)))
258257adantl 473 . . . . 5 ((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) → if((𝐴𝑍) < (𝐵𝑍), ((𝐵𝑍) − (𝐴𝑍)), 0) = ((𝐵𝑍) − (𝐴𝑍)))
259253, 256, 2583eqtrd 2803 . . . 4 ((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) → (𝐴(𝐿𝑋)𝐵) = ((𝐵𝑍) − (𝐴𝑍)))
26058fveq2d 6379 . . . . 5 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗)))) = (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))))
261260adantr 472 . . . 4 ((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗)))) = (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍))))))
262259, 261breq12d 4822 . . 3 ((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) → ((𝐴(𝐿𝑋)𝐵) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗)))) ↔ ((𝐵𝑍) − (𝐴𝑍)) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘(((𝐶𝑗)‘𝑍)[,)((𝐷𝑗)‘𝑍)))))))
263242, 262mpbird 248 . 2 ((𝜑 ∧ (𝐴𝑍) < (𝐵𝑍)) → (𝐴(𝐿𝑋)𝐵) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗)))))
264243adantr 472 . . . 4 ((𝜑 ∧ ¬ (𝐴𝑍) < (𝐵𝑍)) → (𝐴(𝐿𝑋)𝐵) = ∏𝑘𝑋 (vol‘((𝐴𝑘)[,)(𝐵𝑘))))
265244adantr 472 . . . 4 ((𝜑 ∧ ¬ (𝐴𝑍) < (𝐵𝑍)) → ∏𝑘𝑋 (vol‘((𝐴𝑘)[,)(𝐵𝑘))) = ∏𝑘 ∈ {𝑍} (vol‘((𝐴𝑘)[,)(𝐵𝑘))))
266251adantr 472 . . . . 5 ((𝜑 ∧ ¬ (𝐴𝑍) < (𝐵𝑍)) → ∏𝑘 ∈ {𝑍} (vol‘((𝐴𝑘)[,)(𝐵𝑘))) = (vol‘((𝐴𝑍)[,)(𝐵𝑍))))
267255adantr 472 . . . . 5 ((𝜑 ∧ ¬ (𝐴𝑍) < (𝐵𝑍)) → (vol‘((𝐴𝑍)[,)(𝐵𝑍))) = if((𝐴𝑍) < (𝐵𝑍), ((𝐵𝑍) − (𝐴𝑍)), 0))
268 iffalse 4252 . . . . . 6 (¬ (𝐴𝑍) < (𝐵𝑍) → if((𝐴𝑍) < (𝐵𝑍), ((𝐵𝑍) − (𝐴𝑍)), 0) = 0)
269268adantl 473 . . . . 5 ((𝜑 ∧ ¬ (𝐴𝑍) < (𝐵𝑍)) → if((𝐴𝑍) < (𝐵𝑍), ((𝐵𝑍) − (𝐴𝑍)), 0) = 0)
270266, 267, 2693eqtrd 2803 . . . 4 ((𝜑 ∧ ¬ (𝐴𝑍) < (𝐵𝑍)) → ∏𝑘 ∈ {𝑍} (vol‘((𝐴𝑘)[,)(𝐵𝑘))) = 0)
271264, 265, 2703eqtrd 2803 . . 3 ((𝜑 ∧ ¬ (𝐴𝑍) < (𝐵𝑍)) → (𝐴(𝐿𝑋)𝐵) = 0)
27223a1i 11 . . . . 5 (𝜑 → ℕ ∈ V)
273272, 75sge0ge0 41170 . . . 4 (𝜑 → 0 ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗)))))
274273adantr 472 . . 3 ((𝜑 ∧ ¬ (𝐴𝑍) < (𝐵𝑍)) → 0 ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗)))))
275271, 274eqbrtrd 4831 . 2 ((𝜑 ∧ ¬ (𝐴𝑍) < (𝐵𝑍)) → (𝐴(𝐿𝑋)𝐵) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗)))))
276263, 275pm2.61dan 847 1 (𝜑 → (𝐴(𝐿𝑋)𝐵) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶𝑗)(𝐿𝑋)(𝐷𝑗)))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384  w3a 1107   = wceq 1652  wcel 2155  wne 2937  wral 3055  wrex 3056  {crab 3059  Vcvv 3350  wss 3732  c0 4079  ifcif 4243  {csn 4334  cop 4340   ciun 4676   class class class wbr 4809  cmpt 4888  wf 6064  cfv 6068  (class class class)co 6842  cmpt2 6844  𝑚 cmap 8060  Xcixp 8113  Fincfn 8160  supcsup 8553  cc 10187  cr 10188  0cc0 10189  +∞cpnf 10325  *cxr 10327   < clt 10328  cle 10329  cmin 10520  cn 11274  [,)cico 12379  [,]cicc 12380  cprod 14920  volcvol 23521  Σ^csumge0 41148
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2069  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-rep 4930  ax-sep 4941  ax-nul 4949  ax-pow 5001  ax-pr 5062  ax-un 7147  ax-inf2 8753  ax-cnex 10245  ax-resscn 10246  ax-1cn 10247  ax-icn 10248  ax-addcl 10249  ax-addrcl 10250  ax-mulcl 10251  ax-mulrcl 10252  ax-mulcom 10253  ax-addass 10254  ax-mulass 10255  ax-distr 10256  ax-i2m1 10257  ax-1ne0 10258  ax-1rid 10259  ax-rnegex 10260  ax-rrecex 10261  ax-cnre 10262  ax-pre-lttri 10263  ax-pre-lttrn 10264  ax-pre-ltadd 10265  ax-pre-mulgt0 10266  ax-pre-sup 10267
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-fal 1666  df-ex 1875  df-nf 1879  df-sb 2062  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-nel 3041  df-ral 3060  df-rex 3061  df-reu 3062  df-rmo 3063  df-rab 3064  df-v 3352  df-sbc 3597  df-csb 3692  df-dif 3735  df-un 3737  df-in 3739  df-ss 3746  df-pss 3748  df-nul 4080  df-if 4244  df-pw 4317  df-sn 4335  df-pr 4337  df-tp 4339  df-op 4341  df-uni 4595  df-int 4634  df-iun 4678  df-br 4810  df-opab 4872  df-mpt 4889  df-tr 4912  df-id 5185  df-eprel 5190  df-po 5198  df-so 5199  df-fr 5236  df-se 5237  df-we 5238  df-xp 5283  df-rel 5284  df-cnv 5285  df-co 5286  df-dm 5287  df-rn 5288  df-res 5289  df-ima 5290  df-pred 5865  df-ord 5911  df-on 5912  df-lim 5913  df-suc 5914  df-iota 6031  df-fun 6070  df-fn 6071  df-f 6072  df-f1 6073  df-fo 6074  df-f1o 6075  df-fv 6076  df-isom 6077  df-riota 6803  df-ov 6845  df-oprab 6846  df-mpt2 6847  df-of 7095  df-om 7264  df-1st 7366  df-2nd 7367  df-wrecs 7610  df-recs 7672  df-rdg 7710  df-1o 7764  df-2o 7765  df-oadd 7768  df-er 7947  df-map 8062  df-pm 8063  df-ixp 8114  df-en 8161  df-dom 8162  df-sdom 8163  df-fin 8164  df-fi 8524  df-sup 8555  df-inf 8556  df-oi 8622  df-card 9016  df-cda 9243  df-pnf 10330  df-mnf 10331  df-xr 10332  df-ltxr 10333  df-le 10334  df-sub 10522  df-neg 10523  df-div 10939  df-nn 11275  df-2 11335  df-3 11336  df-n0 11539  df-z 11625  df-uz 11887  df-q 11990  df-rp 12029  df-xneg 12146  df-xadd 12147  df-xmul 12148  df-ioo 12381  df-ico 12383  df-icc 12384  df-fz 12534  df-fzo 12674  df-fl 12801  df-seq 13009  df-exp 13068  df-hash 13322  df-cj 14126  df-re 14127  df-im 14128  df-sqrt 14262  df-abs 14263  df-clim 14506  df-rlim 14507  df-sum 14704  df-prod 14921  df-rest 16351  df-topgen 16372  df-psmet 20011  df-xmet 20012  df-met 20013  df-bl 20014  df-mopn 20015  df-top 20978  df-topon 20995  df-bases 21030  df-cmp 21470  df-ovol 23522  df-vol 23523  df-sumge0 41149
This theorem is referenced by:  hoidmvle  41386
  Copyright terms: Public domain W3C validator