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

Theorem ovnsubaddlem1 41282
Description: The Lebesgue outer measure is subadditive. Proposition 115D (a)(iv) of [Fremlin1] p. 31 . (Contributed by Glauco Siliprandi, 11-Oct-2020.)
Hypotheses
Ref Expression
ovnsubaddlem1.x (𝜑𝑋 ∈ Fin)
ovnsubaddlem1.n0 (𝜑𝑋 ≠ ∅)
ovnsubaddlem1.a (𝜑𝐴:ℕ⟶𝒫 (ℝ ↑𝑚 𝑋))
ovnsubaddlem1.e (𝜑𝐸 ∈ ℝ+)
ovnsubaddlem1.z 𝑍 = (𝑎 ∈ 𝒫 (ℝ ↑𝑚 𝑋) ↦ {𝑧 ∈ ℝ* ∣ ∃𝑖 ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)(𝑎 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑖𝑗))‘𝑘) ∧ 𝑧 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘𝑋 (vol‘(([,) ∘ (𝑖𝑗))‘𝑘)))))})
ovnsubaddlem1.c 𝐶 = (𝑎 ∈ 𝒫 (ℝ ↑𝑚 𝑋) ↦ { ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∣ 𝑎 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘)})
ovnsubaddlem1.l 𝐿 = (𝑖 ∈ ((ℝ × ℝ) ↑𝑚 𝑋) ↦ ∏𝑘𝑋 (vol‘(([,) ∘ 𝑖)‘𝑘)))
ovnsubaddlem1.d 𝐷 = (𝑎 ∈ 𝒫 (ℝ ↑𝑚 𝑋) ↦ (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶𝑎) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘𝑎) +𝑒 𝑒)}))
ovnsubaddlem1.i ((𝜑𝑛 ∈ ℕ) → (𝐼𝑛) ∈ ((𝐷‘(𝐴𝑛))‘(𝐸 / (2↑𝑛))))
ovnsubaddlem1.f (𝜑𝐹:ℕ–1-1-onto→(ℕ × ℕ))
ovnsubaddlem1.g 𝐺 = (𝑚 ∈ ℕ ↦ ((𝐼‘(1st ‘(𝐹𝑚)))‘(2nd ‘(𝐹𝑚))))
Assertion
Ref Expression
ovnsubaddlem1 (𝜑 → ((voln*‘𝑋)‘ 𝑛 ∈ ℕ (𝐴𝑛)) ≤ ((Σ^‘(𝑛 ∈ ℕ ↦ ((voln*‘𝑋)‘(𝐴𝑛)))) +𝑒 𝐸))
Distinct variable groups:   𝐴,𝑎,𝑒,𝑖,𝑛   𝐴,,𝑎,𝑛   𝑧,𝐴,𝑎,𝑖,𝑛   𝐶,𝑎,𝑒,𝑖   𝐷,𝑛   𝑒,𝐸,𝑖,𝑛   𝐹,𝑎,𝑒,𝑖,𝑗,𝑚,𝑛   ,𝐹,𝑘,𝑎,𝑗,𝑚,𝑛   𝑖,𝑘,𝐺,𝑗,𝑚,𝑛   ,𝐼,𝑗,𝑘,𝑚,𝑛   𝑖,𝐼   𝐿,𝑎,𝑒,𝑖,𝑗,𝑚,𝑛   𝑋,𝑎,𝑒,𝑖,𝑗,𝑚,𝑛   ,𝑋,𝑘   𝑧,𝑋,𝑗,𝑘   𝜑,𝑎,𝑒,𝑖,𝑗,𝑚,𝑛   𝜑,𝑘
Allowed substitution hints:   𝜑(𝑧,)   𝐴(𝑗,𝑘,𝑚)   𝐶(𝑧,,𝑗,𝑘,𝑚,𝑛)   𝐷(𝑧,𝑒,,𝑖,𝑗,𝑘,𝑚,𝑎)   𝐸(𝑧,,𝑗,𝑘,𝑚,𝑎)   𝐹(𝑧)   𝐺(𝑧,𝑒,,𝑎)   𝐼(𝑧,𝑒,𝑎)   𝐿(𝑧,,𝑘)   𝑍(𝑧,𝑒,,𝑖,𝑗,𝑘,𝑚,𝑛,𝑎)

Proof of Theorem ovnsubaddlem1
Dummy variable 𝑝 is distinct from all other variables.
StepHypRef Expression
1 ovnsubaddlem1.x . . . 4 (𝜑𝑋 ∈ Fin)
2 ovnsubaddlem1.a . . . . . . . . 9 (𝜑𝐴:ℕ⟶𝒫 (ℝ ↑𝑚 𝑋))
32adantr 472 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → 𝐴:ℕ⟶𝒫 (ℝ ↑𝑚 𝑋))
4 simpr 479 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → 𝑛 ∈ ℕ)
53, 4ffvelrnd 6515 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → (𝐴𝑛) ∈ 𝒫 (ℝ ↑𝑚 𝑋))
6 elpwi 4304 . . . . . . 7 ((𝐴𝑛) ∈ 𝒫 (ℝ ↑𝑚 𝑋) → (𝐴𝑛) ⊆ (ℝ ↑𝑚 𝑋))
75, 6syl 17 . . . . . 6 ((𝜑𝑛 ∈ ℕ) → (𝐴𝑛) ⊆ (ℝ ↑𝑚 𝑋))
87ralrimiva 3096 . . . . 5 (𝜑 → ∀𝑛 ∈ ℕ (𝐴𝑛) ⊆ (ℝ ↑𝑚 𝑋))
9 iunss 4705 . . . . 5 ( 𝑛 ∈ ℕ (𝐴𝑛) ⊆ (ℝ ↑𝑚 𝑋) ↔ ∀𝑛 ∈ ℕ (𝐴𝑛) ⊆ (ℝ ↑𝑚 𝑋))
108, 9sylibr 224 . . . 4 (𝜑 𝑛 ∈ ℕ (𝐴𝑛) ⊆ (ℝ ↑𝑚 𝑋))
111, 10ovnxrcl 41281 . . 3 (𝜑 → ((voln*‘𝑋)‘ 𝑛 ∈ ℕ (𝐴𝑛)) ∈ ℝ*)
12 nfv 1984 . . . 4 𝑚𝜑
13 nnex 11210 . . . . 5 ℕ ∈ V
1413a1i 11 . . . 4 (𝜑 → ℕ ∈ V)
15 icossicc 12445 . . . . 5 (0[,)+∞) ⊆ (0[,]+∞)
16 nfv 1984 . . . . . 6 𝑘(𝜑𝑚 ∈ ℕ)
17 simpl 474 . . . . . . 7 ((𝜑𝑚 ∈ ℕ) → 𝜑)
1817, 1syl 17 . . . . . 6 ((𝜑𝑚 ∈ ℕ) → 𝑋 ∈ Fin)
19 ovnsubaddlem1.l . . . . . 6 𝐿 = (𝑖 ∈ ((ℝ × ℝ) ↑𝑚 𝑋) ↦ ∏𝑘𝑋 (vol‘(([,) ∘ 𝑖)‘𝑘)))
20 ovnsubaddlem1.f . . . . . . . . . . . 12 (𝜑𝐹:ℕ–1-1-onto→(ℕ × ℕ))
21 f1of 6290 . . . . . . . . . . . 12 (𝐹:ℕ–1-1-onto→(ℕ × ℕ) → 𝐹:ℕ⟶(ℕ × ℕ))
2220, 21syl 17 . . . . . . . . . . 11 (𝜑𝐹:ℕ⟶(ℕ × ℕ))
2322adantr 472 . . . . . . . . . 10 ((𝜑𝑚 ∈ ℕ) → 𝐹:ℕ⟶(ℕ × ℕ))
24 simpr 479 . . . . . . . . . 10 ((𝜑𝑚 ∈ ℕ) → 𝑚 ∈ ℕ)
2523, 24ffvelrnd 6515 . . . . . . . . 9 ((𝜑𝑚 ∈ ℕ) → (𝐹𝑚) ∈ (ℕ × ℕ))
26 xp1st 7357 . . . . . . . . 9 ((𝐹𝑚) ∈ (ℕ × ℕ) → (1st ‘(𝐹𝑚)) ∈ ℕ)
2725, 26syl 17 . . . . . . . 8 ((𝜑𝑚 ∈ ℕ) → (1st ‘(𝐹𝑚)) ∈ ℕ)
28 xp2nd 7358 . . . . . . . . 9 ((𝐹𝑚) ∈ (ℕ × ℕ) → (2nd ‘(𝐹𝑚)) ∈ ℕ)
2925, 28syl 17 . . . . . . . 8 ((𝜑𝑚 ∈ ℕ) → (2nd ‘(𝐹𝑚)) ∈ ℕ)
30 fvex 6354 . . . . . . . . 9 (2nd ‘(𝐹𝑚)) ∈ V
31 eleq1 2819 . . . . . . . . . . 11 (𝑗 = (2nd ‘(𝐹𝑚)) → (𝑗 ∈ ℕ ↔ (2nd ‘(𝐹𝑚)) ∈ ℕ))
32313anbi3d 1546 . . . . . . . . . 10 (𝑗 = (2nd ‘(𝐹𝑚)) → ((𝜑 ∧ (1st ‘(𝐹𝑚)) ∈ ℕ ∧ 𝑗 ∈ ℕ) ↔ (𝜑 ∧ (1st ‘(𝐹𝑚)) ∈ ℕ ∧ (2nd ‘(𝐹𝑚)) ∈ ℕ)))
33 fveq2 6344 . . . . . . . . . . 11 (𝑗 = (2nd ‘(𝐹𝑚)) → ((𝐼‘(1st ‘(𝐹𝑚)))‘𝑗) = ((𝐼‘(1st ‘(𝐹𝑚)))‘(2nd ‘(𝐹𝑚))))
3433feq1d 6183 . . . . . . . . . 10 (𝑗 = (2nd ‘(𝐹𝑚)) → (((𝐼‘(1st ‘(𝐹𝑚)))‘𝑗):𝑋⟶(ℝ × ℝ) ↔ ((𝐼‘(1st ‘(𝐹𝑚)))‘(2nd ‘(𝐹𝑚))):𝑋⟶(ℝ × ℝ)))
3532, 34imbi12d 333 . . . . . . . . 9 (𝑗 = (2nd ‘(𝐹𝑚)) → (((𝜑 ∧ (1st ‘(𝐹𝑚)) ∈ ℕ ∧ 𝑗 ∈ ℕ) → ((𝐼‘(1st ‘(𝐹𝑚)))‘𝑗):𝑋⟶(ℝ × ℝ)) ↔ ((𝜑 ∧ (1st ‘(𝐹𝑚)) ∈ ℕ ∧ (2nd ‘(𝐹𝑚)) ∈ ℕ) → ((𝐼‘(1st ‘(𝐹𝑚)))‘(2nd ‘(𝐹𝑚))):𝑋⟶(ℝ × ℝ))))
36 fvex 6354 . . . . . . . . . 10 (1st ‘(𝐹𝑚)) ∈ V
37 eleq1 2819 . . . . . . . . . . . 12 (𝑛 = (1st ‘(𝐹𝑚)) → (𝑛 ∈ ℕ ↔ (1st ‘(𝐹𝑚)) ∈ ℕ))
38373anbi2d 1545 . . . . . . . . . . 11 (𝑛 = (1st ‘(𝐹𝑚)) → ((𝜑𝑛 ∈ ℕ ∧ 𝑗 ∈ ℕ) ↔ (𝜑 ∧ (1st ‘(𝐹𝑚)) ∈ ℕ ∧ 𝑗 ∈ ℕ)))
39 fveq2 6344 . . . . . . . . . . . . 13 (𝑛 = (1st ‘(𝐹𝑚)) → (𝐼𝑛) = (𝐼‘(1st ‘(𝐹𝑚))))
4039fveq1d 6346 . . . . . . . . . . . 12 (𝑛 = (1st ‘(𝐹𝑚)) → ((𝐼𝑛)‘𝑗) = ((𝐼‘(1st ‘(𝐹𝑚)))‘𝑗))
4140feq1d 6183 . . . . . . . . . . 11 (𝑛 = (1st ‘(𝐹𝑚)) → (((𝐼𝑛)‘𝑗):𝑋⟶(ℝ × ℝ) ↔ ((𝐼‘(1st ‘(𝐹𝑚)))‘𝑗):𝑋⟶(ℝ × ℝ)))
4238, 41imbi12d 333 . . . . . . . . . 10 (𝑛 = (1st ‘(𝐹𝑚)) → (((𝜑𝑛 ∈ ℕ ∧ 𝑗 ∈ ℕ) → ((𝐼𝑛)‘𝑗):𝑋⟶(ℝ × ℝ)) ↔ ((𝜑 ∧ (1st ‘(𝐹𝑚)) ∈ ℕ ∧ 𝑗 ∈ ℕ) → ((𝐼‘(1st ‘(𝐹𝑚)))‘𝑗):𝑋⟶(ℝ × ℝ))))
43 ovnsubaddlem1.c . . . . . . . . . . . . . . . . . . . 20 𝐶 = (𝑎 ∈ 𝒫 (ℝ ↑𝑚 𝑋) ↦ { ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∣ 𝑎 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘)})
4443a1i 11 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑛 ∈ ℕ) → 𝐶 = (𝑎 ∈ 𝒫 (ℝ ↑𝑚 𝑋) ↦ { ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∣ 𝑎 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘)}))
45 sseq1 3759 . . . . . . . . . . . . . . . . . . . . 21 (𝑎 = (𝐴𝑛) → (𝑎 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘) ↔ (𝐴𝑛) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘)))
4645rabbidv 3321 . . . . . . . . . . . . . . . . . . . 20 (𝑎 = (𝐴𝑛) → { ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∣ 𝑎 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘)} = { ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∣ (𝐴𝑛) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘)})
4746adantl 473 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑛 ∈ ℕ) ∧ 𝑎 = (𝐴𝑛)) → { ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∣ 𝑎 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘)} = { ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∣ (𝐴𝑛) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘)})
48 ovex 6833 . . . . . . . . . . . . . . . . . . . . 21 (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∈ V
4948rabex 4956 . . . . . . . . . . . . . . . . . . . 20 { ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∣ (𝐴𝑛) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘)} ∈ V
5049a1i 11 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑛 ∈ ℕ) → { ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∣ (𝐴𝑛) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘)} ∈ V)
5144, 47, 5, 50fvmptd 6442 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑛 ∈ ℕ) → (𝐶‘(𝐴𝑛)) = { ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∣ (𝐴𝑛) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘)})
52 ssrab2 3820 . . . . . . . . . . . . . . . . . . 19 { ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∣ (𝐴𝑛) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘)} ⊆ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)
5352a1i 11 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑛 ∈ ℕ) → { ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∣ (𝐴𝑛) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘)} ⊆ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ))
5451, 53eqsstrd 3772 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛 ∈ ℕ) → (𝐶‘(𝐴𝑛)) ⊆ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ))
55 ovnsubaddlem1.d . . . . . . . . . . . . . . . . . . . . . 22 𝐷 = (𝑎 ∈ 𝒫 (ℝ ↑𝑚 𝑋) ↦ (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶𝑎) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘𝑎) +𝑒 𝑒)}))
5655a1i 11 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑛 ∈ ℕ) → 𝐷 = (𝑎 ∈ 𝒫 (ℝ ↑𝑚 𝑋) ↦ (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶𝑎) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘𝑎) +𝑒 𝑒)})))
57 fveq2 6344 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑎 = (𝐴𝑛) → (𝐶𝑎) = (𝐶‘(𝐴𝑛)))
5857eleq2d 2817 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑎 = (𝐴𝑛) → (𝑖 ∈ (𝐶𝑎) ↔ 𝑖 ∈ (𝐶‘(𝐴𝑛))))
59 fveq2 6344 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑎 = (𝐴𝑛) → ((voln*‘𝑋)‘𝑎) = ((voln*‘𝑋)‘(𝐴𝑛)))
6059oveq1d 6820 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑎 = (𝐴𝑛) → (((voln*‘𝑋)‘𝑎) +𝑒 𝑒) = (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 𝑒))
6160breq2d 4808 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑎 = (𝐴𝑛) → ((Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘𝑎) +𝑒 𝑒) ↔ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 𝑒)))
6258, 61anbi12d 749 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑎 = (𝐴𝑛) → ((𝑖 ∈ (𝐶𝑎) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘𝑎) +𝑒 𝑒)) ↔ (𝑖 ∈ (𝐶‘(𝐴𝑛)) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 𝑒))))
6362rabbidva2 3318 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑎 = (𝐴𝑛) → {𝑖 ∈ (𝐶𝑎) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘𝑎) +𝑒 𝑒)} = {𝑖 ∈ (𝐶‘(𝐴𝑛)) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 𝑒)})
6463mpteq2dv 4889 . . . . . . . . . . . . . . . . . . . . . 22 (𝑎 = (𝐴𝑛) → (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶𝑎) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘𝑎) +𝑒 𝑒)}) = (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶‘(𝐴𝑛)) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 𝑒)}))
6564adantl 473 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑛 ∈ ℕ) ∧ 𝑎 = (𝐴𝑛)) → (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶𝑎) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘𝑎) +𝑒 𝑒)}) = (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶‘(𝐴𝑛)) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 𝑒)}))
66 rpex 40052 . . . . . . . . . . . . . . . . . . . . . . 23 + ∈ V
6766mptex 6642 . . . . . . . . . . . . . . . . . . . . . 22 (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶‘(𝐴𝑛)) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 𝑒)}) ∈ V
6867a1i 11 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑛 ∈ ℕ) → (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶‘(𝐴𝑛)) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 𝑒)}) ∈ V)
6956, 65, 5, 68fvmptd 6442 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑛 ∈ ℕ) → (𝐷‘(𝐴𝑛)) = (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶‘(𝐴𝑛)) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 𝑒)}))
70 oveq2 6813 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑒 = (𝐸 / (2↑𝑛)) → (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 𝑒) = (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛))))
7170breq2d 4808 . . . . . . . . . . . . . . . . . . . . . 22 (𝑒 = (𝐸 / (2↑𝑛)) → ((Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 𝑒) ↔ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛)))))
7271rabbidv 3321 . . . . . . . . . . . . . . . . . . . . 21 (𝑒 = (𝐸 / (2↑𝑛)) → {𝑖 ∈ (𝐶‘(𝐴𝑛)) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 𝑒)} = {𝑖 ∈ (𝐶‘(𝐴𝑛)) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛)))})
7372adantl 473 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑛 ∈ ℕ) ∧ 𝑒 = (𝐸 / (2↑𝑛))) → {𝑖 ∈ (𝐶‘(𝐴𝑛)) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 𝑒)} = {𝑖 ∈ (𝐶‘(𝐴𝑛)) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛)))})
74 ovnsubaddlem1.e . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝐸 ∈ ℝ+)
7574adantr 472 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑛 ∈ ℕ) → 𝐸 ∈ ℝ+)
76 2nn 11369 . . . . . . . . . . . . . . . . . . . . . . . . 25 2 ∈ ℕ
7776a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 ∈ ℕ → 2 ∈ ℕ)
78 nnnn0 11483 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 ∈ ℕ → 𝑛 ∈ ℕ0)
7977, 78nnexpcld 13216 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 ∈ ℕ → (2↑𝑛) ∈ ℕ)
8079nnrpd 12055 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 ∈ ℕ → (2↑𝑛) ∈ ℝ+)
8180adantl 473 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑛 ∈ ℕ) → (2↑𝑛) ∈ ℝ+)
8275, 81rpdivcld 12074 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑛 ∈ ℕ) → (𝐸 / (2↑𝑛)) ∈ ℝ+)
83 fvex 6354 . . . . . . . . . . . . . . . . . . . . . 22 (𝐶‘(𝐴𝑛)) ∈ V
8483rabex 4956 . . . . . . . . . . . . . . . . . . . . 21 {𝑖 ∈ (𝐶‘(𝐴𝑛)) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛)))} ∈ V
8584a1i 11 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑛 ∈ ℕ) → {𝑖 ∈ (𝐶‘(𝐴𝑛)) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛)))} ∈ V)
8669, 73, 82, 85fvmptd 6442 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑛 ∈ ℕ) → ((𝐷‘(𝐴𝑛))‘(𝐸 / (2↑𝑛))) = {𝑖 ∈ (𝐶‘(𝐴𝑛)) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛)))})
87 ssrab2 3820 . . . . . . . . . . . . . . . . . . . 20 {𝑖 ∈ (𝐶‘(𝐴𝑛)) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛)))} ⊆ (𝐶‘(𝐴𝑛))
8887a1i 11 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑛 ∈ ℕ) → {𝑖 ∈ (𝐶‘(𝐴𝑛)) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛)))} ⊆ (𝐶‘(𝐴𝑛)))
8986, 88eqsstrd 3772 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑛 ∈ ℕ) → ((𝐷‘(𝐴𝑛))‘(𝐸 / (2↑𝑛))) ⊆ (𝐶‘(𝐴𝑛)))
90 ovnsubaddlem1.i . . . . . . . . . . . . . . . . . 18 ((𝜑𝑛 ∈ ℕ) → (𝐼𝑛) ∈ ((𝐷‘(𝐴𝑛))‘(𝐸 / (2↑𝑛))))
9189, 90sseldd 3737 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛 ∈ ℕ) → (𝐼𝑛) ∈ (𝐶‘(𝐴𝑛)))
9254, 91sseldd 3737 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ ℕ) → (𝐼𝑛) ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ))
93 elmapfn 8038 . . . . . . . . . . . . . . . 16 ((𝐼𝑛) ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) → (𝐼𝑛) Fn ℕ)
9492, 93syl 17 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ) → (𝐼𝑛) Fn ℕ)
95 elmapi 8037 . . . . . . . . . . . . . . . . . 18 ((𝐼𝑛) ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) → (𝐼𝑛):ℕ⟶((ℝ × ℝ) ↑𝑚 𝑋))
9692, 95syl 17 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛 ∈ ℕ) → (𝐼𝑛):ℕ⟶((ℝ × ℝ) ↑𝑚 𝑋))
9796ffvelrnda 6514 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → ((𝐼𝑛)‘𝑗) ∈ ((ℝ × ℝ) ↑𝑚 𝑋))
9897ralrimiva 3096 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ) → ∀𝑗 ∈ ℕ ((𝐼𝑛)‘𝑗) ∈ ((ℝ × ℝ) ↑𝑚 𝑋))
9994, 98jca 555 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ ℕ) → ((𝐼𝑛) Fn ℕ ∧ ∀𝑗 ∈ ℕ ((𝐼𝑛)‘𝑗) ∈ ((ℝ × ℝ) ↑𝑚 𝑋)))
100993adant3 1126 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ ℕ ∧ 𝑗 ∈ ℕ) → ((𝐼𝑛) Fn ℕ ∧ ∀𝑗 ∈ ℕ ((𝐼𝑛)‘𝑗) ∈ ((ℝ × ℝ) ↑𝑚 𝑋)))
101 ffnfv 6543 . . . . . . . . . . . . 13 ((𝐼𝑛):ℕ⟶((ℝ × ℝ) ↑𝑚 𝑋) ↔ ((𝐼𝑛) Fn ℕ ∧ ∀𝑗 ∈ ℕ ((𝐼𝑛)‘𝑗) ∈ ((ℝ × ℝ) ↑𝑚 𝑋)))
102100, 101sylibr 224 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ ∧ 𝑗 ∈ ℕ) → (𝐼𝑛):ℕ⟶((ℝ × ℝ) ↑𝑚 𝑋))
103 simp3 1132 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ ℕ)
104102, 103ffvelrnd 6515 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ ∧ 𝑗 ∈ ℕ) → ((𝐼𝑛)‘𝑗) ∈ ((ℝ × ℝ) ↑𝑚 𝑋))
105 elmapi 8037 . . . . . . . . . . 11 (((𝐼𝑛)‘𝑗) ∈ ((ℝ × ℝ) ↑𝑚 𝑋) → ((𝐼𝑛)‘𝑗):𝑋⟶(ℝ × ℝ))
106104, 105syl 17 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ ∧ 𝑗 ∈ ℕ) → ((𝐼𝑛)‘𝑗):𝑋⟶(ℝ × ℝ))
10736, 42, 106vtocl 3391 . . . . . . . . 9 ((𝜑 ∧ (1st ‘(𝐹𝑚)) ∈ ℕ ∧ 𝑗 ∈ ℕ) → ((𝐼‘(1st ‘(𝐹𝑚)))‘𝑗):𝑋⟶(ℝ × ℝ))
10830, 35, 107vtocl 3391 . . . . . . . 8 ((𝜑 ∧ (1st ‘(𝐹𝑚)) ∈ ℕ ∧ (2nd ‘(𝐹𝑚)) ∈ ℕ) → ((𝐼‘(1st ‘(𝐹𝑚)))‘(2nd ‘(𝐹𝑚))):𝑋⟶(ℝ × ℝ))
10917, 27, 29, 108syl3anc 1473 . . . . . . 7 ((𝜑𝑚 ∈ ℕ) → ((𝐼‘(1st ‘(𝐹𝑚)))‘(2nd ‘(𝐹𝑚))):𝑋⟶(ℝ × ℝ))
110 id 22 . . . . . . . . . 10 (𝑚 ∈ ℕ → 𝑚 ∈ ℕ)
111 fvex 6354 . . . . . . . . . . 11 ((𝐼‘(1st ‘(𝐹𝑚)))‘(2nd ‘(𝐹𝑚))) ∈ V
112111a1i 11 . . . . . . . . . 10 (𝑚 ∈ ℕ → ((𝐼‘(1st ‘(𝐹𝑚)))‘(2nd ‘(𝐹𝑚))) ∈ V)
113 ovnsubaddlem1.g . . . . . . . . . . 11 𝐺 = (𝑚 ∈ ℕ ↦ ((𝐼‘(1st ‘(𝐹𝑚)))‘(2nd ‘(𝐹𝑚))))
114113fvmpt2 6445 . . . . . . . . . 10 ((𝑚 ∈ ℕ ∧ ((𝐼‘(1st ‘(𝐹𝑚)))‘(2nd ‘(𝐹𝑚))) ∈ V) → (𝐺𝑚) = ((𝐼‘(1st ‘(𝐹𝑚)))‘(2nd ‘(𝐹𝑚))))
115110, 112, 114syl2anc 696 . . . . . . . . 9 (𝑚 ∈ ℕ → (𝐺𝑚) = ((𝐼‘(1st ‘(𝐹𝑚)))‘(2nd ‘(𝐹𝑚))))
116115adantl 473 . . . . . . . 8 ((𝜑𝑚 ∈ ℕ) → (𝐺𝑚) = ((𝐼‘(1st ‘(𝐹𝑚)))‘(2nd ‘(𝐹𝑚))))
117116feq1d 6183 . . . . . . 7 ((𝜑𝑚 ∈ ℕ) → ((𝐺𝑚):𝑋⟶(ℝ × ℝ) ↔ ((𝐼‘(1st ‘(𝐹𝑚)))‘(2nd ‘(𝐹𝑚))):𝑋⟶(ℝ × ℝ)))
118109, 117mpbird 247 . . . . . 6 ((𝜑𝑚 ∈ ℕ) → (𝐺𝑚):𝑋⟶(ℝ × ℝ))
11916, 18, 19, 118hoiprodcl2 41267 . . . . 5 ((𝜑𝑚 ∈ ℕ) → (𝐿‘(𝐺𝑚)) ∈ (0[,)+∞))
12015, 119sseldi 3734 . . . 4 ((𝜑𝑚 ∈ ℕ) → (𝐿‘(𝐺𝑚)) ∈ (0[,]+∞))
12112, 14, 120sge0xrclmpt 41140 . . 3 (𝜑 → (Σ^‘(𝑚 ∈ ℕ ↦ (𝐿‘(𝐺𝑚)))) ∈ ℝ*)
122 nfv 1984 . . . 4 𝑛𝜑
123 0xr 10270 . . . . . 6 0 ∈ ℝ*
124123a1i 11 . . . . 5 ((𝜑𝑛 ∈ ℕ) → 0 ∈ ℝ*)
125 pnfxr 10276 . . . . . 6 +∞ ∈ ℝ*
126125a1i 11 . . . . 5 ((𝜑𝑛 ∈ ℕ) → +∞ ∈ ℝ*)
1271adantr 472 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → 𝑋 ∈ Fin)
128 ovnsubaddlem1.z . . . . . . . . 9 𝑍 = (𝑎 ∈ 𝒫 (ℝ ↑𝑚 𝑋) ↦ {𝑧 ∈ ℝ* ∣ ∃𝑖 ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)(𝑎 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑖𝑗))‘𝑘) ∧ 𝑧 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘𝑋 (vol‘(([,) ∘ (𝑖𝑗))‘𝑘)))))})
129127, 7, 128ovnval2b 41264 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → ((voln*‘𝑋)‘(𝐴𝑛)) = if(𝑋 = ∅, 0, inf((𝑍‘(𝐴𝑛)), ℝ*, < )))
130 ovnsubaddlem1.n0 . . . . . . . . . . 11 (𝜑𝑋 ≠ ∅)
131130neneqd 2929 . . . . . . . . . 10 (𝜑 → ¬ 𝑋 = ∅)
132131iffalsed 4233 . . . . . . . . 9 (𝜑 → if(𝑋 = ∅, 0, inf((𝑍‘(𝐴𝑛)), ℝ*, < )) = inf((𝑍‘(𝐴𝑛)), ℝ*, < ))
133132adantr 472 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → if(𝑋 = ∅, 0, inf((𝑍‘(𝐴𝑛)), ℝ*, < )) = inf((𝑍‘(𝐴𝑛)), ℝ*, < ))
134129, 133eqtrd 2786 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → ((voln*‘𝑋)‘(𝐴𝑛)) = inf((𝑍‘(𝐴𝑛)), ℝ*, < ))
135128a1i 11 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → 𝑍 = (𝑎 ∈ 𝒫 (ℝ ↑𝑚 𝑋) ↦ {𝑧 ∈ ℝ* ∣ ∃𝑖 ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)(𝑎 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑖𝑗))‘𝑘) ∧ 𝑧 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘𝑋 (vol‘(([,) ∘ (𝑖𝑗))‘𝑘)))))}))
136 sseq1 3759 . . . . . . . . . . . . . 14 (𝑎 = (𝐴𝑛) → (𝑎 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑖𝑗))‘𝑘) ↔ (𝐴𝑛) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑖𝑗))‘𝑘)))
137136anbi1d 743 . . . . . . . . . . . . 13 (𝑎 = (𝐴𝑛) → ((𝑎 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑖𝑗))‘𝑘) ∧ 𝑧 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘𝑋 (vol‘(([,) ∘ (𝑖𝑗))‘𝑘))))) ↔ ((𝐴𝑛) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑖𝑗))‘𝑘) ∧ 𝑧 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘𝑋 (vol‘(([,) ∘ (𝑖𝑗))‘𝑘)))))))
138137rexbidv 3182 . . . . . . . . . . . 12 (𝑎 = (𝐴𝑛) → (∃𝑖 ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)(𝑎 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑖𝑗))‘𝑘) ∧ 𝑧 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘𝑋 (vol‘(([,) ∘ (𝑖𝑗))‘𝑘))))) ↔ ∃𝑖 ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)((𝐴𝑛) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑖𝑗))‘𝑘) ∧ 𝑧 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘𝑋 (vol‘(([,) ∘ (𝑖𝑗))‘𝑘)))))))
139138rabbidv 3321 . . . . . . . . . . 11 (𝑎 = (𝐴𝑛) → {𝑧 ∈ ℝ* ∣ ∃𝑖 ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)(𝑎 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑖𝑗))‘𝑘) ∧ 𝑧 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘𝑋 (vol‘(([,) ∘ (𝑖𝑗))‘𝑘)))))} = {𝑧 ∈ ℝ* ∣ ∃𝑖 ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)((𝐴𝑛) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑖𝑗))‘𝑘) ∧ 𝑧 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘𝑋 (vol‘(([,) ∘ (𝑖𝑗))‘𝑘)))))})
140139adantl 473 . . . . . . . . . 10 (((𝜑𝑛 ∈ ℕ) ∧ 𝑎 = (𝐴𝑛)) → {𝑧 ∈ ℝ* ∣ ∃𝑖 ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)(𝑎 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑖𝑗))‘𝑘) ∧ 𝑧 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘𝑋 (vol‘(([,) ∘ (𝑖𝑗))‘𝑘)))))} = {𝑧 ∈ ℝ* ∣ ∃𝑖 ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)((𝐴𝑛) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑖𝑗))‘𝑘) ∧ 𝑧 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘𝑋 (vol‘(([,) ∘ (𝑖𝑗))‘𝑘)))))})
141 xrex 12014 . . . . . . . . . . . 12 * ∈ V
142141rabex 4956 . . . . . . . . . . 11 {𝑧 ∈ ℝ* ∣ ∃𝑖 ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)((𝐴𝑛) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑖𝑗))‘𝑘) ∧ 𝑧 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘𝑋 (vol‘(([,) ∘ (𝑖𝑗))‘𝑘)))))} ∈ V
143142a1i 11 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → {𝑧 ∈ ℝ* ∣ ∃𝑖 ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)((𝐴𝑛) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑖𝑗))‘𝑘) ∧ 𝑧 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘𝑋 (vol‘(([,) ∘ (𝑖𝑗))‘𝑘)))))} ∈ V)
144135, 140, 5, 143fvmptd 6442 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → (𝑍‘(𝐴𝑛)) = {𝑧 ∈ ℝ* ∣ ∃𝑖 ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)((𝐴𝑛) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑖𝑗))‘𝑘) ∧ 𝑧 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘𝑋 (vol‘(([,) ∘ (𝑖𝑗))‘𝑘)))))})
145 ssrab2 3820 . . . . . . . . . 10 {𝑧 ∈ ℝ* ∣ ∃𝑖 ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)((𝐴𝑛) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑖𝑗))‘𝑘) ∧ 𝑧 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘𝑋 (vol‘(([,) ∘ (𝑖𝑗))‘𝑘)))))} ⊆ ℝ*
146145a1i 11 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → {𝑧 ∈ ℝ* ∣ ∃𝑖 ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)((𝐴𝑛) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑖𝑗))‘𝑘) ∧ 𝑧 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘𝑋 (vol‘(([,) ∘ (𝑖𝑗))‘𝑘)))))} ⊆ ℝ*)
147144, 146eqsstrd 3772 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → (𝑍‘(𝐴𝑛)) ⊆ ℝ*)
148 infxrcl 12348 . . . . . . . 8 ((𝑍‘(𝐴𝑛)) ⊆ ℝ* → inf((𝑍‘(𝐴𝑛)), ℝ*, < ) ∈ ℝ*)
149147, 148syl 17 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → inf((𝑍‘(𝐴𝑛)), ℝ*, < ) ∈ ℝ*)
150134, 149eqeltrd 2831 . . . . . 6 ((𝜑𝑛 ∈ ℕ) → ((voln*‘𝑋)‘(𝐴𝑛)) ∈ ℝ*)
15174rpred 12057 . . . . . . . . 9 (𝜑𝐸 ∈ ℝ)
152151adantr 472 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → 𝐸 ∈ ℝ)
153 2re 11274 . . . . . . . . . . 11 2 ∈ ℝ
154153a1i 11 . . . . . . . . . 10 (𝑛 ∈ ℕ → 2 ∈ ℝ)
155154, 78reexpcld 13211 . . . . . . . . 9 (𝑛 ∈ ℕ → (2↑𝑛) ∈ ℝ)
156155adantl 473 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → (2↑𝑛) ∈ ℝ)
157154recnd 10252 . . . . . . . . . 10 (𝑛 ∈ ℕ → 2 ∈ ℂ)
158 2ne0 11297 . . . . . . . . . . 11 2 ≠ 0
159158a1i 11 . . . . . . . . . 10 (𝑛 ∈ ℕ → 2 ≠ 0)
160 nnz 11583 . . . . . . . . . 10 (𝑛 ∈ ℕ → 𝑛 ∈ ℤ)
161157, 159, 160expne0d 13200 . . . . . . . . 9 (𝑛 ∈ ℕ → (2↑𝑛) ≠ 0)
162161adantl 473 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → (2↑𝑛) ≠ 0)
163152, 156, 162redivcld 11037 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → (𝐸 / (2↑𝑛)) ∈ ℝ)
164163rexrd 10273 . . . . . 6 ((𝜑𝑛 ∈ ℕ) → (𝐸 / (2↑𝑛)) ∈ ℝ*)
165150, 164xaddcld 12316 . . . . 5 ((𝜑𝑛 ∈ ℕ) → (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛))) ∈ ℝ*)
166127, 7ovncl 41279 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → ((voln*‘𝑋)‘(𝐴𝑛)) ∈ (0[,]+∞))
167 xrge0ge0 40053 . . . . . . 7 (((voln*‘𝑋)‘(𝐴𝑛)) ∈ (0[,]+∞) → 0 ≤ ((voln*‘𝑋)‘(𝐴𝑛)))
168166, 167syl 17 . . . . . 6 ((𝜑𝑛 ∈ ℕ) → 0 ≤ ((voln*‘𝑋)‘(𝐴𝑛)))
169 0red 10225 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → 0 ∈ ℝ)
17082rpgt0d 12060 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → 0 < (𝐸 / (2↑𝑛)))
171169, 163, 170ltled 10369 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → 0 ≤ (𝐸 / (2↑𝑛)))
172163ltpnfd 12140 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → (𝐸 / (2↑𝑛)) < +∞)
173164, 126, 172xrltled 39977 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → (𝐸 / (2↑𝑛)) ≤ +∞)
174124, 126, 164, 171, 173eliccxrd 40248 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → (𝐸 / (2↑𝑛)) ∈ (0[,]+∞))
175150, 174xadd0ge 40026 . . . . . 6 ((𝜑𝑛 ∈ ℕ) → ((voln*‘𝑋)‘(𝐴𝑛)) ≤ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛))))
176124, 150, 165, 168, 175xrletrd 12178 . . . . 5 ((𝜑𝑛 ∈ ℕ) → 0 ≤ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛))))
177 pnfge 12149 . . . . . 6 ((((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛))) ∈ ℝ* → (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛))) ≤ +∞)
178165, 177syl 17 . . . . 5 ((𝜑𝑛 ∈ ℕ) → (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛))) ≤ +∞)
179124, 126, 165, 176, 178eliccxrd 40248 . . . 4 ((𝜑𝑛 ∈ ℕ) → (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛))) ∈ (0[,]+∞))
180122, 14, 179sge0xrclmpt 41140 . . 3 (𝜑 → (Σ^‘(𝑛 ∈ ℕ ↦ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛))))) ∈ ℝ*)
18143a1i 11 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ ℕ) → 𝐶 = (𝑎 ∈ 𝒫 (ℝ ↑𝑚 𝑋) ↦ { ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∣ 𝑎 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘)}))
182 sseq1 3759 . . . . . . . . . . . . . 14 (𝑎 = (𝐴‘(1st ‘(𝐹𝑚))) → (𝑎 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘) ↔ (𝐴‘(1st ‘(𝐹𝑚))) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘)))
183182rabbidv 3321 . . . . . . . . . . . . 13 (𝑎 = (𝐴‘(1st ‘(𝐹𝑚))) → { ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∣ 𝑎 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘)} = { ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∣ (𝐴‘(1st ‘(𝐹𝑚))) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘)})
184183adantl 473 . . . . . . . . . . . 12 (((𝜑𝑚 ∈ ℕ) ∧ 𝑎 = (𝐴‘(1st ‘(𝐹𝑚)))) → { ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∣ 𝑎 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘)} = { ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∣ (𝐴‘(1st ‘(𝐹𝑚))) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘)})
1852adantr 472 . . . . . . . . . . . . 13 ((𝜑𝑚 ∈ ℕ) → 𝐴:ℕ⟶𝒫 (ℝ ↑𝑚 𝑋))
186185, 27ffvelrnd 6515 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ ℕ) → (𝐴‘(1st ‘(𝐹𝑚))) ∈ 𝒫 (ℝ ↑𝑚 𝑋))
18748rabex 4956 . . . . . . . . . . . . 13 { ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∣ (𝐴‘(1st ‘(𝐹𝑚))) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘)} ∈ V
188187a1i 11 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ ℕ) → { ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∣ (𝐴‘(1st ‘(𝐹𝑚))) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘)} ∈ V)
189181, 184, 186, 188fvmptd 6442 . . . . . . . . . . 11 ((𝜑𝑚 ∈ ℕ) → (𝐶‘(𝐴‘(1st ‘(𝐹𝑚)))) = { ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∣ (𝐴‘(1st ‘(𝐹𝑚))) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘)})
190 ssrab2 3820 . . . . . . . . . . . 12 { ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∣ (𝐴‘(1st ‘(𝐹𝑚))) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘)} ⊆ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)
191190a1i 11 . . . . . . . . . . 11 ((𝜑𝑚 ∈ ℕ) → { ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∣ (𝐴‘(1st ‘(𝐹𝑚))) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘)} ⊆ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ))
192189, 191eqsstrd 3772 . . . . . . . . . 10 ((𝜑𝑚 ∈ ℕ) → (𝐶‘(𝐴‘(1st ‘(𝐹𝑚)))) ⊆ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ))
19355a1i 11 . . . . . . . . . . . . . 14 ((𝜑𝑚 ∈ ℕ) → 𝐷 = (𝑎 ∈ 𝒫 (ℝ ↑𝑚 𝑋) ↦ (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶𝑎) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘𝑎) +𝑒 𝑒)})))
194 fveq2 6344 . . . . . . . . . . . . . . . . . . 19 (𝑎 = (𝐴‘(1st ‘(𝐹𝑚))) → (𝐶𝑎) = (𝐶‘(𝐴‘(1st ‘(𝐹𝑚)))))
195194eleq2d 2817 . . . . . . . . . . . . . . . . . 18 (𝑎 = (𝐴‘(1st ‘(𝐹𝑚))) → (𝑖 ∈ (𝐶𝑎) ↔ 𝑖 ∈ (𝐶‘(𝐴‘(1st ‘(𝐹𝑚))))))
196 fveq2 6344 . . . . . . . . . . . . . . . . . . . 20 (𝑎 = (𝐴‘(1st ‘(𝐹𝑚))) → ((voln*‘𝑋)‘𝑎) = ((voln*‘𝑋)‘(𝐴‘(1st ‘(𝐹𝑚)))))
197196oveq1d 6820 . . . . . . . . . . . . . . . . . . 19 (𝑎 = (𝐴‘(1st ‘(𝐹𝑚))) → (((voln*‘𝑋)‘𝑎) +𝑒 𝑒) = (((voln*‘𝑋)‘(𝐴‘(1st ‘(𝐹𝑚)))) +𝑒 𝑒))
198197breq2d 4808 . . . . . . . . . . . . . . . . . 18 (𝑎 = (𝐴‘(1st ‘(𝐹𝑚))) → ((Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘𝑎) +𝑒 𝑒) ↔ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴‘(1st ‘(𝐹𝑚)))) +𝑒 𝑒)))
199195, 198anbi12d 749 . . . . . . . . . . . . . . . . 17 (𝑎 = (𝐴‘(1st ‘(𝐹𝑚))) → ((𝑖 ∈ (𝐶𝑎) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘𝑎) +𝑒 𝑒)) ↔ (𝑖 ∈ (𝐶‘(𝐴‘(1st ‘(𝐹𝑚)))) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴‘(1st ‘(𝐹𝑚)))) +𝑒 𝑒))))
200199rabbidva2 3318 . . . . . . . . . . . . . . . 16 (𝑎 = (𝐴‘(1st ‘(𝐹𝑚))) → {𝑖 ∈ (𝐶𝑎) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘𝑎) +𝑒 𝑒)} = {𝑖 ∈ (𝐶‘(𝐴‘(1st ‘(𝐹𝑚)))) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴‘(1st ‘(𝐹𝑚)))) +𝑒 𝑒)})
201200mpteq2dv 4889 . . . . . . . . . . . . . . 15 (𝑎 = (𝐴‘(1st ‘(𝐹𝑚))) → (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶𝑎) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘𝑎) +𝑒 𝑒)}) = (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶‘(𝐴‘(1st ‘(𝐹𝑚)))) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴‘(1st ‘(𝐹𝑚)))) +𝑒 𝑒)}))
202201adantl 473 . . . . . . . . . . . . . 14 (((𝜑𝑚 ∈ ℕ) ∧ 𝑎 = (𝐴‘(1st ‘(𝐹𝑚)))) → (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶𝑎) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘𝑎) +𝑒 𝑒)}) = (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶‘(𝐴‘(1st ‘(𝐹𝑚)))) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴‘(1st ‘(𝐹𝑚)))) +𝑒 𝑒)}))
20366mptex 6642 . . . . . . . . . . . . . . 15 (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶‘(𝐴‘(1st ‘(𝐹𝑚)))) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴‘(1st ‘(𝐹𝑚)))) +𝑒 𝑒)}) ∈ V
204203a1i 11 . . . . . . . . . . . . . 14 ((𝜑𝑚 ∈ ℕ) → (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶‘(𝐴‘(1st ‘(𝐹𝑚)))) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴‘(1st ‘(𝐹𝑚)))) +𝑒 𝑒)}) ∈ V)
205193, 202, 186, 204fvmptd 6442 . . . . . . . . . . . . 13 ((𝜑𝑚 ∈ ℕ) → (𝐷‘(𝐴‘(1st ‘(𝐹𝑚)))) = (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶‘(𝐴‘(1st ‘(𝐹𝑚)))) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴‘(1st ‘(𝐹𝑚)))) +𝑒 𝑒)}))
206 oveq2 6813 . . . . . . . . . . . . . . . 16 (𝑒 = (𝐸 / (2↑(1st ‘(𝐹𝑚)))) → (((voln*‘𝑋)‘(𝐴‘(1st ‘(𝐹𝑚)))) +𝑒 𝑒) = (((voln*‘𝑋)‘(𝐴‘(1st ‘(𝐹𝑚)))) +𝑒 (𝐸 / (2↑(1st ‘(𝐹𝑚))))))
207206breq2d 4808 . . . . . . . . . . . . . . 15 (𝑒 = (𝐸 / (2↑(1st ‘(𝐹𝑚)))) → ((Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴‘(1st ‘(𝐹𝑚)))) +𝑒 𝑒) ↔ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴‘(1st ‘(𝐹𝑚)))) +𝑒 (𝐸 / (2↑(1st ‘(𝐹𝑚)))))))
208207rabbidv 3321 . . . . . . . . . . . . . 14 (𝑒 = (𝐸 / (2↑(1st ‘(𝐹𝑚)))) → {𝑖 ∈ (𝐶‘(𝐴‘(1st ‘(𝐹𝑚)))) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴‘(1st ‘(𝐹𝑚)))) +𝑒 𝑒)} = {𝑖 ∈ (𝐶‘(𝐴‘(1st ‘(𝐹𝑚)))) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴‘(1st ‘(𝐹𝑚)))) +𝑒 (𝐸 / (2↑(1st ‘(𝐹𝑚)))))})
209208adantl 473 . . . . . . . . . . . . 13 (((𝜑𝑚 ∈ ℕ) ∧ 𝑒 = (𝐸 / (2↑(1st ‘(𝐹𝑚))))) → {𝑖 ∈ (𝐶‘(𝐴‘(1st ‘(𝐹𝑚)))) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴‘(1st ‘(𝐹𝑚)))) +𝑒 𝑒)} = {𝑖 ∈ (𝐶‘(𝐴‘(1st ‘(𝐹𝑚)))) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴‘(1st ‘(𝐹𝑚)))) +𝑒 (𝐸 / (2↑(1st ‘(𝐹𝑚)))))})
21017, 74syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑚 ∈ ℕ) → 𝐸 ∈ ℝ+)
211 2rp 12022 . . . . . . . . . . . . . . . 16 2 ∈ ℝ+
212211a1i 11 . . . . . . . . . . . . . . 15 ((𝜑𝑚 ∈ ℕ) → 2 ∈ ℝ+)
21327nnzd 11665 . . . . . . . . . . . . . . 15 ((𝜑𝑚 ∈ ℕ) → (1st ‘(𝐹𝑚)) ∈ ℤ)
214212, 213rpexpcld 13218 . . . . . . . . . . . . . 14 ((𝜑𝑚 ∈ ℕ) → (2↑(1st ‘(𝐹𝑚))) ∈ ℝ+)
215210, 214rpdivcld 12074 . . . . . . . . . . . . 13 ((𝜑𝑚 ∈ ℕ) → (𝐸 / (2↑(1st ‘(𝐹𝑚)))) ∈ ℝ+)
216 fvex 6354 . . . . . . . . . . . . . . 15 (𝐶‘(𝐴‘(1st ‘(𝐹𝑚)))) ∈ V
217216rabex 4956 . . . . . . . . . . . . . 14 {𝑖 ∈ (𝐶‘(𝐴‘(1st ‘(𝐹𝑚)))) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴‘(1st ‘(𝐹𝑚)))) +𝑒 (𝐸 / (2↑(1st ‘(𝐹𝑚)))))} ∈ V
218217a1i 11 . . . . . . . . . . . . 13 ((𝜑𝑚 ∈ ℕ) → {𝑖 ∈ (𝐶‘(𝐴‘(1st ‘(𝐹𝑚)))) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴‘(1st ‘(𝐹𝑚)))) +𝑒 (𝐸 / (2↑(1st ‘(𝐹𝑚)))))} ∈ V)
219205, 209, 215, 218fvmptd 6442 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ ℕ) → ((𝐷‘(𝐴‘(1st ‘(𝐹𝑚))))‘(𝐸 / (2↑(1st ‘(𝐹𝑚))))) = {𝑖 ∈ (𝐶‘(𝐴‘(1st ‘(𝐹𝑚)))) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴‘(1st ‘(𝐹𝑚)))) +𝑒 (𝐸 / (2↑(1st ‘(𝐹𝑚)))))})
220 ssrab2 3820 . . . . . . . . . . . . 13 {𝑖 ∈ (𝐶‘(𝐴‘(1st ‘(𝐹𝑚)))) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴‘(1st ‘(𝐹𝑚)))) +𝑒 (𝐸 / (2↑(1st ‘(𝐹𝑚)))))} ⊆ (𝐶‘(𝐴‘(1st ‘(𝐹𝑚))))
221220a1i 11 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ ℕ) → {𝑖 ∈ (𝐶‘(𝐴‘(1st ‘(𝐹𝑚)))) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴‘(1st ‘(𝐹𝑚)))) +𝑒 (𝐸 / (2↑(1st ‘(𝐹𝑚)))))} ⊆ (𝐶‘(𝐴‘(1st ‘(𝐹𝑚)))))
222219, 221eqsstrd 3772 . . . . . . . . . . 11 ((𝜑𝑚 ∈ ℕ) → ((𝐷‘(𝐴‘(1st ‘(𝐹𝑚))))‘(𝐸 / (2↑(1st ‘(𝐹𝑚))))) ⊆ (𝐶‘(𝐴‘(1st ‘(𝐹𝑚)))))
22337anbi2d 742 . . . . . . . . . . . . . 14 (𝑛 = (1st ‘(𝐹𝑚)) → ((𝜑𝑛 ∈ ℕ) ↔ (𝜑 ∧ (1st ‘(𝐹𝑚)) ∈ ℕ)))
224 fveq2 6344 . . . . . . . . . . . . . . . . 17 (𝑛 = (1st ‘(𝐹𝑚)) → (𝐴𝑛) = (𝐴‘(1st ‘(𝐹𝑚))))
225224fveq2d 6348 . . . . . . . . . . . . . . . 16 (𝑛 = (1st ‘(𝐹𝑚)) → (𝐷‘(𝐴𝑛)) = (𝐷‘(𝐴‘(1st ‘(𝐹𝑚)))))
226 oveq2 6813 . . . . . . . . . . . . . . . . 17 (𝑛 = (1st ‘(𝐹𝑚)) → (2↑𝑛) = (2↑(1st ‘(𝐹𝑚))))
227226oveq2d 6821 . . . . . . . . . . . . . . . 16 (𝑛 = (1st ‘(𝐹𝑚)) → (𝐸 / (2↑𝑛)) = (𝐸 / (2↑(1st ‘(𝐹𝑚)))))
228225, 227fveq12d 6350 . . . . . . . . . . . . . . 15 (𝑛 = (1st ‘(𝐹𝑚)) → ((𝐷‘(𝐴𝑛))‘(𝐸 / (2↑𝑛))) = ((𝐷‘(𝐴‘(1st ‘(𝐹𝑚))))‘(𝐸 / (2↑(1st ‘(𝐹𝑚))))))
22939, 228eleq12d 2825 . . . . . . . . . . . . . 14 (𝑛 = (1st ‘(𝐹𝑚)) → ((𝐼𝑛) ∈ ((𝐷‘(𝐴𝑛))‘(𝐸 / (2↑𝑛))) ↔ (𝐼‘(1st ‘(𝐹𝑚))) ∈ ((𝐷‘(𝐴‘(1st ‘(𝐹𝑚))))‘(𝐸 / (2↑(1st ‘(𝐹𝑚)))))))
230223, 229imbi12d 333 . . . . . . . . . . . . 13 (𝑛 = (1st ‘(𝐹𝑚)) → (((𝜑𝑛 ∈ ℕ) → (𝐼𝑛) ∈ ((𝐷‘(𝐴𝑛))‘(𝐸 / (2↑𝑛)))) ↔ ((𝜑 ∧ (1st ‘(𝐹𝑚)) ∈ ℕ) → (𝐼‘(1st ‘(𝐹𝑚))) ∈ ((𝐷‘(𝐴‘(1st ‘(𝐹𝑚))))‘(𝐸 / (2↑(1st ‘(𝐹𝑚))))))))
23136, 230, 90vtocl 3391 . . . . . . . . . . . 12 ((𝜑 ∧ (1st ‘(𝐹𝑚)) ∈ ℕ) → (𝐼‘(1st ‘(𝐹𝑚))) ∈ ((𝐷‘(𝐴‘(1st ‘(𝐹𝑚))))‘(𝐸 / (2↑(1st ‘(𝐹𝑚))))))
23217, 27, 231syl2anc 696 . . . . . . . . . . 11 ((𝜑𝑚 ∈ ℕ) → (𝐼‘(1st ‘(𝐹𝑚))) ∈ ((𝐷‘(𝐴‘(1st ‘(𝐹𝑚))))‘(𝐸 / (2↑(1st ‘(𝐹𝑚))))))
233222, 232sseldd 3737 . . . . . . . . . 10 ((𝜑𝑚 ∈ ℕ) → (𝐼‘(1st ‘(𝐹𝑚))) ∈ (𝐶‘(𝐴‘(1st ‘(𝐹𝑚)))))
234192, 233sseldd 3737 . . . . . . . . 9 ((𝜑𝑚 ∈ ℕ) → (𝐼‘(1st ‘(𝐹𝑚))) ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ))
235 elmapfn 8038 . . . . . . . . 9 ((𝐼‘(1st ‘(𝐹𝑚))) ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) → (𝐼‘(1st ‘(𝐹𝑚))) Fn ℕ)
236234, 235syl 17 . . . . . . . 8 ((𝜑𝑚 ∈ ℕ) → (𝐼‘(1st ‘(𝐹𝑚))) Fn ℕ)
237 elmapi 8037 . . . . . . . . . . 11 ((𝐼‘(1st ‘(𝐹𝑚))) ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) → (𝐼‘(1st ‘(𝐹𝑚))):ℕ⟶((ℝ × ℝ) ↑𝑚 𝑋))
238234, 237syl 17 . . . . . . . . . 10 ((𝜑𝑚 ∈ ℕ) → (𝐼‘(1st ‘(𝐹𝑚))):ℕ⟶((ℝ × ℝ) ↑𝑚 𝑋))
239238ffvelrnda 6514 . . . . . . . . 9 (((𝜑𝑚 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → ((𝐼‘(1st ‘(𝐹𝑚)))‘𝑗) ∈ ((ℝ × ℝ) ↑𝑚 𝑋))
240239ralrimiva 3096 . . . . . . . 8 ((𝜑𝑚 ∈ ℕ) → ∀𝑗 ∈ ℕ ((𝐼‘(1st ‘(𝐹𝑚)))‘𝑗) ∈ ((ℝ × ℝ) ↑𝑚 𝑋))
241236, 240jca 555 . . . . . . 7 ((𝜑𝑚 ∈ ℕ) → ((𝐼‘(1st ‘(𝐹𝑚))) Fn ℕ ∧ ∀𝑗 ∈ ℕ ((𝐼‘(1st ‘(𝐹𝑚)))‘𝑗) ∈ ((ℝ × ℝ) ↑𝑚 𝑋)))
242 ffnfv 6543 . . . . . . 7 ((𝐼‘(1st ‘(𝐹𝑚))):ℕ⟶((ℝ × ℝ) ↑𝑚 𝑋) ↔ ((𝐼‘(1st ‘(𝐹𝑚))) Fn ℕ ∧ ∀𝑗 ∈ ℕ ((𝐼‘(1st ‘(𝐹𝑚)))‘𝑗) ∈ ((ℝ × ℝ) ↑𝑚 𝑋)))
243241, 242sylibr 224 . . . . . 6 ((𝜑𝑚 ∈ ℕ) → (𝐼‘(1st ‘(𝐹𝑚))):ℕ⟶((ℝ × ℝ) ↑𝑚 𝑋))
244243, 29ffvelrnd 6515 . . . . 5 ((𝜑𝑚 ∈ ℕ) → ((𝐼‘(1st ‘(𝐹𝑚)))‘(2nd ‘(𝐹𝑚))) ∈ ((ℝ × ℝ) ↑𝑚 𝑋))
245244, 113fmptd 6540 . . . 4 (𝜑𝐺:ℕ⟶((ℝ × ℝ) ↑𝑚 𝑋))
246 simpl 474 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → 𝜑)
24790, 86eleqtrd 2833 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → (𝐼𝑛) ∈ {𝑖 ∈ (𝐶‘(𝐴𝑛)) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛)))})
24887, 247sseldi 3734 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → (𝐼𝑛) ∈ (𝐶‘(𝐴𝑛)))
249 simp3 1132 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ ∧ (𝐼𝑛) ∈ (𝐶‘(𝐴𝑛))) → (𝐼𝑛) ∈ (𝐶‘(𝐴𝑛)))
250513adant3 1126 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ ∧ (𝐼𝑛) ∈ (𝐶‘(𝐴𝑛))) → (𝐶‘(𝐴𝑛)) = { ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∣ (𝐴𝑛) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘)})
251249, 250eleqtrd 2833 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ ∧ (𝐼𝑛) ∈ (𝐶‘(𝐴𝑛))) → (𝐼𝑛) ∈ { ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∣ (𝐴𝑛) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘)})
252 fveq1 6343 . . . . . . . . . . . . . . . . 17 ( = (𝐼𝑛) → (𝑗) = ((𝐼𝑛)‘𝑗))
253252coeq2d 5432 . . . . . . . . . . . . . . . 16 ( = (𝐼𝑛) → ([,) ∘ (𝑗)) = ([,) ∘ ((𝐼𝑛)‘𝑗)))
254253fveq1d 6346 . . . . . . . . . . . . . . 15 ( = (𝐼𝑛) → (([,) ∘ (𝑗))‘𝑘) = (([,) ∘ ((𝐼𝑛)‘𝑗))‘𝑘))
255254ixpeq2dv 8082 . . . . . . . . . . . . . 14 ( = (𝐼𝑛) → X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘) = X𝑘𝑋 (([,) ∘ ((𝐼𝑛)‘𝑗))‘𝑘))
256255iuneq2d 4691 . . . . . . . . . . . . 13 ( = (𝐼𝑛) → 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘) = 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ ((𝐼𝑛)‘𝑗))‘𝑘))
257256sseq2d 3766 . . . . . . . . . . . 12 ( = (𝐼𝑛) → ((𝐴𝑛) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘) ↔ (𝐴𝑛) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ ((𝐼𝑛)‘𝑗))‘𝑘)))
258257elrab 3496 . . . . . . . . . . 11 ((𝐼𝑛) ∈ { ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∣ (𝐴𝑛) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘)} ↔ ((𝐼𝑛) ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∧ (𝐴𝑛) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ ((𝐼𝑛)‘𝑗))‘𝑘)))
259251, 258sylib 208 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ ∧ (𝐼𝑛) ∈ (𝐶‘(𝐴𝑛))) → ((𝐼𝑛) ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∧ (𝐴𝑛) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ ((𝐼𝑛)‘𝑗))‘𝑘)))
260259simprd 482 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ ∧ (𝐼𝑛) ∈ (𝐶‘(𝐴𝑛))) → (𝐴𝑛) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ ((𝐼𝑛)‘𝑗))‘𝑘))
261246, 4, 248, 260syl3anc 1473 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → (𝐴𝑛) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ ((𝐼𝑛)‘𝑗))‘𝑘))
262 f1ofo 6297 . . . . . . . . . . . . . 14 (𝐹:ℕ–1-1-onto→(ℕ × ℕ) → 𝐹:ℕ–onto→(ℕ × ℕ))
26320, 262syl 17 . . . . . . . . . . . . 13 (𝜑𝐹:ℕ–onto→(ℕ × ℕ))
264263ad2antrr 764 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → 𝐹:ℕ–onto→(ℕ × ℕ))
265 opelxpi 5297 . . . . . . . . . . . . 13 ((𝑛 ∈ ℕ ∧ 𝑗 ∈ ℕ) → ⟨𝑛, 𝑗⟩ ∈ (ℕ × ℕ))
2664, 265sylan 489 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → ⟨𝑛, 𝑗⟩ ∈ (ℕ × ℕ))
267 foelrni 6398 . . . . . . . . . . . 12 ((𝐹:ℕ–onto→(ℕ × ℕ) ∧ ⟨𝑛, 𝑗⟩ ∈ (ℕ × ℕ)) → ∃𝑚 ∈ ℕ (𝐹𝑚) = ⟨𝑛, 𝑗⟩)
268264, 266, 267syl2anc 696 . . . . . . . . . . 11 (((𝜑𝑛 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → ∃𝑚 ∈ ℕ (𝐹𝑚) = ⟨𝑛, 𝑗⟩)
269 nfv 1984 . . . . . . . . . . . 12 𝑚((𝜑𝑛 ∈ ℕ) ∧ 𝑗 ∈ ℕ)
270 nfre1 3135 . . . . . . . . . . . 12 𝑚𝑚 ∈ {𝑖 ∈ ℕ ∣ (1st ‘(𝐹𝑖)) = 𝑛}X𝑘𝑋 (([,) ∘ ((𝐼𝑛)‘𝑗))‘𝑘) ⊆ X𝑘𝑋 (([,) ∘ (𝐺𝑚))‘𝑘)
271 simpl 474 . . . . . . . . . . . . . . . . 17 ((𝑚 ∈ ℕ ∧ (𝐹𝑚) = ⟨𝑛, 𝑗⟩) → 𝑚 ∈ ℕ)
272 fveq2 6344 . . . . . . . . . . . . . . . . . . 19 ((𝐹𝑚) = ⟨𝑛, 𝑗⟩ → (1st ‘(𝐹𝑚)) = (1st ‘⟨𝑛, 𝑗⟩))
273 vex 3335 . . . . . . . . . . . . . . . . . . . . 21 𝑛 ∈ V
274 vex 3335 . . . . . . . . . . . . . . . . . . . . 21 𝑗 ∈ V
275 op1stg 7337 . . . . . . . . . . . . . . . . . . . . 21 ((𝑛 ∈ V ∧ 𝑗 ∈ V) → (1st ‘⟨𝑛, 𝑗⟩) = 𝑛)
276273, 274, 275mp2an 710 . . . . . . . . . . . . . . . . . . . 20 (1st ‘⟨𝑛, 𝑗⟩) = 𝑛
277276a1i 11 . . . . . . . . . . . . . . . . . . 19 ((𝐹𝑚) = ⟨𝑛, 𝑗⟩ → (1st ‘⟨𝑛, 𝑗⟩) = 𝑛)
278272, 277eqtrd 2786 . . . . . . . . . . . . . . . . . 18 ((𝐹𝑚) = ⟨𝑛, 𝑗⟩ → (1st ‘(𝐹𝑚)) = 𝑛)
279278adantl 473 . . . . . . . . . . . . . . . . 17 ((𝑚 ∈ ℕ ∧ (𝐹𝑚) = ⟨𝑛, 𝑗⟩) → (1st ‘(𝐹𝑚)) = 𝑛)
280271, 279jca 555 . . . . . . . . . . . . . . . 16 ((𝑚 ∈ ℕ ∧ (𝐹𝑚) = ⟨𝑛, 𝑗⟩) → (𝑚 ∈ ℕ ∧ (1st ‘(𝐹𝑚)) = 𝑛))
281 fveq2 6344 . . . . . . . . . . . . . . . . . . 19 (𝑖 = 𝑚 → (𝐹𝑖) = (𝐹𝑚))
282281fveq2d 6348 . . . . . . . . . . . . . . . . . 18 (𝑖 = 𝑚 → (1st ‘(𝐹𝑖)) = (1st ‘(𝐹𝑚)))
283282eqeq1d 2754 . . . . . . . . . . . . . . . . 17 (𝑖 = 𝑚 → ((1st ‘(𝐹𝑖)) = 𝑛 ↔ (1st ‘(𝐹𝑚)) = 𝑛))
284283elrab 3496 . . . . . . . . . . . . . . . 16 (𝑚 ∈ {𝑖 ∈ ℕ ∣ (1st ‘(𝐹𝑖)) = 𝑛} ↔ (𝑚 ∈ ℕ ∧ (1st ‘(𝐹𝑚)) = 𝑛))
285280, 284sylibr 224 . . . . . . . . . . . . . . 15 ((𝑚 ∈ ℕ ∧ (𝐹𝑚) = ⟨𝑛, 𝑗⟩) → 𝑚 ∈ {𝑖 ∈ ℕ ∣ (1st ‘(𝐹𝑖)) = 𝑛})
2862853adant1 1124 . . . . . . . . . . . . . 14 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑗 ∈ ℕ) ∧ 𝑚 ∈ ℕ ∧ (𝐹𝑚) = ⟨𝑛, 𝑗⟩) → 𝑚 ∈ {𝑖 ∈ ℕ ∣ (1st ‘(𝐹𝑖)) = 𝑛})
287271, 115syl 17 . . . . . . . . . . . . . . . . . . . 20 ((𝑚 ∈ ℕ ∧ (𝐹𝑚) = ⟨𝑛, 𝑗⟩) → (𝐺𝑚) = ((𝐼‘(1st ‘(𝐹𝑚)))‘(2nd ‘(𝐹𝑚))))
288278fveq2d 6348 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐹𝑚) = ⟨𝑛, 𝑗⟩ → (𝐼‘(1st ‘(𝐹𝑚))) = (𝐼𝑛))
289273, 274op2ndd 7336 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐹𝑚) = ⟨𝑛, 𝑗⟩ → (2nd ‘(𝐹𝑚)) = 𝑗)
290288, 289fveq12d 6350 . . . . . . . . . . . . . . . . . . . . 21 ((𝐹𝑚) = ⟨𝑛, 𝑗⟩ → ((𝐼‘(1st ‘(𝐹𝑚)))‘(2nd ‘(𝐹𝑚))) = ((𝐼𝑛)‘𝑗))
291290adantl 473 . . . . . . . . . . . . . . . . . . . 20 ((𝑚 ∈ ℕ ∧ (𝐹𝑚) = ⟨𝑛, 𝑗⟩) → ((𝐼‘(1st ‘(𝐹𝑚)))‘(2nd ‘(𝐹𝑚))) = ((𝐼𝑛)‘𝑗))
292287, 291eqtr2d 2787 . . . . . . . . . . . . . . . . . . 19 ((𝑚 ∈ ℕ ∧ (𝐹𝑚) = ⟨𝑛, 𝑗⟩) → ((𝐼𝑛)‘𝑗) = (𝐺𝑚))
293292coeq2d 5432 . . . . . . . . . . . . . . . . . 18 ((𝑚 ∈ ℕ ∧ (𝐹𝑚) = ⟨𝑛, 𝑗⟩) → ([,) ∘ ((𝐼𝑛)‘𝑗)) = ([,) ∘ (𝐺𝑚)))
294293fveq1d 6346 . . . . . . . . . . . . . . . . 17 ((𝑚 ∈ ℕ ∧ (𝐹𝑚) = ⟨𝑛, 𝑗⟩) → (([,) ∘ ((𝐼𝑛)‘𝑗))‘𝑘) = (([,) ∘ (𝐺𝑚))‘𝑘))
295294ixpeq2dv 8082 . . . . . . . . . . . . . . . 16 ((𝑚 ∈ ℕ ∧ (𝐹𝑚) = ⟨𝑛, 𝑗⟩) → X𝑘𝑋 (([,) ∘ ((𝐼𝑛)‘𝑗))‘𝑘) = X𝑘𝑋 (([,) ∘ (𝐺𝑚))‘𝑘))
296 eqimss 3790 . . . . . . . . . . . . . . . 16 (X𝑘𝑋 (([,) ∘ ((𝐼𝑛)‘𝑗))‘𝑘) = X𝑘𝑋 (([,) ∘ (𝐺𝑚))‘𝑘) → X𝑘𝑋 (([,) ∘ ((𝐼𝑛)‘𝑗))‘𝑘) ⊆ X𝑘𝑋 (([,) ∘ (𝐺𝑚))‘𝑘))
297295, 296syl 17 . . . . . . . . . . . . . . 15 ((𝑚 ∈ ℕ ∧ (𝐹𝑚) = ⟨𝑛, 𝑗⟩) → X𝑘𝑋 (([,) ∘ ((𝐼𝑛)‘𝑗))‘𝑘) ⊆ X𝑘𝑋 (([,) ∘ (𝐺𝑚))‘𝑘))
2982973adant1 1124 . . . . . . . . . . . . . 14 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑗 ∈ ℕ) ∧ 𝑚 ∈ ℕ ∧ (𝐹𝑚) = ⟨𝑛, 𝑗⟩) → X𝑘𝑋 (([,) ∘ ((𝐼𝑛)‘𝑗))‘𝑘) ⊆ X𝑘𝑋 (([,) ∘ (𝐺𝑚))‘𝑘))
299 rspe 3133 . . . . . . . . . . . . . 14 ((𝑚 ∈ {𝑖 ∈ ℕ ∣ (1st ‘(𝐹𝑖)) = 𝑛} ∧ X𝑘𝑋 (([,) ∘ ((𝐼𝑛)‘𝑗))‘𝑘) ⊆ X𝑘𝑋 (([,) ∘ (𝐺𝑚))‘𝑘)) → ∃𝑚 ∈ {𝑖 ∈ ℕ ∣ (1st ‘(𝐹𝑖)) = 𝑛}X𝑘𝑋 (([,) ∘ ((𝐼𝑛)‘𝑗))‘𝑘) ⊆ X𝑘𝑋 (([,) ∘ (𝐺𝑚))‘𝑘))
300286, 298, 299syl2anc 696 . . . . . . . . . . . . 13 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑗 ∈ ℕ) ∧ 𝑚 ∈ ℕ ∧ (𝐹𝑚) = ⟨𝑛, 𝑗⟩) → ∃𝑚 ∈ {𝑖 ∈ ℕ ∣ (1st ‘(𝐹𝑖)) = 𝑛}X𝑘𝑋 (([,) ∘ ((𝐼𝑛)‘𝑗))‘𝑘) ⊆ X𝑘𝑋 (([,) ∘ (𝐺𝑚))‘𝑘))
3013003exp 1112 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → (𝑚 ∈ ℕ → ((𝐹𝑚) = ⟨𝑛, 𝑗⟩ → ∃𝑚 ∈ {𝑖 ∈ ℕ ∣ (1st ‘(𝐹𝑖)) = 𝑛}X𝑘𝑋 (([,) ∘ ((𝐼𝑛)‘𝑗))‘𝑘) ⊆ X𝑘𝑋 (([,) ∘ (𝐺𝑚))‘𝑘))))
302269, 270, 301rexlimd 3156 . . . . . . . . . . 11 (((𝜑𝑛 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → (∃𝑚 ∈ ℕ (𝐹𝑚) = ⟨𝑛, 𝑗⟩ → ∃𝑚 ∈ {𝑖 ∈ ℕ ∣ (1st ‘(𝐹𝑖)) = 𝑛}X𝑘𝑋 (([,) ∘ ((𝐼𝑛)‘𝑗))‘𝑘) ⊆ X𝑘𝑋 (([,) ∘ (𝐺𝑚))‘𝑘)))
303268, 302mpd 15 . . . . . . . . . 10 (((𝜑𝑛 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → ∃𝑚 ∈ {𝑖 ∈ ℕ ∣ (1st ‘(𝐹𝑖)) = 𝑛}X𝑘𝑋 (([,) ∘ ((𝐼𝑛)‘𝑗))‘𝑘) ⊆ X𝑘𝑋 (([,) ∘ (𝐺𝑚))‘𝑘))
304303ralrimiva 3096 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → ∀𝑗 ∈ ℕ ∃𝑚 ∈ {𝑖 ∈ ℕ ∣ (1st ‘(𝐹𝑖)) = 𝑛}X𝑘𝑋 (([,) ∘ ((𝐼𝑛)‘𝑗))‘𝑘) ⊆ X𝑘𝑋 (([,) ∘ (𝐺𝑚))‘𝑘))
305 iunss2 4709 . . . . . . . . 9 (∀𝑗 ∈ ℕ ∃𝑚 ∈ {𝑖 ∈ ℕ ∣ (1st ‘(𝐹𝑖)) = 𝑛}X𝑘𝑋 (([,) ∘ ((𝐼𝑛)‘𝑗))‘𝑘) ⊆ X𝑘𝑋 (([,) ∘ (𝐺𝑚))‘𝑘) → 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ ((𝐼𝑛)‘𝑗))‘𝑘) ⊆ 𝑚 ∈ {𝑖 ∈ ℕ ∣ (1st ‘(𝐹𝑖)) = 𝑛}X𝑘𝑋 (([,) ∘ (𝐺𝑚))‘𝑘))
306304, 305syl 17 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ ((𝐼𝑛)‘𝑗))‘𝑘) ⊆ 𝑚 ∈ {𝑖 ∈ ℕ ∣ (1st ‘(𝐹𝑖)) = 𝑛}X𝑘𝑋 (([,) ∘ (𝐺𝑚))‘𝑘))
307261, 306sstrd 3746 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → (𝐴𝑛) ⊆ 𝑚 ∈ {𝑖 ∈ ℕ ∣ (1st ‘(𝐹𝑖)) = 𝑛}X𝑘𝑋 (([,) ∘ (𝐺𝑚))‘𝑘))
308 ssrab2 3820 . . . . . . . . 9 {𝑖 ∈ ℕ ∣ (1st ‘(𝐹𝑖)) = 𝑛} ⊆ ℕ
309 iunss1 4676 . . . . . . . . 9 ({𝑖 ∈ ℕ ∣ (1st ‘(𝐹𝑖)) = 𝑛} ⊆ ℕ → 𝑚 ∈ {𝑖 ∈ ℕ ∣ (1st ‘(𝐹𝑖)) = 𝑛}X𝑘𝑋 (([,) ∘ (𝐺𝑚))‘𝑘) ⊆ 𝑚 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝐺𝑚))‘𝑘))
310308, 309ax-mp 5 . . . . . . . 8 𝑚 ∈ {𝑖 ∈ ℕ ∣ (1st ‘(𝐹𝑖)) = 𝑛}X𝑘𝑋 (([,) ∘ (𝐺𝑚))‘𝑘) ⊆ 𝑚 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝐺𝑚))‘𝑘)
311310a1i 11 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → 𝑚 ∈ {𝑖 ∈ ℕ ∣ (1st ‘(𝐹𝑖)) = 𝑛}X𝑘𝑋 (([,) ∘ (𝐺𝑚))‘𝑘) ⊆ 𝑚 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝐺𝑚))‘𝑘))
312307, 311sstrd 3746 . . . . . 6 ((𝜑𝑛 ∈ ℕ) → (𝐴𝑛) ⊆ 𝑚 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝐺𝑚))‘𝑘))
313312ralrimiva 3096 . . . . 5 (𝜑 → ∀𝑛 ∈ ℕ (𝐴𝑛) ⊆ 𝑚 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝐺𝑚))‘𝑘))
314 iunss 4705 . . . . 5 ( 𝑛 ∈ ℕ (𝐴𝑛) ⊆ 𝑚 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝐺𝑚))‘𝑘) ↔ ∀𝑛 ∈ ℕ (𝐴𝑛) ⊆ 𝑚 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝐺𝑚))‘𝑘))
315313, 314sylibr 224 . . . 4 (𝜑 𝑛 ∈ ℕ (𝐴𝑛) ⊆ 𝑚 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝐺𝑚))‘𝑘))
3161, 130, 19, 245, 315ovnlecvr 41270 . . 3 (𝜑 → ((voln*‘𝑋)‘ 𝑛 ∈ ℕ (𝐴𝑛)) ≤ (Σ^‘(𝑚 ∈ ℕ ↦ (𝐿‘(𝐺𝑚)))))
317116fveq2d 6348 . . . . . . 7 ((𝜑𝑚 ∈ ℕ) → (𝐿‘(𝐺𝑚)) = (𝐿‘((𝐼‘(1st ‘(𝐹𝑚)))‘(2nd ‘(𝐹𝑚)))))
318317mpteq2dva 4888 . . . . . 6 (𝜑 → (𝑚 ∈ ℕ ↦ (𝐿‘(𝐺𝑚))) = (𝑚 ∈ ℕ ↦ (𝐿‘((𝐼‘(1st ‘(𝐹𝑚)))‘(2nd ‘(𝐹𝑚))))))
319318fveq2d 6348 . . . . 5 (𝜑 → (Σ^‘(𝑚 ∈ ℕ ↦ (𝐿‘(𝐺𝑚)))) = (Σ^‘(𝑚 ∈ ℕ ↦ (𝐿‘((𝐼‘(1st ‘(𝐹𝑚)))‘(2nd ‘(𝐹𝑚)))))))
320 nfv 1984 . . . . . 6 𝑝𝜑
321 fveq2 6344 . . . . . . . . 9 (𝑝 = (𝐹𝑚) → (1st𝑝) = (1st ‘(𝐹𝑚)))
322321fveq2d 6348 . . . . . . . 8 (𝑝 = (𝐹𝑚) → (𝐼‘(1st𝑝)) = (𝐼‘(1st ‘(𝐹𝑚))))
323 fveq2 6344 . . . . . . . 8 (𝑝 = (𝐹𝑚) → (2nd𝑝) = (2nd ‘(𝐹𝑚)))
324322, 323fveq12d 6350 . . . . . . 7 (𝑝 = (𝐹𝑚) → ((𝐼‘(1st𝑝))‘(2nd𝑝)) = ((𝐼‘(1st ‘(𝐹𝑚)))‘(2nd ‘(𝐹𝑚))))
325324fveq2d 6348 . . . . . 6 (𝑝 = (𝐹𝑚) → (𝐿‘((𝐼‘(1st𝑝))‘(2nd𝑝))) = (𝐿‘((𝐼‘(1st ‘(𝐹𝑚)))‘(2nd ‘(𝐹𝑚)))))
326 eqidd 2753 . . . . . 6 ((𝜑𝑚 ∈ ℕ) → (𝐹𝑚) = (𝐹𝑚))
327 nfv 1984 . . . . . . . 8 𝑘(𝜑𝑝 ∈ (ℕ × ℕ))
3281adantr 472 . . . . . . . 8 ((𝜑𝑝 ∈ (ℕ × ℕ)) → 𝑋 ∈ Fin)
329 simpl 474 . . . . . . . . 9 ((𝜑𝑝 ∈ (ℕ × ℕ)) → 𝜑)
330 xp1st 7357 . . . . . . . . . 10 (𝑝 ∈ (ℕ × ℕ) → (1st𝑝) ∈ ℕ)
331330adantl 473 . . . . . . . . 9 ((𝜑𝑝 ∈ (ℕ × ℕ)) → (1st𝑝) ∈ ℕ)
332 xp2nd 7358 . . . . . . . . . 10 (𝑝 ∈ (ℕ × ℕ) → (2nd𝑝) ∈ ℕ)
333332adantl 473 . . . . . . . . 9 ((𝜑𝑝 ∈ (ℕ × ℕ)) → (2nd𝑝) ∈ ℕ)
334 fvex 6354 . . . . . . . . . 10 (2nd𝑝) ∈ V
335 eleq1 2819 . . . . . . . . . . . 12 (𝑗 = (2nd𝑝) → (𝑗 ∈ ℕ ↔ (2nd𝑝) ∈ ℕ))
3363353anbi3d 1546 . . . . . . . . . . 11 (𝑗 = (2nd𝑝) → ((𝜑 ∧ (1st𝑝) ∈ ℕ ∧ 𝑗 ∈ ℕ) ↔ (𝜑 ∧ (1st𝑝) ∈ ℕ ∧ (2nd𝑝) ∈ ℕ)))
337 fveq2 6344 . . . . . . . . . . . 12 (𝑗 = (2nd𝑝) → ((𝐼‘(1st𝑝))‘𝑗) = ((𝐼‘(1st𝑝))‘(2nd𝑝)))
338337feq1d 6183 . . . . . . . . . . 11 (𝑗 = (2nd𝑝) → (((𝐼‘(1st𝑝))‘𝑗):𝑋⟶(ℝ × ℝ) ↔ ((𝐼‘(1st𝑝))‘(2nd𝑝)):𝑋⟶(ℝ × ℝ)))
339336, 338imbi12d 333 . . . . . . . . . 10 (𝑗 = (2nd𝑝) → (((𝜑 ∧ (1st𝑝) ∈ ℕ ∧ 𝑗 ∈ ℕ) → ((𝐼‘(1st𝑝))‘𝑗):𝑋⟶(ℝ × ℝ)) ↔ ((𝜑 ∧ (1st𝑝) ∈ ℕ ∧ (2nd𝑝) ∈ ℕ) → ((𝐼‘(1st𝑝))‘(2nd𝑝)):𝑋⟶(ℝ × ℝ))))
340 fvex 6354 . . . . . . . . . . 11 (1st𝑝) ∈ V
341 eleq1 2819 . . . . . . . . . . . . 13 (𝑛 = (1st𝑝) → (𝑛 ∈ ℕ ↔ (1st𝑝) ∈ ℕ))
3423413anbi2d 1545 . . . . . . . . . . . 12 (𝑛 = (1st𝑝) → ((𝜑𝑛 ∈ ℕ ∧ 𝑗 ∈ ℕ) ↔ (𝜑 ∧ (1st𝑝) ∈ ℕ ∧ 𝑗 ∈ ℕ)))
343 fveq2 6344 . . . . . . . . . . . . . 14 (𝑛 = (1st𝑝) → (𝐼𝑛) = (𝐼‘(1st𝑝)))
344343fveq1d 6346 . . . . . . . . . . . . 13 (𝑛 = (1st𝑝) → ((𝐼𝑛)‘𝑗) = ((𝐼‘(1st𝑝))‘𝑗))
345344feq1d 6183 . . . . . . . . . . . 12 (𝑛 = (1st𝑝) → (((𝐼𝑛)‘𝑗):𝑋⟶(ℝ × ℝ) ↔ ((𝐼‘(1st𝑝))‘𝑗):𝑋⟶(ℝ × ℝ)))
346342, 345imbi12d 333 . . . . . . . . . . 11 (𝑛 = (1st𝑝) → (((𝜑𝑛 ∈ ℕ ∧ 𝑗 ∈ ℕ) → ((𝐼𝑛)‘𝑗):𝑋⟶(ℝ × ℝ)) ↔ ((𝜑 ∧ (1st𝑝) ∈ ℕ ∧ 𝑗 ∈ ℕ) → ((𝐼‘(1st𝑝))‘𝑗):𝑋⟶(ℝ × ℝ))))
347340, 346, 106vtocl 3391 . . . . . . . . . 10 ((𝜑 ∧ (1st𝑝) ∈ ℕ ∧ 𝑗 ∈ ℕ) → ((𝐼‘(1st𝑝))‘𝑗):𝑋⟶(ℝ × ℝ))
348334, 339, 347vtocl 3391 . . . . . . . . 9 ((𝜑 ∧ (1st𝑝) ∈ ℕ ∧ (2nd𝑝) ∈ ℕ) → ((𝐼‘(1st𝑝))‘(2nd𝑝)):𝑋⟶(ℝ × ℝ))
349329, 331, 333, 348syl3anc 1473 . . . . . . . 8 ((𝜑𝑝 ∈ (ℕ × ℕ)) → ((𝐼‘(1st𝑝))‘(2nd𝑝)):𝑋⟶(ℝ × ℝ))
350327, 328, 19, 349hoiprodcl2 41267 . . . . . . 7 ((𝜑𝑝 ∈ (ℕ × ℕ)) → (𝐿‘((𝐼‘(1st𝑝))‘(2nd𝑝))) ∈ (0[,)+∞))
35115, 350sseldi 3734 . . . . . 6 ((𝜑𝑝 ∈ (ℕ × ℕ)) → (𝐿‘((𝐼‘(1st𝑝))‘(2nd𝑝))) ∈ (0[,]+∞))
352320, 12, 325, 14, 20, 326, 351sge0f1o 41094 . . . . 5 (𝜑 → (Σ^‘(𝑝 ∈ (ℕ × ℕ) ↦ (𝐿‘((𝐼‘(1st𝑝))‘(2nd𝑝))))) = (Σ^‘(𝑚 ∈ ℕ ↦ (𝐿‘((𝐼‘(1st ‘(𝐹𝑚)))‘(2nd ‘(𝐹𝑚)))))))
353319, 352eqtr4d 2789 . . . 4 (𝜑 → (Σ^‘(𝑚 ∈ ℕ ↦ (𝐿‘(𝐺𝑚)))) = (Σ^‘(𝑝 ∈ (ℕ × ℕ) ↦ (𝐿‘((𝐼‘(1st𝑝))‘(2nd𝑝))))))
354 nfv 1984 . . . . . . 7 𝑗𝜑
355273, 274op1std 7335 . . . . . . . . . 10 (𝑝 = ⟨𝑛, 𝑗⟩ → (1st𝑝) = 𝑛)
356355fveq2d 6348 . . . . . . . . 9 (𝑝 = ⟨𝑛, 𝑗⟩ → (𝐼‘(1st𝑝)) = (𝐼𝑛))
357273, 274op2ndd 7336 . . . . . . . . 9 (𝑝 = ⟨𝑛, 𝑗⟩ → (2nd𝑝) = 𝑗)
358356, 357fveq12d 6350 . . . . . . . 8 (𝑝 = ⟨𝑛, 𝑗⟩ → ((𝐼‘(1st𝑝))‘(2nd𝑝)) = ((𝐼𝑛)‘𝑗))
359358fveq2d 6348 . . . . . . 7 (𝑝 = ⟨𝑛, 𝑗⟩ → (𝐿‘((𝐼‘(1st𝑝))‘(2nd𝑝))) = (𝐿‘((𝐼𝑛)‘𝑗)))
360 nfv 1984 . . . . . . . . . 10 𝑘((𝜑𝑛 ∈ ℕ) ∧ 𝑗 ∈ ℕ)
361127adantr 472 . . . . . . . . . 10 (((𝜑𝑛 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → 𝑋 ∈ Fin)
36297, 105syl 17 . . . . . . . . . 10 (((𝜑𝑛 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → ((𝐼𝑛)‘𝑗):𝑋⟶(ℝ × ℝ))
363360, 361, 19, 362hoiprodcl2 41267 . . . . . . . . 9 (((𝜑𝑛 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → (𝐿‘((𝐼𝑛)‘𝑗)) ∈ (0[,)+∞))
36415, 363sseldi 3734 . . . . . . . 8 (((𝜑𝑛 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → (𝐿‘((𝐼𝑛)‘𝑗)) ∈ (0[,]+∞))
3653643impa 1100 . . . . . . 7 ((𝜑𝑛 ∈ ℕ ∧ 𝑗 ∈ ℕ) → (𝐿‘((𝐼𝑛)‘𝑗)) ∈ (0[,]+∞))
366354, 359, 14, 14, 365sge0xp 41141 . . . . . 6 (𝜑 → (Σ^‘(𝑛 ∈ ℕ ↦ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘((𝐼𝑛)‘𝑗)))))) = (Σ^‘(𝑝 ∈ (ℕ × ℕ) ↦ (𝐿‘((𝐼‘(1st𝑝))‘(2nd𝑝))))))
367366eqcomd 2758 . . . . 5 (𝜑 → (Σ^‘(𝑝 ∈ (ℕ × ℕ) ↦ (𝐿‘((𝐼‘(1st𝑝))‘(2nd𝑝))))) = (Σ^‘(𝑛 ∈ ℕ ↦ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘((𝐼𝑛)‘𝑗)))))))
36813a1i 11 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → ℕ ∈ V)
369 eqid 2752 . . . . . . . 8 (𝑗 ∈ ℕ ↦ (𝐿‘((𝐼𝑛)‘𝑗))) = (𝑗 ∈ ℕ ↦ (𝐿‘((𝐼𝑛)‘𝑗)))
370364, 369fmptd 6540 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → (𝑗 ∈ ℕ ↦ (𝐿‘((𝐼𝑛)‘𝑗))):ℕ⟶(0[,]+∞))
371368, 370sge0cl 41093 . . . . . 6 ((𝜑𝑛 ∈ ℕ) → (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘((𝐼𝑛)‘𝑗)))) ∈ (0[,]+∞))
372 fveq1 6343 . . . . . . . . . . . . 13 (𝑖 = (𝐼𝑛) → (𝑖𝑗) = ((𝐼𝑛)‘𝑗))
373372fveq2d 6348 . . . . . . . . . . . 12 (𝑖 = (𝐼𝑛) → (𝐿‘(𝑖𝑗)) = (𝐿‘((𝐼𝑛)‘𝑗)))
374373mpteq2dv 4889 . . . . . . . . . . 11 (𝑖 = (𝐼𝑛) → (𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗))) = (𝑗 ∈ ℕ ↦ (𝐿‘((𝐼𝑛)‘𝑗))))
375374fveq2d 6348 . . . . . . . . . 10 (𝑖 = (𝐼𝑛) → (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) = (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘((𝐼𝑛)‘𝑗)))))
376375breq1d 4806 . . . . . . . . 9 (𝑖 = (𝐼𝑛) → ((Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛))) ↔ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘((𝐼𝑛)‘𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛)))))
377376elrab 3496 . . . . . . . 8 ((𝐼𝑛) ∈ {𝑖 ∈ (𝐶‘(𝐴𝑛)) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛)))} ↔ ((𝐼𝑛) ∈ (𝐶‘(𝐴𝑛)) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘((𝐼𝑛)‘𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛)))))
378247, 377sylib 208 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → ((𝐼𝑛) ∈ (𝐶‘(𝐴𝑛)) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘((𝐼𝑛)‘𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛)))))
379378simprd 482 . . . . . 6 ((𝜑𝑛 ∈ ℕ) → (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘((𝐼𝑛)‘𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛))))
380122, 14, 371, 179, 379sge0lempt 41122 . . . . 5 (𝜑 → (Σ^‘(𝑛 ∈ ℕ ↦ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘((𝐼𝑛)‘𝑗)))))) ≤ (Σ^‘(𝑛 ∈ ℕ ↦ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛))))))
381367, 380eqbrtrd 4818 . . . 4 (𝜑 → (Σ^‘(𝑝 ∈ (ℕ × ℕ) ↦ (𝐿‘((𝐼‘(1st𝑝))‘(2nd𝑝))))) ≤ (Σ^‘(𝑛 ∈ ℕ ↦ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛))))))
382353, 381eqbrtrd 4818 . . 3 (𝜑 → (Σ^‘(𝑚 ∈ ℕ ↦ (𝐿‘(𝐺𝑚)))) ≤ (Σ^‘(𝑛 ∈ ℕ ↦ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛))))))
38311, 121, 180, 316, 382xrletrd 12178 . 2 (𝜑 → ((voln*‘𝑋)‘ 𝑛 ∈ ℕ (𝐴𝑛)) ≤ (Σ^‘(𝑛 ∈ ℕ ↦ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛))))))
384122, 14, 166, 174sge0xadd 41147 . . 3 (𝜑 → (Σ^‘(𝑛 ∈ ℕ ↦ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛))))) = ((Σ^‘(𝑛 ∈ ℕ ↦ ((voln*‘𝑋)‘(𝐴𝑛)))) +𝑒^‘(𝑛 ∈ ℕ ↦ (𝐸 / (2↑𝑛))))))
385123a1i 11 . . . . . 6 (𝜑 → 0 ∈ ℝ*)
386125a1i 11 . . . . . 6 (𝜑 → +∞ ∈ ℝ*)
387151rexrd 10273 . . . . . 6 (𝜑𝐸 ∈ ℝ*)
38874rpge0d 12061 . . . . . 6 (𝜑 → 0 ≤ 𝐸)
389151ltpnfd 12140 . . . . . 6 (𝜑𝐸 < +∞)
390385, 386, 387, 388, 389elicod 12409 . . . . 5 (𝜑𝐸 ∈ (0[,)+∞))
391390sge0ad2en 41143 . . . 4 (𝜑 → (Σ^‘(𝑛 ∈ ℕ ↦ (𝐸 / (2↑𝑛)))) = 𝐸)
392391oveq2d 6821 . . 3 (𝜑 → ((Σ^‘(𝑛 ∈ ℕ ↦ ((voln*‘𝑋)‘(𝐴𝑛)))) +𝑒^‘(𝑛 ∈ ℕ ↦ (𝐸 / (2↑𝑛))))) = ((Σ^‘(𝑛 ∈ ℕ ↦ ((voln*‘𝑋)‘(𝐴𝑛)))) +𝑒 𝐸))
393384, 392eqtrd 2786 . 2 (𝜑 → (Σ^‘(𝑛 ∈ ℕ ↦ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛))))) = ((Σ^‘(𝑛 ∈ ℕ ↦ ((voln*‘𝑋)‘(𝐴𝑛)))) +𝑒 𝐸))
394383, 393breqtrd 4822 1 (𝜑 → ((voln*‘𝑋)‘ 𝑛 ∈ ℕ (𝐴𝑛)) ≤ ((Σ^‘(𝑛 ∈ ℕ ↦ ((voln*‘𝑋)‘(𝐴𝑛)))) +𝑒 𝐸))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3a 1072   = wceq 1624  wcel 2131  wne 2924  wral 3042  wrex 3043  {crab 3046  Vcvv 3332  wss 3707  c0 4050  ifcif 4222  𝒫 cpw 4294  cop 4319   ciun 4664   class class class wbr 4796  cmpt 4873   × cxp 5256  ccom 5262   Fn wfn 6036  wf 6037  ontowfo 6039  1-1-ontowf1o 6040  cfv 6041  (class class class)co 6805  1st c1st 7323  2nd c2nd 7324  𝑚 cmap 8015  Xcixp 8066  Fincfn 8113  infcinf 8504  cr 10119  0cc0 10120  +∞cpnf 10255  *cxr 10257   < clt 10258  cle 10259   / cdiv 10868  cn 11204  2c2 11254  +crp 12017   +𝑒 cxad 12129  [,)cico 12362  [,]cicc 12363  cexp 13046  cprod 14826  volcvol 23424  Σ^csumge0 41074  voln*covoln 41248
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863  ax-4 1878  ax-5 1980  ax-6 2046  ax-7 2082  ax-8 2133  ax-9 2140  ax-10 2160  ax-11 2175  ax-12 2188  ax-13 2383  ax-ext 2732  ax-rep 4915  ax-sep 4925  ax-nul 4933  ax-pow 4984  ax-pr 5047  ax-un 7106  ax-inf2 8703  ax-ac2 9469  ax-cnex 10176  ax-resscn 10177  ax-1cn 10178  ax-icn 10179  ax-addcl 10180  ax-addrcl 10181  ax-mulcl 10182  ax-mulrcl 10183  ax-mulcom 10184  ax-addass 10185  ax-mulass 10186  ax-distr 10187  ax-i2m1 10188  ax-1ne0 10189  ax-1rid 10190  ax-rnegex 10191  ax-rrecex 10192  ax-cnre 10193  ax-pre-lttri 10194  ax-pre-lttrn 10195  ax-pre-ltadd 10196  ax-pre-mulgt0 10197  ax-pre-sup 10198  ax-addf 10199  ax-mulf 10200
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1627  df-fal 1630  df-ex 1846  df-nf 1851  df-sb 2039  df-eu 2603  df-mo 2604  df-clab 2739  df-cleq 2745  df-clel 2748  df-nfc 2883  df-ne 2925  df-nel 3028  df-ral 3047  df-rex 3048  df-reu 3049  df-rmo 3050  df-rab 3051  df-v 3334  df-sbc 3569  df-csb 3667  df-dif 3710  df-un 3712  df-in 3714  df-ss 3721  df-pss 3723  df-nul 4051  df-if 4223  df-pw 4296  df-sn 4314  df-pr 4316  df-tp 4318  df-op 4320  df-uni 4581  df-int 4620  df-iun 4666  df-disj 4765  df-br 4797  df-opab 4857  df-mpt 4874  df-tr 4897  df-id 5166  df-eprel 5171  df-po 5179  df-so 5180  df-fr 5217  df-se 5218  df-we 5219  df-xp 5264  df-rel 5265  df-cnv 5266  df-co 5267  df-dm 5268  df-rn 5269  df-res 5270  df-ima 5271  df-pred 5833  df-ord 5879  df-on 5880  df-lim 5881  df-suc 5882  df-iota 6004  df-fun 6043  df-fn 6044  df-f 6045  df-f1 6046  df-fo 6047  df-f1o 6048  df-fv 6049  df-isom 6050  df-riota 6766  df-ov 6808  df-oprab 6809  df-mpt2 6810  df-of 7054  df-om 7223  df-1st 7325  df-2nd 7326  df-tpos 7513  df-wrecs 7568  df-recs 7629  df-rdg 7667  df-1o 7721  df-2o 7722  df-oadd 7725  df-er 7903  df-map 8017  df-pm 8018  df-ixp 8067  df-en 8114  df-dom 8115  df-sdom 8116  df-fin 8117  df-fi 8474  df-sup 8505  df-inf 8506  df-oi 8572  df-card 8947  df-acn 8950  df-ac 9121  df-cda 9174  df-pnf 10260  df-mnf 10261  df-xr 10262  df-ltxr 10263  df-le 10264  df-sub 10452  df-neg 10453  df-div 10869  df-nn 11205  df-2 11263  df-3 11264  df-4 11265  df-5 11266  df-6 11267  df-7 11268  df-8 11269  df-9 11270  df-n0 11477  df-z 11562  df-dec 11678  df-uz 11872  df-q 11974  df-rp 12018  df-xneg 12131  df-xadd 12132  df-xmul 12133  df-ioo 12364  df-ico 12366  df-icc 12367  df-fz 12512  df-fzo 12652  df-fl 12779  df-seq 12988  df-exp 13047  df-hash 13304  df-cj 14030  df-re 14031  df-im 14032  df-sqrt 14166  df-abs 14167  df-clim 14410  df-rlim 14411  df-sum 14608  df-prod 14827  df-struct 16053  df-ndx 16054  df-slot 16055  df-base 16057  df-sets 16058  df-ress 16059  df-plusg 16148  df-mulr 16149  df-starv 16150  df-tset 16154  df-ple 16155  df-ds 16158  df-unif 16159  df-rest 16277  df-0g 16296  df-topgen 16298  df-mgm 17435  df-sgrp 17477  df-mnd 17488  df-grp 17618  df-minusg 17619  df-subg 17784  df-cmn 18387  df-abl 18388  df-mgp 18682  df-ur 18694  df-ring 18741  df-cring 18742  df-oppr 18815  df-dvdsr 18833  df-unit 18834  df-invr 18864  df-dvr 18875  df-drng 18943  df-psmet 19932  df-xmet 19933  df-met 19934  df-bl 19935  df-mopn 19936  df-cnfld 19941  df-top 20893  df-topon 20910  df-bases 20944  df-cmp 21384  df-ovol 23425  df-vol 23426  df-sumge0 41075  df-ovoln 41249
This theorem is referenced by:  ovnsubaddlem2  41283
  Copyright terms: Public domain W3C validator