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 41263
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 468 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → 𝐴:ℕ⟶𝒫 (ℝ ↑𝑚 𝑋))
4 simpr 473 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → 𝑛 ∈ ℕ)
53, 4ffvelrnd 6579 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → (𝐴𝑛) ∈ 𝒫 (ℝ ↑𝑚 𝑋))
6 elpwi 4358 . . . . . . 7 ((𝐴𝑛) ∈ 𝒫 (ℝ ↑𝑚 𝑋) → (𝐴𝑛) ⊆ (ℝ ↑𝑚 𝑋))
75, 6syl 17 . . . . . 6 ((𝜑𝑛 ∈ ℕ) → (𝐴𝑛) ⊆ (ℝ ↑𝑚 𝑋))
87ralrimiva 3153 . . . . 5 (𝜑 → ∀𝑛 ∈ ℕ (𝐴𝑛) ⊆ (ℝ ↑𝑚 𝑋))
9 iunss 4749 . . . . 5 ( 𝑛 ∈ ℕ (𝐴𝑛) ⊆ (ℝ ↑𝑚 𝑋) ↔ ∀𝑛 ∈ ℕ (𝐴𝑛) ⊆ (ℝ ↑𝑚 𝑋))
108, 9sylibr 225 . . . 4 (𝜑 𝑛 ∈ ℕ (𝐴𝑛) ⊆ (ℝ ↑𝑚 𝑋))
111, 10ovnxrcl 41262 . . 3 (𝜑 → ((voln*‘𝑋)‘ 𝑛 ∈ ℕ (𝐴𝑛)) ∈ ℝ*)
12 nfv 2008 . . . 4 𝑚𝜑
13 nnex 11308 . . . . 5 ℕ ∈ V
1413a1i 11 . . . 4 (𝜑 → ℕ ∈ V)
15 icossicc 12475 . . . . 5 (0[,)+∞) ⊆ (0[,]+∞)
16 nfv 2008 . . . . . 6 𝑘(𝜑𝑚 ∈ ℕ)
17 simpl 470 . . . . . . 7 ((𝜑𝑚 ∈ ℕ) → 𝜑)
1817, 1syl 17 . . . . . 6 ((𝜑𝑚 ∈ ℕ) → 𝑋 ∈ Fin)
19 ovnsubaddlem1.l . . . . . 6 𝐿 = (𝑖 ∈ ((ℝ × ℝ) ↑𝑚 𝑋) ↦ ∏𝑘𝑋 (vol‘(([,) ∘ 𝑖)‘𝑘)))
20 ovnsubaddlem1.f . . . . . . . . . . . 12 (𝜑𝐹:ℕ–1-1-onto→(ℕ × ℕ))
21 f1of 6350 . . . . . . . . . . . 12 (𝐹:ℕ–1-1-onto→(ℕ × ℕ) → 𝐹:ℕ⟶(ℕ × ℕ))
2220, 21syl 17 . . . . . . . . . . 11 (𝜑𝐹:ℕ⟶(ℕ × ℕ))
2322adantr 468 . . . . . . . . . 10 ((𝜑𝑚 ∈ ℕ) → 𝐹:ℕ⟶(ℕ × ℕ))
24 simpr 473 . . . . . . . . . 10 ((𝜑𝑚 ∈ ℕ) → 𝑚 ∈ ℕ)
2523, 24ffvelrnd 6579 . . . . . . . . 9 ((𝜑𝑚 ∈ ℕ) → (𝐹𝑚) ∈ (ℕ × ℕ))
26 xp1st 7427 . . . . . . . . 9 ((𝐹𝑚) ∈ (ℕ × ℕ) → (1st ‘(𝐹𝑚)) ∈ ℕ)
2725, 26syl 17 . . . . . . . 8 ((𝜑𝑚 ∈ ℕ) → (1st ‘(𝐹𝑚)) ∈ ℕ)
28 xp2nd 7428 . . . . . . . . 9 ((𝐹𝑚) ∈ (ℕ × ℕ) → (2nd ‘(𝐹𝑚)) ∈ ℕ)
2925, 28syl 17 . . . . . . . 8 ((𝜑𝑚 ∈ ℕ) → (2nd ‘(𝐹𝑚)) ∈ ℕ)
30 fvex 6418 . . . . . . . . 9 (2nd ‘(𝐹𝑚)) ∈ V
31 eleq1 2872 . . . . . . . . . . 11 (𝑗 = (2nd ‘(𝐹𝑚)) → (𝑗 ∈ ℕ ↔ (2nd ‘(𝐹𝑚)) ∈ ℕ))
32313anbi3d 1559 . . . . . . . . . 10 (𝑗 = (2nd ‘(𝐹𝑚)) → ((𝜑 ∧ (1st ‘(𝐹𝑚)) ∈ ℕ ∧ 𝑗 ∈ ℕ) ↔ (𝜑 ∧ (1st ‘(𝐹𝑚)) ∈ ℕ ∧ (2nd ‘(𝐹𝑚)) ∈ ℕ)))
33 fveq2 6405 . . . . . . . . . . 11 (𝑗 = (2nd ‘(𝐹𝑚)) → ((𝐼‘(1st ‘(𝐹𝑚)))‘𝑗) = ((𝐼‘(1st ‘(𝐹𝑚)))‘(2nd ‘(𝐹𝑚))))
3433feq1d 6238 . . . . . . . . . 10 (𝑗 = (2nd ‘(𝐹𝑚)) → (((𝐼‘(1st ‘(𝐹𝑚)))‘𝑗):𝑋⟶(ℝ × ℝ) ↔ ((𝐼‘(1st ‘(𝐹𝑚)))‘(2nd ‘(𝐹𝑚))):𝑋⟶(ℝ × ℝ)))
3532, 34imbi12d 335 . . . . . . . . 9 (𝑗 = (2nd ‘(𝐹𝑚)) → (((𝜑 ∧ (1st ‘(𝐹𝑚)) ∈ ℕ ∧ 𝑗 ∈ ℕ) → ((𝐼‘(1st ‘(𝐹𝑚)))‘𝑗):𝑋⟶(ℝ × ℝ)) ↔ ((𝜑 ∧ (1st ‘(𝐹𝑚)) ∈ ℕ ∧ (2nd ‘(𝐹𝑚)) ∈ ℕ) → ((𝐼‘(1st ‘(𝐹𝑚)))‘(2nd ‘(𝐹𝑚))):𝑋⟶(ℝ × ℝ))))
36 fvex 6418 . . . . . . . . . 10 (1st ‘(𝐹𝑚)) ∈ V
37 eleq1 2872 . . . . . . . . . . . 12 (𝑛 = (1st ‘(𝐹𝑚)) → (𝑛 ∈ ℕ ↔ (1st ‘(𝐹𝑚)) ∈ ℕ))
38373anbi2d 1558 . . . . . . . . . . 11 (𝑛 = (1st ‘(𝐹𝑚)) → ((𝜑𝑛 ∈ ℕ ∧ 𝑗 ∈ ℕ) ↔ (𝜑 ∧ (1st ‘(𝐹𝑚)) ∈ ℕ ∧ 𝑗 ∈ ℕ)))
39 fveq2 6405 . . . . . . . . . . . . 13 (𝑛 = (1st ‘(𝐹𝑚)) → (𝐼𝑛) = (𝐼‘(1st ‘(𝐹𝑚))))
4039fveq1d 6407 . . . . . . . . . . . 12 (𝑛 = (1st ‘(𝐹𝑚)) → ((𝐼𝑛)‘𝑗) = ((𝐼‘(1st ‘(𝐹𝑚)))‘𝑗))
4140feq1d 6238 . . . . . . . . . . 11 (𝑛 = (1st ‘(𝐹𝑚)) → (((𝐼𝑛)‘𝑗):𝑋⟶(ℝ × ℝ) ↔ ((𝐼‘(1st ‘(𝐹𝑚)))‘𝑗):𝑋⟶(ℝ × ℝ)))
4238, 41imbi12d 335 . . . . . . . . . 10 (𝑛 = (1st ‘(𝐹𝑚)) → (((𝜑𝑛 ∈ ℕ ∧ 𝑗 ∈ ℕ) → ((𝐼𝑛)‘𝑗):𝑋⟶(ℝ × ℝ)) ↔ ((𝜑 ∧ (1st ‘(𝐹𝑚)) ∈ ℕ ∧ 𝑗 ∈ ℕ) → ((𝐼‘(1st ‘(𝐹𝑚)))‘𝑗):𝑋⟶(ℝ × ℝ))))
43 ovnsubaddlem1.c . . . . . . . . . . . . . . . . . . . 20 𝐶 = (𝑎 ∈ 𝒫 (ℝ ↑𝑚 𝑋) ↦ { ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∣ 𝑎 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘)})
4443a1i 11 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑛 ∈ ℕ) → 𝐶 = (𝑎 ∈ 𝒫 (ℝ ↑𝑚 𝑋) ↦ { ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∣ 𝑎 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘)}))
45 sseq1 3820 . . . . . . . . . . . . . . . . . . . . 21 (𝑎 = (𝐴𝑛) → (𝑎 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘) ↔ (𝐴𝑛) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘)))
4645rabbidv 3378 . . . . . . . . . . . . . . . . . . . 20 (𝑎 = (𝐴𝑛) → { ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∣ 𝑎 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘)} = { ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∣ (𝐴𝑛) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘)})
4746adantl 469 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑛 ∈ ℕ) ∧ 𝑎 = (𝐴𝑛)) → { ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∣ 𝑎 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘)} = { ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∣ (𝐴𝑛) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘)})
48 ovex 6903 . . . . . . . . . . . . . . . . . . . . 21 (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∈ V
4948rabex 5004 . . . . . . . . . . . . . . . . . . . 20 { ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∣ (𝐴𝑛) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘)} ∈ V
5049a1i 11 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑛 ∈ ℕ) → { ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∣ (𝐴𝑛) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘)} ∈ V)
5144, 47, 5, 50fvmptd 6506 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑛 ∈ ℕ) → (𝐶‘(𝐴𝑛)) = { ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∣ (𝐴𝑛) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘)})
52 ssrab2 3881 . . . . . . . . . . . . . . . . . . 19 { ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∣ (𝐴𝑛) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘)} ⊆ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)
5352a1i 11 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑛 ∈ ℕ) → { ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∣ (𝐴𝑛) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘)} ⊆ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ))
5451, 53eqsstrd 3833 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛 ∈ ℕ) → (𝐶‘(𝐴𝑛)) ⊆ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ))
55 ovnsubaddlem1.d . . . . . . . . . . . . . . . . . . . . . 22 𝐷 = (𝑎 ∈ 𝒫 (ℝ ↑𝑚 𝑋) ↦ (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶𝑎) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘𝑎) +𝑒 𝑒)}))
5655a1i 11 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑛 ∈ ℕ) → 𝐷 = (𝑎 ∈ 𝒫 (ℝ ↑𝑚 𝑋) ↦ (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶𝑎) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘𝑎) +𝑒 𝑒)})))
57 fveq2 6405 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑎 = (𝐴𝑛) → (𝐶𝑎) = (𝐶‘(𝐴𝑛)))
5857eleq2d 2870 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑎 = (𝐴𝑛) → (𝑖 ∈ (𝐶𝑎) ↔ 𝑖 ∈ (𝐶‘(𝐴𝑛))))
59 fveq2 6405 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑎 = (𝐴𝑛) → ((voln*‘𝑋)‘𝑎) = ((voln*‘𝑋)‘(𝐴𝑛)))
6059oveq1d 6886 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑎 = (𝐴𝑛) → (((voln*‘𝑋)‘𝑎) +𝑒 𝑒) = (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 𝑒))
6160breq2d 4852 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑎 = (𝐴𝑛) → ((Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘𝑎) +𝑒 𝑒) ↔ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 𝑒)))
6258, 61anbi12d 618 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑎 = (𝐴𝑛) → ((𝑖 ∈ (𝐶𝑎) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘𝑎) +𝑒 𝑒)) ↔ (𝑖 ∈ (𝐶‘(𝐴𝑛)) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 𝑒))))
6362rabbidva2 3375 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑎 = (𝐴𝑛) → {𝑖 ∈ (𝐶𝑎) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘𝑎) +𝑒 𝑒)} = {𝑖 ∈ (𝐶‘(𝐴𝑛)) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 𝑒)})
6463mpteq2dv 4935 . . . . . . . . . . . . . . . . . . . . . 22 (𝑎 = (𝐴𝑛) → (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶𝑎) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘𝑎) +𝑒 𝑒)}) = (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶‘(𝐴𝑛)) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 𝑒)}))
6564adantl 469 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑛 ∈ ℕ) ∧ 𝑎 = (𝐴𝑛)) → (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶𝑎) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘𝑎) +𝑒 𝑒)}) = (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶‘(𝐴𝑛)) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 𝑒)}))
66 rpex 40039 . . . . . . . . . . . . . . . . . . . . . . 23 + ∈ V
6766mptex 6708 . . . . . . . . . . . . . . . . . . . . . 22 (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶‘(𝐴𝑛)) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 𝑒)}) ∈ V
6867a1i 11 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑛 ∈ ℕ) → (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶‘(𝐴𝑛)) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 𝑒)}) ∈ V)
6956, 65, 5, 68fvmptd 6506 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑛 ∈ ℕ) → (𝐷‘(𝐴𝑛)) = (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶‘(𝐴𝑛)) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 𝑒)}))
70 oveq2 6879 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑒 = (𝐸 / (2↑𝑛)) → (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 𝑒) = (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛))))
7170breq2d 4852 . . . . . . . . . . . . . . . . . . . . . 22 (𝑒 = (𝐸 / (2↑𝑛)) → ((Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 𝑒) ↔ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛)))))
7271rabbidv 3378 . . . . . . . . . . . . . . . . . . . . 21 (𝑒 = (𝐸 / (2↑𝑛)) → {𝑖 ∈ (𝐶‘(𝐴𝑛)) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 𝑒)} = {𝑖 ∈ (𝐶‘(𝐴𝑛)) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛)))})
7372adantl 469 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑛 ∈ ℕ) ∧ 𝑒 = (𝐸 / (2↑𝑛))) → {𝑖 ∈ (𝐶‘(𝐴𝑛)) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 𝑒)} = {𝑖 ∈ (𝐶‘(𝐴𝑛)) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛)))})
74 ovnsubaddlem1.e . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝐸 ∈ ℝ+)
7574adantr 468 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑛 ∈ ℕ) → 𝐸 ∈ ℝ+)
76 2nn 11458 . . . . . . . . . . . . . . . . . . . . . . . . 25 2 ∈ ℕ
7776a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 ∈ ℕ → 2 ∈ ℕ)
78 nnnn0 11562 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 ∈ ℕ → 𝑛 ∈ ℕ0)
7977, 78nnexpcld 13249 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 ∈ ℕ → (2↑𝑛) ∈ ℕ)
8079nnrpd 12080 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 ∈ ℕ → (2↑𝑛) ∈ ℝ+)
8180adantl 469 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑛 ∈ ℕ) → (2↑𝑛) ∈ ℝ+)
8275, 81rpdivcld 12099 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑛 ∈ ℕ) → (𝐸 / (2↑𝑛)) ∈ ℝ+)
83 fvex 6418 . . . . . . . . . . . . . . . . . . . . . 22 (𝐶‘(𝐴𝑛)) ∈ V
8483rabex 5004 . . . . . . . . . . . . . . . . . . . . 21 {𝑖 ∈ (𝐶‘(𝐴𝑛)) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛)))} ∈ V
8584a1i 11 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑛 ∈ ℕ) → {𝑖 ∈ (𝐶‘(𝐴𝑛)) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛)))} ∈ V)
8669, 73, 82, 85fvmptd 6506 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑛 ∈ ℕ) → ((𝐷‘(𝐴𝑛))‘(𝐸 / (2↑𝑛))) = {𝑖 ∈ (𝐶‘(𝐴𝑛)) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛)))})
87 ssrab2 3881 . . . . . . . . . . . . . . . . . . . 20 {𝑖 ∈ (𝐶‘(𝐴𝑛)) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛)))} ⊆ (𝐶‘(𝐴𝑛))
8887a1i 11 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑛 ∈ ℕ) → {𝑖 ∈ (𝐶‘(𝐴𝑛)) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛)))} ⊆ (𝐶‘(𝐴𝑛)))
8986, 88eqsstrd 3833 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑛 ∈ ℕ) → ((𝐷‘(𝐴𝑛))‘(𝐸 / (2↑𝑛))) ⊆ (𝐶‘(𝐴𝑛)))
90 ovnsubaddlem1.i . . . . . . . . . . . . . . . . . 18 ((𝜑𝑛 ∈ ℕ) → (𝐼𝑛) ∈ ((𝐷‘(𝐴𝑛))‘(𝐸 / (2↑𝑛))))
9189, 90sseldd 3796 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛 ∈ ℕ) → (𝐼𝑛) ∈ (𝐶‘(𝐴𝑛)))
9254, 91sseldd 3796 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ ℕ) → (𝐼𝑛) ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ))
93 elmapfn 8112 . . . . . . . . . . . . . . . 16 ((𝐼𝑛) ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) → (𝐼𝑛) Fn ℕ)
9492, 93syl 17 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ) → (𝐼𝑛) Fn ℕ)
95 elmapi 8111 . . . . . . . . . . . . . . . . . 18 ((𝐼𝑛) ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) → (𝐼𝑛):ℕ⟶((ℝ × ℝ) ↑𝑚 𝑋))
9692, 95syl 17 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛 ∈ ℕ) → (𝐼𝑛):ℕ⟶((ℝ × ℝ) ↑𝑚 𝑋))
9796ffvelrnda 6578 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → ((𝐼𝑛)‘𝑗) ∈ ((ℝ × ℝ) ↑𝑚 𝑋))
9897ralrimiva 3153 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ) → ∀𝑗 ∈ ℕ ((𝐼𝑛)‘𝑗) ∈ ((ℝ × ℝ) ↑𝑚 𝑋))
9994, 98jca 503 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ ℕ) → ((𝐼𝑛) Fn ℕ ∧ ∀𝑗 ∈ ℕ ((𝐼𝑛)‘𝑗) ∈ ((ℝ × ℝ) ↑𝑚 𝑋)))
100993adant3 1155 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ ℕ ∧ 𝑗 ∈ ℕ) → ((𝐼𝑛) Fn ℕ ∧ ∀𝑗 ∈ ℕ ((𝐼𝑛)‘𝑗) ∈ ((ℝ × ℝ) ↑𝑚 𝑋)))
101 ffnfv 6607 . . . . . . . . . . . . 13 ((𝐼𝑛):ℕ⟶((ℝ × ℝ) ↑𝑚 𝑋) ↔ ((𝐼𝑛) Fn ℕ ∧ ∀𝑗 ∈ ℕ ((𝐼𝑛)‘𝑗) ∈ ((ℝ × ℝ) ↑𝑚 𝑋)))
102100, 101sylibr 225 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ ∧ 𝑗 ∈ ℕ) → (𝐼𝑛):ℕ⟶((ℝ × ℝ) ↑𝑚 𝑋))
103 simp3 1161 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ ℕ)
104102, 103ffvelrnd 6579 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ ∧ 𝑗 ∈ ℕ) → ((𝐼𝑛)‘𝑗) ∈ ((ℝ × ℝ) ↑𝑚 𝑋))
105 elmapi 8111 . . . . . . . . . . 11 (((𝐼𝑛)‘𝑗) ∈ ((ℝ × ℝ) ↑𝑚 𝑋) → ((𝐼𝑛)‘𝑗):𝑋⟶(ℝ × ℝ))
106104, 105syl 17 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ ∧ 𝑗 ∈ ℕ) → ((𝐼𝑛)‘𝑗):𝑋⟶(ℝ × ℝ))
10736, 42, 106vtocl 3451 . . . . . . . . 9 ((𝜑 ∧ (1st ‘(𝐹𝑚)) ∈ ℕ ∧ 𝑗 ∈ ℕ) → ((𝐼‘(1st ‘(𝐹𝑚)))‘𝑗):𝑋⟶(ℝ × ℝ))
10830, 35, 107vtocl 3451 . . . . . . . 8 ((𝜑 ∧ (1st ‘(𝐹𝑚)) ∈ ℕ ∧ (2nd ‘(𝐹𝑚)) ∈ ℕ) → ((𝐼‘(1st ‘(𝐹𝑚)))‘(2nd ‘(𝐹𝑚))):𝑋⟶(ℝ × ℝ))
10917, 27, 29, 108syl3anc 1483 . . . . . . 7 ((𝜑𝑚 ∈ ℕ) → ((𝐼‘(1st ‘(𝐹𝑚)))‘(2nd ‘(𝐹𝑚))):𝑋⟶(ℝ × ℝ))
110 id 22 . . . . . . . . . 10 (𝑚 ∈ ℕ → 𝑚 ∈ ℕ)
111 fvex 6418 . . . . . . . . . . 11 ((𝐼‘(1st ‘(𝐹𝑚)))‘(2nd ‘(𝐹𝑚))) ∈ V
112111a1i 11 . . . . . . . . . 10 (𝑚 ∈ ℕ → ((𝐼‘(1st ‘(𝐹𝑚)))‘(2nd ‘(𝐹𝑚))) ∈ V)
113 ovnsubaddlem1.g . . . . . . . . . . 11 𝐺 = (𝑚 ∈ ℕ ↦ ((𝐼‘(1st ‘(𝐹𝑚)))‘(2nd ‘(𝐹𝑚))))
114113fvmpt2 6509 . . . . . . . . . 10 ((𝑚 ∈ ℕ ∧ ((𝐼‘(1st ‘(𝐹𝑚)))‘(2nd ‘(𝐹𝑚))) ∈ V) → (𝐺𝑚) = ((𝐼‘(1st ‘(𝐹𝑚)))‘(2nd ‘(𝐹𝑚))))
115110, 112, 114syl2anc 575 . . . . . . . . 9 (𝑚 ∈ ℕ → (𝐺𝑚) = ((𝐼‘(1st ‘(𝐹𝑚)))‘(2nd ‘(𝐹𝑚))))
116115adantl 469 . . . . . . . 8 ((𝜑𝑚 ∈ ℕ) → (𝐺𝑚) = ((𝐼‘(1st ‘(𝐹𝑚)))‘(2nd ‘(𝐹𝑚))))
117116feq1d 6238 . . . . . . 7 ((𝜑𝑚 ∈ ℕ) → ((𝐺𝑚):𝑋⟶(ℝ × ℝ) ↔ ((𝐼‘(1st ‘(𝐹𝑚)))‘(2nd ‘(𝐹𝑚))):𝑋⟶(ℝ × ℝ)))
118109, 117mpbird 248 . . . . . 6 ((𝜑𝑚 ∈ ℕ) → (𝐺𝑚):𝑋⟶(ℝ × ℝ))
11916, 18, 19, 118hoiprodcl2 41248 . . . . 5 ((𝜑𝑚 ∈ ℕ) → (𝐿‘(𝐺𝑚)) ∈ (0[,)+∞))
12015, 119sseldi 3793 . . . 4 ((𝜑𝑚 ∈ ℕ) → (𝐿‘(𝐺𝑚)) ∈ (0[,]+∞))
12112, 14, 120sge0xrclmpt 41121 . . 3 (𝜑 → (Σ^‘(𝑚 ∈ ℕ ↦ (𝐿‘(𝐺𝑚)))) ∈ ℝ*)
122 nfv 2008 . . . 4 𝑛𝜑
123 0xr 10368 . . . . . 6 0 ∈ ℝ*
124123a1i 11 . . . . 5 ((𝜑𝑛 ∈ ℕ) → 0 ∈ ℝ*)
125 pnfxr 10374 . . . . . 6 +∞ ∈ ℝ*
126125a1i 11 . . . . 5 ((𝜑𝑛 ∈ ℕ) → +∞ ∈ ℝ*)
1271adantr 468 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → 𝑋 ∈ Fin)
128 ovnsubaddlem1.z . . . . . . . . 9 𝑍 = (𝑎 ∈ 𝒫 (ℝ ↑𝑚 𝑋) ↦ {𝑧 ∈ ℝ* ∣ ∃𝑖 ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)(𝑎 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑖𝑗))‘𝑘) ∧ 𝑧 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘𝑋 (vol‘(([,) ∘ (𝑖𝑗))‘𝑘)))))})
129127, 7, 128ovnval2b 41245 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → ((voln*‘𝑋)‘(𝐴𝑛)) = if(𝑋 = ∅, 0, inf((𝑍‘(𝐴𝑛)), ℝ*, < )))
130 ovnsubaddlem1.n0 . . . . . . . . . . 11 (𝜑𝑋 ≠ ∅)
131130neneqd 2982 . . . . . . . . . 10 (𝜑 → ¬ 𝑋 = ∅)
132131iffalsed 4287 . . . . . . . . 9 (𝜑 → if(𝑋 = ∅, 0, inf((𝑍‘(𝐴𝑛)), ℝ*, < )) = inf((𝑍‘(𝐴𝑛)), ℝ*, < ))
133132adantr 468 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → if(𝑋 = ∅, 0, inf((𝑍‘(𝐴𝑛)), ℝ*, < )) = inf((𝑍‘(𝐴𝑛)), ℝ*, < ))
134129, 133eqtrd 2839 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → ((voln*‘𝑋)‘(𝐴𝑛)) = inf((𝑍‘(𝐴𝑛)), ℝ*, < ))
135128a1i 11 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → 𝑍 = (𝑎 ∈ 𝒫 (ℝ ↑𝑚 𝑋) ↦ {𝑧 ∈ ℝ* ∣ ∃𝑖 ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)(𝑎 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑖𝑗))‘𝑘) ∧ 𝑧 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘𝑋 (vol‘(([,) ∘ (𝑖𝑗))‘𝑘)))))}))
136 sseq1 3820 . . . . . . . . . . . . . 14 (𝑎 = (𝐴𝑛) → (𝑎 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑖𝑗))‘𝑘) ↔ (𝐴𝑛) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑖𝑗))‘𝑘)))
137136anbi1d 617 . . . . . . . . . . . . 13 (𝑎 = (𝐴𝑛) → ((𝑎 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑖𝑗))‘𝑘) ∧ 𝑧 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘𝑋 (vol‘(([,) ∘ (𝑖𝑗))‘𝑘))))) ↔ ((𝐴𝑛) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑖𝑗))‘𝑘) ∧ 𝑧 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘𝑋 (vol‘(([,) ∘ (𝑖𝑗))‘𝑘)))))))
138137rexbidv 3239 . . . . . . . . . . . 12 (𝑎 = (𝐴𝑛) → (∃𝑖 ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)(𝑎 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑖𝑗))‘𝑘) ∧ 𝑧 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘𝑋 (vol‘(([,) ∘ (𝑖𝑗))‘𝑘))))) ↔ ∃𝑖 ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)((𝐴𝑛) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑖𝑗))‘𝑘) ∧ 𝑧 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘𝑋 (vol‘(([,) ∘ (𝑖𝑗))‘𝑘)))))))
139138rabbidv 3378 . . . . . . . . . . 11 (𝑎 = (𝐴𝑛) → {𝑧 ∈ ℝ* ∣ ∃𝑖 ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)(𝑎 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑖𝑗))‘𝑘) ∧ 𝑧 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘𝑋 (vol‘(([,) ∘ (𝑖𝑗))‘𝑘)))))} = {𝑧 ∈ ℝ* ∣ ∃𝑖 ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)((𝐴𝑛) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑖𝑗))‘𝑘) ∧ 𝑧 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘𝑋 (vol‘(([,) ∘ (𝑖𝑗))‘𝑘)))))})
140139adantl 469 . . . . . . . . . 10 (((𝜑𝑛 ∈ ℕ) ∧ 𝑎 = (𝐴𝑛)) → {𝑧 ∈ ℝ* ∣ ∃𝑖 ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)(𝑎 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑖𝑗))‘𝑘) ∧ 𝑧 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘𝑋 (vol‘(([,) ∘ (𝑖𝑗))‘𝑘)))))} = {𝑧 ∈ ℝ* ∣ ∃𝑖 ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)((𝐴𝑛) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑖𝑗))‘𝑘) ∧ 𝑧 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘𝑋 (vol‘(([,) ∘ (𝑖𝑗))‘𝑘)))))})
141 xrex 12039 . . . . . . . . . . . 12 * ∈ V
142141rabex 5004 . . . . . . . . . . 11 {𝑧 ∈ ℝ* ∣ ∃𝑖 ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)((𝐴𝑛) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑖𝑗))‘𝑘) ∧ 𝑧 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘𝑋 (vol‘(([,) ∘ (𝑖𝑗))‘𝑘)))))} ∈ V
143142a1i 11 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → {𝑧 ∈ ℝ* ∣ ∃𝑖 ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)((𝐴𝑛) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑖𝑗))‘𝑘) ∧ 𝑧 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘𝑋 (vol‘(([,) ∘ (𝑖𝑗))‘𝑘)))))} ∈ V)
144135, 140, 5, 143fvmptd 6506 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → (𝑍‘(𝐴𝑛)) = {𝑧 ∈ ℝ* ∣ ∃𝑖 ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)((𝐴𝑛) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑖𝑗))‘𝑘) ∧ 𝑧 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘𝑋 (vol‘(([,) ∘ (𝑖𝑗))‘𝑘)))))})
145 ssrab2 3881 . . . . . . . . . 10 {𝑧 ∈ ℝ* ∣ ∃𝑖 ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)((𝐴𝑛) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑖𝑗))‘𝑘) ∧ 𝑧 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘𝑋 (vol‘(([,) ∘ (𝑖𝑗))‘𝑘)))))} ⊆ ℝ*
146145a1i 11 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → {𝑧 ∈ ℝ* ∣ ∃𝑖 ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)((𝐴𝑛) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑖𝑗))‘𝑘) ∧ 𝑧 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘𝑋 (vol‘(([,) ∘ (𝑖𝑗))‘𝑘)))))} ⊆ ℝ*)
147144, 146eqsstrd 3833 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → (𝑍‘(𝐴𝑛)) ⊆ ℝ*)
148 infxrcl 12377 . . . . . . . 8 ((𝑍‘(𝐴𝑛)) ⊆ ℝ* → inf((𝑍‘(𝐴𝑛)), ℝ*, < ) ∈ ℝ*)
149147, 148syl 17 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → inf((𝑍‘(𝐴𝑛)), ℝ*, < ) ∈ ℝ*)
150134, 149eqeltrd 2884 . . . . . 6 ((𝜑𝑛 ∈ ℕ) → ((voln*‘𝑋)‘(𝐴𝑛)) ∈ ℝ*)
15174rpred 12082 . . . . . . . . 9 (𝜑𝐸 ∈ ℝ)
152151adantr 468 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → 𝐸 ∈ ℝ)
153 2re 11370 . . . . . . . . . . 11 2 ∈ ℝ
154153a1i 11 . . . . . . . . . 10 (𝑛 ∈ ℕ → 2 ∈ ℝ)
155154, 78reexpcld 13244 . . . . . . . . 9 (𝑛 ∈ ℕ → (2↑𝑛) ∈ ℝ)
156155adantl 469 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → (2↑𝑛) ∈ ℝ)
157154recnd 10350 . . . . . . . . . 10 (𝑛 ∈ ℕ → 2 ∈ ℂ)
158 2ne0 11392 . . . . . . . . . . 11 2 ≠ 0
159158a1i 11 . . . . . . . . . 10 (𝑛 ∈ ℕ → 2 ≠ 0)
160 nnz 11661 . . . . . . . . . 10 (𝑛 ∈ ℕ → 𝑛 ∈ ℤ)
161157, 159, 160expne0d 13233 . . . . . . . . 9 (𝑛 ∈ ℕ → (2↑𝑛) ≠ 0)
162161adantl 469 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → (2↑𝑛) ≠ 0)
163152, 156, 162redivcld 11135 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → (𝐸 / (2↑𝑛)) ∈ ℝ)
164163rexrd 10371 . . . . . 6 ((𝜑𝑛 ∈ ℕ) → (𝐸 / (2↑𝑛)) ∈ ℝ*)
165150, 164xaddcld 12345 . . . . 5 ((𝜑𝑛 ∈ ℕ) → (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛))) ∈ ℝ*)
166127, 7ovncl 41260 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → ((voln*‘𝑋)‘(𝐴𝑛)) ∈ (0[,]+∞))
167 xrge0ge0 40040 . . . . . . 7 (((voln*‘𝑋)‘(𝐴𝑛)) ∈ (0[,]+∞) → 0 ≤ ((voln*‘𝑋)‘(𝐴𝑛)))
168166, 167syl 17 . . . . . 6 ((𝜑𝑛 ∈ ℕ) → 0 ≤ ((voln*‘𝑋)‘(𝐴𝑛)))
169 0red 10325 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → 0 ∈ ℝ)
17082rpgt0d 12085 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → 0 < (𝐸 / (2↑𝑛)))
171169, 163, 170ltled 10467 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → 0 ≤ (𝐸 / (2↑𝑛)))
172163ltpnfd 12167 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → (𝐸 / (2↑𝑛)) < +∞)
173164, 126, 172xrltled 12195 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → (𝐸 / (2↑𝑛)) ≤ +∞)
174124, 126, 164, 171, 173eliccxrd 40231 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → (𝐸 / (2↑𝑛)) ∈ (0[,]+∞))
175150, 174xadd0ge 40013 . . . . . 6 ((𝜑𝑛 ∈ ℕ) → ((voln*‘𝑋)‘(𝐴𝑛)) ≤ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛))))
176124, 150, 165, 168, 175xrletrd 12207 . . . . 5 ((𝜑𝑛 ∈ ℕ) → 0 ≤ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛))))
177 pnfge 12176 . . . . . 6 ((((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛))) ∈ ℝ* → (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛))) ≤ +∞)
178165, 177syl 17 . . . . 5 ((𝜑𝑛 ∈ ℕ) → (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛))) ≤ +∞)
179124, 126, 165, 176, 178eliccxrd 40231 . . . 4 ((𝜑𝑛 ∈ ℕ) → (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛))) ∈ (0[,]+∞))
180122, 14, 179sge0xrclmpt 41121 . . 3 (𝜑 → (Σ^‘(𝑛 ∈ ℕ ↦ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛))))) ∈ ℝ*)
18143a1i 11 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ ℕ) → 𝐶 = (𝑎 ∈ 𝒫 (ℝ ↑𝑚 𝑋) ↦ { ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∣ 𝑎 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘)}))
182 sseq1 3820 . . . . . . . . . . . . . 14 (𝑎 = (𝐴‘(1st ‘(𝐹𝑚))) → (𝑎 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘) ↔ (𝐴‘(1st ‘(𝐹𝑚))) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘)))
183182rabbidv 3378 . . . . . . . . . . . . 13 (𝑎 = (𝐴‘(1st ‘(𝐹𝑚))) → { ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∣ 𝑎 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘)} = { ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∣ (𝐴‘(1st ‘(𝐹𝑚))) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘)})
184183adantl 469 . . . . . . . . . . . 12 (((𝜑𝑚 ∈ ℕ) ∧ 𝑎 = (𝐴‘(1st ‘(𝐹𝑚)))) → { ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∣ 𝑎 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘)} = { ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∣ (𝐴‘(1st ‘(𝐹𝑚))) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘)})
1852adantr 468 . . . . . . . . . . . . 13 ((𝜑𝑚 ∈ ℕ) → 𝐴:ℕ⟶𝒫 (ℝ ↑𝑚 𝑋))
186185, 27ffvelrnd 6579 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ ℕ) → (𝐴‘(1st ‘(𝐹𝑚))) ∈ 𝒫 (ℝ ↑𝑚 𝑋))
18748rabex 5004 . . . . . . . . . . . . 13 { ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∣ (𝐴‘(1st ‘(𝐹𝑚))) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘)} ∈ V
188187a1i 11 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ ℕ) → { ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∣ (𝐴‘(1st ‘(𝐹𝑚))) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘)} ∈ V)
189181, 184, 186, 188fvmptd 6506 . . . . . . . . . . 11 ((𝜑𝑚 ∈ ℕ) → (𝐶‘(𝐴‘(1st ‘(𝐹𝑚)))) = { ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∣ (𝐴‘(1st ‘(𝐹𝑚))) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘)})
190 ssrab2 3881 . . . . . . . . . . . 12 { ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∣ (𝐴‘(1st ‘(𝐹𝑚))) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘)} ⊆ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)
191190a1i 11 . . . . . . . . . . 11 ((𝜑𝑚 ∈ ℕ) → { ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∣ (𝐴‘(1st ‘(𝐹𝑚))) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘)} ⊆ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ))
192189, 191eqsstrd 3833 . . . . . . . . . 10 ((𝜑𝑚 ∈ ℕ) → (𝐶‘(𝐴‘(1st ‘(𝐹𝑚)))) ⊆ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ))
19355a1i 11 . . . . . . . . . . . . . 14 ((𝜑𝑚 ∈ ℕ) → 𝐷 = (𝑎 ∈ 𝒫 (ℝ ↑𝑚 𝑋) ↦ (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶𝑎) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘𝑎) +𝑒 𝑒)})))
194 fveq2 6405 . . . . . . . . . . . . . . . . . . 19 (𝑎 = (𝐴‘(1st ‘(𝐹𝑚))) → (𝐶𝑎) = (𝐶‘(𝐴‘(1st ‘(𝐹𝑚)))))
195194eleq2d 2870 . . . . . . . . . . . . . . . . . 18 (𝑎 = (𝐴‘(1st ‘(𝐹𝑚))) → (𝑖 ∈ (𝐶𝑎) ↔ 𝑖 ∈ (𝐶‘(𝐴‘(1st ‘(𝐹𝑚))))))
196 fveq2 6405 . . . . . . . . . . . . . . . . . . . 20 (𝑎 = (𝐴‘(1st ‘(𝐹𝑚))) → ((voln*‘𝑋)‘𝑎) = ((voln*‘𝑋)‘(𝐴‘(1st ‘(𝐹𝑚)))))
197196oveq1d 6886 . . . . . . . . . . . . . . . . . . 19 (𝑎 = (𝐴‘(1st ‘(𝐹𝑚))) → (((voln*‘𝑋)‘𝑎) +𝑒 𝑒) = (((voln*‘𝑋)‘(𝐴‘(1st ‘(𝐹𝑚)))) +𝑒 𝑒))
198197breq2d 4852 . . . . . . . . . . . . . . . . . 18 (𝑎 = (𝐴‘(1st ‘(𝐹𝑚))) → ((Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘𝑎) +𝑒 𝑒) ↔ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴‘(1st ‘(𝐹𝑚)))) +𝑒 𝑒)))
199195, 198anbi12d 618 . . . . . . . . . . . . . . . . 17 (𝑎 = (𝐴‘(1st ‘(𝐹𝑚))) → ((𝑖 ∈ (𝐶𝑎) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘𝑎) +𝑒 𝑒)) ↔ (𝑖 ∈ (𝐶‘(𝐴‘(1st ‘(𝐹𝑚)))) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴‘(1st ‘(𝐹𝑚)))) +𝑒 𝑒))))
200199rabbidva2 3375 . . . . . . . . . . . . . . . 16 (𝑎 = (𝐴‘(1st ‘(𝐹𝑚))) → {𝑖 ∈ (𝐶𝑎) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘𝑎) +𝑒 𝑒)} = {𝑖 ∈ (𝐶‘(𝐴‘(1st ‘(𝐹𝑚)))) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴‘(1st ‘(𝐹𝑚)))) +𝑒 𝑒)})
201200mpteq2dv 4935 . . . . . . . . . . . . . . 15 (𝑎 = (𝐴‘(1st ‘(𝐹𝑚))) → (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶𝑎) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘𝑎) +𝑒 𝑒)}) = (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶‘(𝐴‘(1st ‘(𝐹𝑚)))) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴‘(1st ‘(𝐹𝑚)))) +𝑒 𝑒)}))
202201adantl 469 . . . . . . . . . . . . . 14 (((𝜑𝑚 ∈ ℕ) ∧ 𝑎 = (𝐴‘(1st ‘(𝐹𝑚)))) → (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶𝑎) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘𝑎) +𝑒 𝑒)}) = (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶‘(𝐴‘(1st ‘(𝐹𝑚)))) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴‘(1st ‘(𝐹𝑚)))) +𝑒 𝑒)}))
20366mptex 6708 . . . . . . . . . . . . . . 15 (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶‘(𝐴‘(1st ‘(𝐹𝑚)))) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴‘(1st ‘(𝐹𝑚)))) +𝑒 𝑒)}) ∈ V
204203a1i 11 . . . . . . . . . . . . . 14 ((𝜑𝑚 ∈ ℕ) → (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶‘(𝐴‘(1st ‘(𝐹𝑚)))) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴‘(1st ‘(𝐹𝑚)))) +𝑒 𝑒)}) ∈ V)
205193, 202, 186, 204fvmptd 6506 . . . . . . . . . . . . 13 ((𝜑𝑚 ∈ ℕ) → (𝐷‘(𝐴‘(1st ‘(𝐹𝑚)))) = (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶‘(𝐴‘(1st ‘(𝐹𝑚)))) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴‘(1st ‘(𝐹𝑚)))) +𝑒 𝑒)}))
206 oveq2 6879 . . . . . . . . . . . . . . . 16 (𝑒 = (𝐸 / (2↑(1st ‘(𝐹𝑚)))) → (((voln*‘𝑋)‘(𝐴‘(1st ‘(𝐹𝑚)))) +𝑒 𝑒) = (((voln*‘𝑋)‘(𝐴‘(1st ‘(𝐹𝑚)))) +𝑒 (𝐸 / (2↑(1st ‘(𝐹𝑚))))))
207206breq2d 4852 . . . . . . . . . . . . . . 15 (𝑒 = (𝐸 / (2↑(1st ‘(𝐹𝑚)))) → ((Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴‘(1st ‘(𝐹𝑚)))) +𝑒 𝑒) ↔ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴‘(1st ‘(𝐹𝑚)))) +𝑒 (𝐸 / (2↑(1st ‘(𝐹𝑚)))))))
208207rabbidv 3378 . . . . . . . . . . . . . 14 (𝑒 = (𝐸 / (2↑(1st ‘(𝐹𝑚)))) → {𝑖 ∈ (𝐶‘(𝐴‘(1st ‘(𝐹𝑚)))) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴‘(1st ‘(𝐹𝑚)))) +𝑒 𝑒)} = {𝑖 ∈ (𝐶‘(𝐴‘(1st ‘(𝐹𝑚)))) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴‘(1st ‘(𝐹𝑚)))) +𝑒 (𝐸 / (2↑(1st ‘(𝐹𝑚)))))})
209208adantl 469 . . . . . . . . . . . . 13 (((𝜑𝑚 ∈ ℕ) ∧ 𝑒 = (𝐸 / (2↑(1st ‘(𝐹𝑚))))) → {𝑖 ∈ (𝐶‘(𝐴‘(1st ‘(𝐹𝑚)))) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴‘(1st ‘(𝐹𝑚)))) +𝑒 𝑒)} = {𝑖 ∈ (𝐶‘(𝐴‘(1st ‘(𝐹𝑚)))) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴‘(1st ‘(𝐹𝑚)))) +𝑒 (𝐸 / (2↑(1st ‘(𝐹𝑚)))))})
21017, 74syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑚 ∈ ℕ) → 𝐸 ∈ ℝ+)
211 2rp 12047 . . . . . . . . . . . . . . . 16 2 ∈ ℝ+
212211a1i 11 . . . . . . . . . . . . . . 15 ((𝜑𝑚 ∈ ℕ) → 2 ∈ ℝ+)
21327nnzd 11743 . . . . . . . . . . . . . . 15 ((𝜑𝑚 ∈ ℕ) → (1st ‘(𝐹𝑚)) ∈ ℤ)
214212, 213rpexpcld 13251 . . . . . . . . . . . . . 14 ((𝜑𝑚 ∈ ℕ) → (2↑(1st ‘(𝐹𝑚))) ∈ ℝ+)
215210, 214rpdivcld 12099 . . . . . . . . . . . . 13 ((𝜑𝑚 ∈ ℕ) → (𝐸 / (2↑(1st ‘(𝐹𝑚)))) ∈ ℝ+)
216 fvex 6418 . . . . . . . . . . . . . . 15 (𝐶‘(𝐴‘(1st ‘(𝐹𝑚)))) ∈ V
217216rabex 5004 . . . . . . . . . . . . . 14 {𝑖 ∈ (𝐶‘(𝐴‘(1st ‘(𝐹𝑚)))) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴‘(1st ‘(𝐹𝑚)))) +𝑒 (𝐸 / (2↑(1st ‘(𝐹𝑚)))))} ∈ V
218217a1i 11 . . . . . . . . . . . . 13 ((𝜑𝑚 ∈ ℕ) → {𝑖 ∈ (𝐶‘(𝐴‘(1st ‘(𝐹𝑚)))) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴‘(1st ‘(𝐹𝑚)))) +𝑒 (𝐸 / (2↑(1st ‘(𝐹𝑚)))))} ∈ V)
219205, 209, 215, 218fvmptd 6506 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ ℕ) → ((𝐷‘(𝐴‘(1st ‘(𝐹𝑚))))‘(𝐸 / (2↑(1st ‘(𝐹𝑚))))) = {𝑖 ∈ (𝐶‘(𝐴‘(1st ‘(𝐹𝑚)))) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴‘(1st ‘(𝐹𝑚)))) +𝑒 (𝐸 / (2↑(1st ‘(𝐹𝑚)))))})
220 ssrab2 3881 . . . . . . . . . . . . 13 {𝑖 ∈ (𝐶‘(𝐴‘(1st ‘(𝐹𝑚)))) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴‘(1st ‘(𝐹𝑚)))) +𝑒 (𝐸 / (2↑(1st ‘(𝐹𝑚)))))} ⊆ (𝐶‘(𝐴‘(1st ‘(𝐹𝑚))))
221220a1i 11 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ ℕ) → {𝑖 ∈ (𝐶‘(𝐴‘(1st ‘(𝐹𝑚)))) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴‘(1st ‘(𝐹𝑚)))) +𝑒 (𝐸 / (2↑(1st ‘(𝐹𝑚)))))} ⊆ (𝐶‘(𝐴‘(1st ‘(𝐹𝑚)))))
222219, 221eqsstrd 3833 . . . . . . . . . . 11 ((𝜑𝑚 ∈ ℕ) → ((𝐷‘(𝐴‘(1st ‘(𝐹𝑚))))‘(𝐸 / (2↑(1st ‘(𝐹𝑚))))) ⊆ (𝐶‘(𝐴‘(1st ‘(𝐹𝑚)))))
22337anbi2d 616 . . . . . . . . . . . . . 14 (𝑛 = (1st ‘(𝐹𝑚)) → ((𝜑𝑛 ∈ ℕ) ↔ (𝜑 ∧ (1st ‘(𝐹𝑚)) ∈ ℕ)))
224 2fveq3 6410 . . . . . . . . . . . . . . . 16 (𝑛 = (1st ‘(𝐹𝑚)) → (𝐷‘(𝐴𝑛)) = (𝐷‘(𝐴‘(1st ‘(𝐹𝑚)))))
225 oveq2 6879 . . . . . . . . . . . . . . . . 17 (𝑛 = (1st ‘(𝐹𝑚)) → (2↑𝑛) = (2↑(1st ‘(𝐹𝑚))))
226225oveq2d 6887 . . . . . . . . . . . . . . . 16 (𝑛 = (1st ‘(𝐹𝑚)) → (𝐸 / (2↑𝑛)) = (𝐸 / (2↑(1st ‘(𝐹𝑚)))))
227224, 226fveq12d 6412 . . . . . . . . . . . . . . 15 (𝑛 = (1st ‘(𝐹𝑚)) → ((𝐷‘(𝐴𝑛))‘(𝐸 / (2↑𝑛))) = ((𝐷‘(𝐴‘(1st ‘(𝐹𝑚))))‘(𝐸 / (2↑(1st ‘(𝐹𝑚))))))
22839, 227eleq12d 2878 . . . . . . . . . . . . . 14 (𝑛 = (1st ‘(𝐹𝑚)) → ((𝐼𝑛) ∈ ((𝐷‘(𝐴𝑛))‘(𝐸 / (2↑𝑛))) ↔ (𝐼‘(1st ‘(𝐹𝑚))) ∈ ((𝐷‘(𝐴‘(1st ‘(𝐹𝑚))))‘(𝐸 / (2↑(1st ‘(𝐹𝑚)))))))
229223, 228imbi12d 335 . . . . . . . . . . . . 13 (𝑛 = (1st ‘(𝐹𝑚)) → (((𝜑𝑛 ∈ ℕ) → (𝐼𝑛) ∈ ((𝐷‘(𝐴𝑛))‘(𝐸 / (2↑𝑛)))) ↔ ((𝜑 ∧ (1st ‘(𝐹𝑚)) ∈ ℕ) → (𝐼‘(1st ‘(𝐹𝑚))) ∈ ((𝐷‘(𝐴‘(1st ‘(𝐹𝑚))))‘(𝐸 / (2↑(1st ‘(𝐹𝑚))))))))
23036, 229, 90vtocl 3451 . . . . . . . . . . . 12 ((𝜑 ∧ (1st ‘(𝐹𝑚)) ∈ ℕ) → (𝐼‘(1st ‘(𝐹𝑚))) ∈ ((𝐷‘(𝐴‘(1st ‘(𝐹𝑚))))‘(𝐸 / (2↑(1st ‘(𝐹𝑚))))))
23117, 27, 230syl2anc 575 . . . . . . . . . . 11 ((𝜑𝑚 ∈ ℕ) → (𝐼‘(1st ‘(𝐹𝑚))) ∈ ((𝐷‘(𝐴‘(1st ‘(𝐹𝑚))))‘(𝐸 / (2↑(1st ‘(𝐹𝑚))))))
232222, 231sseldd 3796 . . . . . . . . . 10 ((𝜑𝑚 ∈ ℕ) → (𝐼‘(1st ‘(𝐹𝑚))) ∈ (𝐶‘(𝐴‘(1st ‘(𝐹𝑚)))))
233192, 232sseldd 3796 . . . . . . . . 9 ((𝜑𝑚 ∈ ℕ) → (𝐼‘(1st ‘(𝐹𝑚))) ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ))
234 elmapfn 8112 . . . . . . . . 9 ((𝐼‘(1st ‘(𝐹𝑚))) ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) → (𝐼‘(1st ‘(𝐹𝑚))) Fn ℕ)
235233, 234syl 17 . . . . . . . 8 ((𝜑𝑚 ∈ ℕ) → (𝐼‘(1st ‘(𝐹𝑚))) Fn ℕ)
236 elmapi 8111 . . . . . . . . . . 11 ((𝐼‘(1st ‘(𝐹𝑚))) ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) → (𝐼‘(1st ‘(𝐹𝑚))):ℕ⟶((ℝ × ℝ) ↑𝑚 𝑋))
237233, 236syl 17 . . . . . . . . . 10 ((𝜑𝑚 ∈ ℕ) → (𝐼‘(1st ‘(𝐹𝑚))):ℕ⟶((ℝ × ℝ) ↑𝑚 𝑋))
238237ffvelrnda 6578 . . . . . . . . 9 (((𝜑𝑚 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → ((𝐼‘(1st ‘(𝐹𝑚)))‘𝑗) ∈ ((ℝ × ℝ) ↑𝑚 𝑋))
239238ralrimiva 3153 . . . . . . . 8 ((𝜑𝑚 ∈ ℕ) → ∀𝑗 ∈ ℕ ((𝐼‘(1st ‘(𝐹𝑚)))‘𝑗) ∈ ((ℝ × ℝ) ↑𝑚 𝑋))
240235, 239jca 503 . . . . . . 7 ((𝜑𝑚 ∈ ℕ) → ((𝐼‘(1st ‘(𝐹𝑚))) Fn ℕ ∧ ∀𝑗 ∈ ℕ ((𝐼‘(1st ‘(𝐹𝑚)))‘𝑗) ∈ ((ℝ × ℝ) ↑𝑚 𝑋)))
241 ffnfv 6607 . . . . . . 7 ((𝐼‘(1st ‘(𝐹𝑚))):ℕ⟶((ℝ × ℝ) ↑𝑚 𝑋) ↔ ((𝐼‘(1st ‘(𝐹𝑚))) Fn ℕ ∧ ∀𝑗 ∈ ℕ ((𝐼‘(1st ‘(𝐹𝑚)))‘𝑗) ∈ ((ℝ × ℝ) ↑𝑚 𝑋)))
242240, 241sylibr 225 . . . . . 6 ((𝜑𝑚 ∈ ℕ) → (𝐼‘(1st ‘(𝐹𝑚))):ℕ⟶((ℝ × ℝ) ↑𝑚 𝑋))
243242, 29ffvelrnd 6579 . . . . 5 ((𝜑𝑚 ∈ ℕ) → ((𝐼‘(1st ‘(𝐹𝑚)))‘(2nd ‘(𝐹𝑚))) ∈ ((ℝ × ℝ) ↑𝑚 𝑋))
244243, 113fmptd 6603 . . . 4 (𝜑𝐺:ℕ⟶((ℝ × ℝ) ↑𝑚 𝑋))
245 simpl 470 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → 𝜑)
24690, 86eleqtrd 2886 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → (𝐼𝑛) ∈ {𝑖 ∈ (𝐶‘(𝐴𝑛)) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛)))})
24787, 246sseldi 3793 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → (𝐼𝑛) ∈ (𝐶‘(𝐴𝑛)))
248 simp3 1161 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ ∧ (𝐼𝑛) ∈ (𝐶‘(𝐴𝑛))) → (𝐼𝑛) ∈ (𝐶‘(𝐴𝑛)))
249513adant3 1155 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ ∧ (𝐼𝑛) ∈ (𝐶‘(𝐴𝑛))) → (𝐶‘(𝐴𝑛)) = { ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∣ (𝐴𝑛) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘)})
250248, 249eleqtrd 2886 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ ∧ (𝐼𝑛) ∈ (𝐶‘(𝐴𝑛))) → (𝐼𝑛) ∈ { ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∣ (𝐴𝑛) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘)})
251 fveq1 6404 . . . . . . . . . . . . . . . . 17 ( = (𝐼𝑛) → (𝑗) = ((𝐼𝑛)‘𝑗))
252251coeq2d 5483 . . . . . . . . . . . . . . . 16 ( = (𝐼𝑛) → ([,) ∘ (𝑗)) = ([,) ∘ ((𝐼𝑛)‘𝑗)))
253252fveq1d 6407 . . . . . . . . . . . . . . 15 ( = (𝐼𝑛) → (([,) ∘ (𝑗))‘𝑘) = (([,) ∘ ((𝐼𝑛)‘𝑗))‘𝑘))
254253ixpeq2dv 8158 . . . . . . . . . . . . . 14 ( = (𝐼𝑛) → X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘) = X𝑘𝑋 (([,) ∘ ((𝐼𝑛)‘𝑗))‘𝑘))
255254iuneq2d 4735 . . . . . . . . . . . . 13 ( = (𝐼𝑛) → 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘) = 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ ((𝐼𝑛)‘𝑗))‘𝑘))
256255sseq2d 3827 . . . . . . . . . . . 12 ( = (𝐼𝑛) → ((𝐴𝑛) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘) ↔ (𝐴𝑛) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ ((𝐼𝑛)‘𝑗))‘𝑘)))
257256elrab 3558 . . . . . . . . . . 11 ((𝐼𝑛) ∈ { ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∣ (𝐴𝑛) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘)} ↔ ((𝐼𝑛) ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∧ (𝐴𝑛) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ ((𝐼𝑛)‘𝑗))‘𝑘)))
258250, 257sylib 209 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ ∧ (𝐼𝑛) ∈ (𝐶‘(𝐴𝑛))) → ((𝐼𝑛) ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∧ (𝐴𝑛) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ ((𝐼𝑛)‘𝑗))‘𝑘)))
259258simprd 485 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ ∧ (𝐼𝑛) ∈ (𝐶‘(𝐴𝑛))) → (𝐴𝑛) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ ((𝐼𝑛)‘𝑗))‘𝑘))
260245, 4, 247, 259syl3anc 1483 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → (𝐴𝑛) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ ((𝐼𝑛)‘𝑗))‘𝑘))
261 f1ofo 6357 . . . . . . . . . . . . . 14 (𝐹:ℕ–1-1-onto→(ℕ × ℕ) → 𝐹:ℕ–onto→(ℕ × ℕ))
26220, 261syl 17 . . . . . . . . . . . . 13 (𝜑𝐹:ℕ–onto→(ℕ × ℕ))
263262ad2antrr 708 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → 𝐹:ℕ–onto→(ℕ × ℕ))
264 opelxpi 5345 . . . . . . . . . . . . 13 ((𝑛 ∈ ℕ ∧ 𝑗 ∈ ℕ) → ⟨𝑛, 𝑗⟩ ∈ (ℕ × ℕ))
2654, 264sylan 571 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → ⟨𝑛, 𝑗⟩ ∈ (ℕ × ℕ))
266 foelrni 6462 . . . . . . . . . . . 12 ((𝐹:ℕ–onto→(ℕ × ℕ) ∧ ⟨𝑛, 𝑗⟩ ∈ (ℕ × ℕ)) → ∃𝑚 ∈ ℕ (𝐹𝑚) = ⟨𝑛, 𝑗⟩)
267263, 265, 266syl2anc 575 . . . . . . . . . . 11 (((𝜑𝑛 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → ∃𝑚 ∈ ℕ (𝐹𝑚) = ⟨𝑛, 𝑗⟩)
268 nfv 2008 . . . . . . . . . . . 12 𝑚((𝜑𝑛 ∈ ℕ) ∧ 𝑗 ∈ ℕ)
269 nfre1 3191 . . . . . . . . . . . 12 𝑚𝑚 ∈ {𝑖 ∈ ℕ ∣ (1st ‘(𝐹𝑖)) = 𝑛}X𝑘𝑋 (([,) ∘ ((𝐼𝑛)‘𝑗))‘𝑘) ⊆ X𝑘𝑋 (([,) ∘ (𝐺𝑚))‘𝑘)
270 simpl 470 . . . . . . . . . . . . . . . . 17 ((𝑚 ∈ ℕ ∧ (𝐹𝑚) = ⟨𝑛, 𝑗⟩) → 𝑚 ∈ ℕ)
271 fveq2 6405 . . . . . . . . . . . . . . . . . . 19 ((𝐹𝑚) = ⟨𝑛, 𝑗⟩ → (1st ‘(𝐹𝑚)) = (1st ‘⟨𝑛, 𝑗⟩))
272 vex 3393 . . . . . . . . . . . . . . . . . . . . 21 𝑛 ∈ V
273 vex 3393 . . . . . . . . . . . . . . . . . . . . 21 𝑗 ∈ V
274 op1stg 7407 . . . . . . . . . . . . . . . . . . . . 21 ((𝑛 ∈ V ∧ 𝑗 ∈ V) → (1st ‘⟨𝑛, 𝑗⟩) = 𝑛)
275272, 273, 274mp2an 675 . . . . . . . . . . . . . . . . . . . 20 (1st ‘⟨𝑛, 𝑗⟩) = 𝑛
276275a1i 11 . . . . . . . . . . . . . . . . . . 19 ((𝐹𝑚) = ⟨𝑛, 𝑗⟩ → (1st ‘⟨𝑛, 𝑗⟩) = 𝑛)
277271, 276eqtrd 2839 . . . . . . . . . . . . . . . . . 18 ((𝐹𝑚) = ⟨𝑛, 𝑗⟩ → (1st ‘(𝐹𝑚)) = 𝑛)
278277adantl 469 . . . . . . . . . . . . . . . . 17 ((𝑚 ∈ ℕ ∧ (𝐹𝑚) = ⟨𝑛, 𝑗⟩) → (1st ‘(𝐹𝑚)) = 𝑛)
279270, 278jca 503 . . . . . . . . . . . . . . . 16 ((𝑚 ∈ ℕ ∧ (𝐹𝑚) = ⟨𝑛, 𝑗⟩) → (𝑚 ∈ ℕ ∧ (1st ‘(𝐹𝑚)) = 𝑛))
280 2fveq3 6410 . . . . . . . . . . . . . . . . . 18 (𝑖 = 𝑚 → (1st ‘(𝐹𝑖)) = (1st ‘(𝐹𝑚)))
281280eqeq1d 2807 . . . . . . . . . . . . . . . . 17 (𝑖 = 𝑚 → ((1st ‘(𝐹𝑖)) = 𝑛 ↔ (1st ‘(𝐹𝑚)) = 𝑛))
282281elrab 3558 . . . . . . . . . . . . . . . 16 (𝑚 ∈ {𝑖 ∈ ℕ ∣ (1st ‘(𝐹𝑖)) = 𝑛} ↔ (𝑚 ∈ ℕ ∧ (1st ‘(𝐹𝑚)) = 𝑛))
283279, 282sylibr 225 . . . . . . . . . . . . . . 15 ((𝑚 ∈ ℕ ∧ (𝐹𝑚) = ⟨𝑛, 𝑗⟩) → 𝑚 ∈ {𝑖 ∈ ℕ ∣ (1st ‘(𝐹𝑖)) = 𝑛})
2842833adant1 1153 . . . . . . . . . . . . . 14 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑗 ∈ ℕ) ∧ 𝑚 ∈ ℕ ∧ (𝐹𝑚) = ⟨𝑛, 𝑗⟩) → 𝑚 ∈ {𝑖 ∈ ℕ ∣ (1st ‘(𝐹𝑖)) = 𝑛})
285270, 115syl 17 . . . . . . . . . . . . . . . . . . . 20 ((𝑚 ∈ ℕ ∧ (𝐹𝑚) = ⟨𝑛, 𝑗⟩) → (𝐺𝑚) = ((𝐼‘(1st ‘(𝐹𝑚)))‘(2nd ‘(𝐹𝑚))))
286277fveq2d 6409 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐹𝑚) = ⟨𝑛, 𝑗⟩ → (𝐼‘(1st ‘(𝐹𝑚))) = (𝐼𝑛))
287272, 273op2ndd 7406 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐹𝑚) = ⟨𝑛, 𝑗⟩ → (2nd ‘(𝐹𝑚)) = 𝑗)
288286, 287fveq12d 6412 . . . . . . . . . . . . . . . . . . . . 21 ((𝐹𝑚) = ⟨𝑛, 𝑗⟩ → ((𝐼‘(1st ‘(𝐹𝑚)))‘(2nd ‘(𝐹𝑚))) = ((𝐼𝑛)‘𝑗))
289288adantl 469 . . . . . . . . . . . . . . . . . . . 20 ((𝑚 ∈ ℕ ∧ (𝐹𝑚) = ⟨𝑛, 𝑗⟩) → ((𝐼‘(1st ‘(𝐹𝑚)))‘(2nd ‘(𝐹𝑚))) = ((𝐼𝑛)‘𝑗))
290285, 289eqtr2d 2840 . . . . . . . . . . . . . . . . . . 19 ((𝑚 ∈ ℕ ∧ (𝐹𝑚) = ⟨𝑛, 𝑗⟩) → ((𝐼𝑛)‘𝑗) = (𝐺𝑚))
291290coeq2d 5483 . . . . . . . . . . . . . . . . . 18 ((𝑚 ∈ ℕ ∧ (𝐹𝑚) = ⟨𝑛, 𝑗⟩) → ([,) ∘ ((𝐼𝑛)‘𝑗)) = ([,) ∘ (𝐺𝑚)))
292291fveq1d 6407 . . . . . . . . . . . . . . . . 17 ((𝑚 ∈ ℕ ∧ (𝐹𝑚) = ⟨𝑛, 𝑗⟩) → (([,) ∘ ((𝐼𝑛)‘𝑗))‘𝑘) = (([,) ∘ (𝐺𝑚))‘𝑘))
293292ixpeq2dv 8158 . . . . . . . . . . . . . . . 16 ((𝑚 ∈ ℕ ∧ (𝐹𝑚) = ⟨𝑛, 𝑗⟩) → X𝑘𝑋 (([,) ∘ ((𝐼𝑛)‘𝑗))‘𝑘) = X𝑘𝑋 (([,) ∘ (𝐺𝑚))‘𝑘))
294 eqimss 3851 . . . . . . . . . . . . . . . 16 (X𝑘𝑋 (([,) ∘ ((𝐼𝑛)‘𝑗))‘𝑘) = X𝑘𝑋 (([,) ∘ (𝐺𝑚))‘𝑘) → X𝑘𝑋 (([,) ∘ ((𝐼𝑛)‘𝑗))‘𝑘) ⊆ X𝑘𝑋 (([,) ∘ (𝐺𝑚))‘𝑘))
295293, 294syl 17 . . . . . . . . . . . . . . 15 ((𝑚 ∈ ℕ ∧ (𝐹𝑚) = ⟨𝑛, 𝑗⟩) → X𝑘𝑋 (([,) ∘ ((𝐼𝑛)‘𝑗))‘𝑘) ⊆ X𝑘𝑋 (([,) ∘ (𝐺𝑚))‘𝑘))
2962953adant1 1153 . . . . . . . . . . . . . 14 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑗 ∈ ℕ) ∧ 𝑚 ∈ ℕ ∧ (𝐹𝑚) = ⟨𝑛, 𝑗⟩) → X𝑘𝑋 (([,) ∘ ((𝐼𝑛)‘𝑗))‘𝑘) ⊆ X𝑘𝑋 (([,) ∘ (𝐺𝑚))‘𝑘))
297 rspe 3189 . . . . . . . . . . . . . 14 ((𝑚 ∈ {𝑖 ∈ ℕ ∣ (1st ‘(𝐹𝑖)) = 𝑛} ∧ X𝑘𝑋 (([,) ∘ ((𝐼𝑛)‘𝑗))‘𝑘) ⊆ X𝑘𝑋 (([,) ∘ (𝐺𝑚))‘𝑘)) → ∃𝑚 ∈ {𝑖 ∈ ℕ ∣ (1st ‘(𝐹𝑖)) = 𝑛}X𝑘𝑋 (([,) ∘ ((𝐼𝑛)‘𝑗))‘𝑘) ⊆ X𝑘𝑋 (([,) ∘ (𝐺𝑚))‘𝑘))
298284, 296, 297syl2anc 575 . . . . . . . . . . . . 13 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑗 ∈ ℕ) ∧ 𝑚 ∈ ℕ ∧ (𝐹𝑚) = ⟨𝑛, 𝑗⟩) → ∃𝑚 ∈ {𝑖 ∈ ℕ ∣ (1st ‘(𝐹𝑖)) = 𝑛}X𝑘𝑋 (([,) ∘ ((𝐼𝑛)‘𝑗))‘𝑘) ⊆ X𝑘𝑋 (([,) ∘ (𝐺𝑚))‘𝑘))
2992983exp 1141 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → (𝑚 ∈ ℕ → ((𝐹𝑚) = ⟨𝑛, 𝑗⟩ → ∃𝑚 ∈ {𝑖 ∈ ℕ ∣ (1st ‘(𝐹𝑖)) = 𝑛}X𝑘𝑋 (([,) ∘ ((𝐼𝑛)‘𝑗))‘𝑘) ⊆ X𝑘𝑋 (([,) ∘ (𝐺𝑚))‘𝑘))))
300268, 269, 299rexlimd 3213 . . . . . . . . . . 11 (((𝜑𝑛 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → (∃𝑚 ∈ ℕ (𝐹𝑚) = ⟨𝑛, 𝑗⟩ → ∃𝑚 ∈ {𝑖 ∈ ℕ ∣ (1st ‘(𝐹𝑖)) = 𝑛}X𝑘𝑋 (([,) ∘ ((𝐼𝑛)‘𝑗))‘𝑘) ⊆ X𝑘𝑋 (([,) ∘ (𝐺𝑚))‘𝑘)))
301267, 300mpd 15 . . . . . . . . . 10 (((𝜑𝑛 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → ∃𝑚 ∈ {𝑖 ∈ ℕ ∣ (1st ‘(𝐹𝑖)) = 𝑛}X𝑘𝑋 (([,) ∘ ((𝐼𝑛)‘𝑗))‘𝑘) ⊆ X𝑘𝑋 (([,) ∘ (𝐺𝑚))‘𝑘))
302301ralrimiva 3153 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → ∀𝑗 ∈ ℕ ∃𝑚 ∈ {𝑖 ∈ ℕ ∣ (1st ‘(𝐹𝑖)) = 𝑛}X𝑘𝑋 (([,) ∘ ((𝐼𝑛)‘𝑗))‘𝑘) ⊆ X𝑘𝑋 (([,) ∘ (𝐺𝑚))‘𝑘))
303 iunss2 4753 . . . . . . . . 9 (∀𝑗 ∈ ℕ ∃𝑚 ∈ {𝑖 ∈ ℕ ∣ (1st ‘(𝐹𝑖)) = 𝑛}X𝑘𝑋 (([,) ∘ ((𝐼𝑛)‘𝑗))‘𝑘) ⊆ X𝑘𝑋 (([,) ∘ (𝐺𝑚))‘𝑘) → 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ ((𝐼𝑛)‘𝑗))‘𝑘) ⊆ 𝑚 ∈ {𝑖 ∈ ℕ ∣ (1st ‘(𝐹𝑖)) = 𝑛}X𝑘𝑋 (([,) ∘ (𝐺𝑚))‘𝑘))
304302, 303syl 17 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ ((𝐼𝑛)‘𝑗))‘𝑘) ⊆ 𝑚 ∈ {𝑖 ∈ ℕ ∣ (1st ‘(𝐹𝑖)) = 𝑛}X𝑘𝑋 (([,) ∘ (𝐺𝑚))‘𝑘))
305260, 304sstrd 3805 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → (𝐴𝑛) ⊆ 𝑚 ∈ {𝑖 ∈ ℕ ∣ (1st ‘(𝐹𝑖)) = 𝑛}X𝑘𝑋 (([,) ∘ (𝐺𝑚))‘𝑘))
306 ssrab2 3881 . . . . . . . . 9 {𝑖 ∈ ℕ ∣ (1st ‘(𝐹𝑖)) = 𝑛} ⊆ ℕ
307 iunss1 4720 . . . . . . . . 9 ({𝑖 ∈ ℕ ∣ (1st ‘(𝐹𝑖)) = 𝑛} ⊆ ℕ → 𝑚 ∈ {𝑖 ∈ ℕ ∣ (1st ‘(𝐹𝑖)) = 𝑛}X𝑘𝑋 (([,) ∘ (𝐺𝑚))‘𝑘) ⊆ 𝑚 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝐺𝑚))‘𝑘))
308306, 307ax-mp 5 . . . . . . . 8 𝑚 ∈ {𝑖 ∈ ℕ ∣ (1st ‘(𝐹𝑖)) = 𝑛}X𝑘𝑋 (([,) ∘ (𝐺𝑚))‘𝑘) ⊆ 𝑚 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝐺𝑚))‘𝑘)
309308a1i 11 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → 𝑚 ∈ {𝑖 ∈ ℕ ∣ (1st ‘(𝐹𝑖)) = 𝑛}X𝑘𝑋 (([,) ∘ (𝐺𝑚))‘𝑘) ⊆ 𝑚 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝐺𝑚))‘𝑘))
310305, 309sstrd 3805 . . . . . 6 ((𝜑𝑛 ∈ ℕ) → (𝐴𝑛) ⊆ 𝑚 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝐺𝑚))‘𝑘))
311310ralrimiva 3153 . . . . 5 (𝜑 → ∀𝑛 ∈ ℕ (𝐴𝑛) ⊆ 𝑚 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝐺𝑚))‘𝑘))
312 iunss 4749 . . . . 5 ( 𝑛 ∈ ℕ (𝐴𝑛) ⊆ 𝑚 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝐺𝑚))‘𝑘) ↔ ∀𝑛 ∈ ℕ (𝐴𝑛) ⊆ 𝑚 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝐺𝑚))‘𝑘))
313311, 312sylibr 225 . . . 4 (𝜑 𝑛 ∈ ℕ (𝐴𝑛) ⊆ 𝑚 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝐺𝑚))‘𝑘))
3141, 130, 19, 244, 313ovnlecvr 41251 . . 3 (𝜑 → ((voln*‘𝑋)‘ 𝑛 ∈ ℕ (𝐴𝑛)) ≤ (Σ^‘(𝑚 ∈ ℕ ↦ (𝐿‘(𝐺𝑚)))))
315116fveq2d 6409 . . . . . . 7 ((𝜑𝑚 ∈ ℕ) → (𝐿‘(𝐺𝑚)) = (𝐿‘((𝐼‘(1st ‘(𝐹𝑚)))‘(2nd ‘(𝐹𝑚)))))
316315mpteq2dva 4934 . . . . . 6 (𝜑 → (𝑚 ∈ ℕ ↦ (𝐿‘(𝐺𝑚))) = (𝑚 ∈ ℕ ↦ (𝐿‘((𝐼‘(1st ‘(𝐹𝑚)))‘(2nd ‘(𝐹𝑚))))))
317316fveq2d 6409 . . . . 5 (𝜑 → (Σ^‘(𝑚 ∈ ℕ ↦ (𝐿‘(𝐺𝑚)))) = (Σ^‘(𝑚 ∈ ℕ ↦ (𝐿‘((𝐼‘(1st ‘(𝐹𝑚)))‘(2nd ‘(𝐹𝑚)))))))
318 nfv 2008 . . . . . 6 𝑝𝜑
319 2fveq3 6410 . . . . . . . 8 (𝑝 = (𝐹𝑚) → (𝐼‘(1st𝑝)) = (𝐼‘(1st ‘(𝐹𝑚))))
320 fveq2 6405 . . . . . . . 8 (𝑝 = (𝐹𝑚) → (2nd𝑝) = (2nd ‘(𝐹𝑚)))
321319, 320fveq12d 6412 . . . . . . 7 (𝑝 = (𝐹𝑚) → ((𝐼‘(1st𝑝))‘(2nd𝑝)) = ((𝐼‘(1st ‘(𝐹𝑚)))‘(2nd ‘(𝐹𝑚))))
322321fveq2d 6409 . . . . . 6 (𝑝 = (𝐹𝑚) → (𝐿‘((𝐼‘(1st𝑝))‘(2nd𝑝))) = (𝐿‘((𝐼‘(1st ‘(𝐹𝑚)))‘(2nd ‘(𝐹𝑚)))))
323 eqidd 2806 . . . . . 6 ((𝜑𝑚 ∈ ℕ) → (𝐹𝑚) = (𝐹𝑚))
324 nfv 2008 . . . . . . . 8 𝑘(𝜑𝑝 ∈ (ℕ × ℕ))
3251adantr 468 . . . . . . . 8 ((𝜑𝑝 ∈ (ℕ × ℕ)) → 𝑋 ∈ Fin)
326 simpl 470 . . . . . . . . 9 ((𝜑𝑝 ∈ (ℕ × ℕ)) → 𝜑)
327 xp1st 7427 . . . . . . . . . 10 (𝑝 ∈ (ℕ × ℕ) → (1st𝑝) ∈ ℕ)
328327adantl 469 . . . . . . . . 9 ((𝜑𝑝 ∈ (ℕ × ℕ)) → (1st𝑝) ∈ ℕ)
329 xp2nd 7428 . . . . . . . . . 10 (𝑝 ∈ (ℕ × ℕ) → (2nd𝑝) ∈ ℕ)
330329adantl 469 . . . . . . . . 9 ((𝜑𝑝 ∈ (ℕ × ℕ)) → (2nd𝑝) ∈ ℕ)
331 fvex 6418 . . . . . . . . . 10 (2nd𝑝) ∈ V
332 eleq1 2872 . . . . . . . . . . . 12 (𝑗 = (2nd𝑝) → (𝑗 ∈ ℕ ↔ (2nd𝑝) ∈ ℕ))
3333323anbi3d 1559 . . . . . . . . . . 11 (𝑗 = (2nd𝑝) → ((𝜑 ∧ (1st𝑝) ∈ ℕ ∧ 𝑗 ∈ ℕ) ↔ (𝜑 ∧ (1st𝑝) ∈ ℕ ∧ (2nd𝑝) ∈ ℕ)))
334 fveq2 6405 . . . . . . . . . . . 12 (𝑗 = (2nd𝑝) → ((𝐼‘(1st𝑝))‘𝑗) = ((𝐼‘(1st𝑝))‘(2nd𝑝)))
335334feq1d 6238 . . . . . . . . . . 11 (𝑗 = (2nd𝑝) → (((𝐼‘(1st𝑝))‘𝑗):𝑋⟶(ℝ × ℝ) ↔ ((𝐼‘(1st𝑝))‘(2nd𝑝)):𝑋⟶(ℝ × ℝ)))
336333, 335imbi12d 335 . . . . . . . . . 10 (𝑗 = (2nd𝑝) → (((𝜑 ∧ (1st𝑝) ∈ ℕ ∧ 𝑗 ∈ ℕ) → ((𝐼‘(1st𝑝))‘𝑗):𝑋⟶(ℝ × ℝ)) ↔ ((𝜑 ∧ (1st𝑝) ∈ ℕ ∧ (2nd𝑝) ∈ ℕ) → ((𝐼‘(1st𝑝))‘(2nd𝑝)):𝑋⟶(ℝ × ℝ))))
337 fvex 6418 . . . . . . . . . . 11 (1st𝑝) ∈ V
338 eleq1 2872 . . . . . . . . . . . . 13 (𝑛 = (1st𝑝) → (𝑛 ∈ ℕ ↔ (1st𝑝) ∈ ℕ))
3393383anbi2d 1558 . . . . . . . . . . . 12 (𝑛 = (1st𝑝) → ((𝜑𝑛 ∈ ℕ ∧ 𝑗 ∈ ℕ) ↔ (𝜑 ∧ (1st𝑝) ∈ ℕ ∧ 𝑗 ∈ ℕ)))
340 fveq2 6405 . . . . . . . . . . . . . 14 (𝑛 = (1st𝑝) → (𝐼𝑛) = (𝐼‘(1st𝑝)))
341340fveq1d 6407 . . . . . . . . . . . . 13 (𝑛 = (1st𝑝) → ((𝐼𝑛)‘𝑗) = ((𝐼‘(1st𝑝))‘𝑗))
342341feq1d 6238 . . . . . . . . . . . 12 (𝑛 = (1st𝑝) → (((𝐼𝑛)‘𝑗):𝑋⟶(ℝ × ℝ) ↔ ((𝐼‘(1st𝑝))‘𝑗):𝑋⟶(ℝ × ℝ)))
343339, 342imbi12d 335 . . . . . . . . . . 11 (𝑛 = (1st𝑝) → (((𝜑𝑛 ∈ ℕ ∧ 𝑗 ∈ ℕ) → ((𝐼𝑛)‘𝑗):𝑋⟶(ℝ × ℝ)) ↔ ((𝜑 ∧ (1st𝑝) ∈ ℕ ∧ 𝑗 ∈ ℕ) → ((𝐼‘(1st𝑝))‘𝑗):𝑋⟶(ℝ × ℝ))))
344337, 343, 106vtocl 3451 . . . . . . . . . 10 ((𝜑 ∧ (1st𝑝) ∈ ℕ ∧ 𝑗 ∈ ℕ) → ((𝐼‘(1st𝑝))‘𝑗):𝑋⟶(ℝ × ℝ))
345331, 336, 344vtocl 3451 . . . . . . . . 9 ((𝜑 ∧ (1st𝑝) ∈ ℕ ∧ (2nd𝑝) ∈ ℕ) → ((𝐼‘(1st𝑝))‘(2nd𝑝)):𝑋⟶(ℝ × ℝ))
346326, 328, 330, 345syl3anc 1483 . . . . . . . 8 ((𝜑𝑝 ∈ (ℕ × ℕ)) → ((𝐼‘(1st𝑝))‘(2nd𝑝)):𝑋⟶(ℝ × ℝ))
347324, 325, 19, 346hoiprodcl2 41248 . . . . . . 7 ((𝜑𝑝 ∈ (ℕ × ℕ)) → (𝐿‘((𝐼‘(1st𝑝))‘(2nd𝑝))) ∈ (0[,)+∞))
34815, 347sseldi 3793 . . . . . 6 ((𝜑𝑝 ∈ (ℕ × ℕ)) → (𝐿‘((𝐼‘(1st𝑝))‘(2nd𝑝))) ∈ (0[,]+∞))
349318, 12, 322, 14, 20, 323, 348sge0f1o 41075 . . . . 5 (𝜑 → (Σ^‘(𝑝 ∈ (ℕ × ℕ) ↦ (𝐿‘((𝐼‘(1st𝑝))‘(2nd𝑝))))) = (Σ^‘(𝑚 ∈ ℕ ↦ (𝐿‘((𝐼‘(1st ‘(𝐹𝑚)))‘(2nd ‘(𝐹𝑚)))))))
350317, 349eqtr4d 2842 . . . 4 (𝜑 → (Σ^‘(𝑚 ∈ ℕ ↦ (𝐿‘(𝐺𝑚)))) = (Σ^‘(𝑝 ∈ (ℕ × ℕ) ↦ (𝐿‘((𝐼‘(1st𝑝))‘(2nd𝑝))))))
351 nfv 2008 . . . . . . 7 𝑗𝜑
352272, 273op1std 7405 . . . . . . . . . 10 (𝑝 = ⟨𝑛, 𝑗⟩ → (1st𝑝) = 𝑛)
353352fveq2d 6409 . . . . . . . . 9 (𝑝 = ⟨𝑛, 𝑗⟩ → (𝐼‘(1st𝑝)) = (𝐼𝑛))
354272, 273op2ndd 7406 . . . . . . . . 9 (𝑝 = ⟨𝑛, 𝑗⟩ → (2nd𝑝) = 𝑗)
355353, 354fveq12d 6412 . . . . . . . 8 (𝑝 = ⟨𝑛, 𝑗⟩ → ((𝐼‘(1st𝑝))‘(2nd𝑝)) = ((𝐼𝑛)‘𝑗))
356355fveq2d 6409 . . . . . . 7 (𝑝 = ⟨𝑛, 𝑗⟩ → (𝐿‘((𝐼‘(1st𝑝))‘(2nd𝑝))) = (𝐿‘((𝐼𝑛)‘𝑗)))
357 nfv 2008 . . . . . . . . . 10 𝑘((𝜑𝑛 ∈ ℕ) ∧ 𝑗 ∈ ℕ)
358127adantr 468 . . . . . . . . . 10 (((𝜑𝑛 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → 𝑋 ∈ Fin)
35997, 105syl 17 . . . . . . . . . 10 (((𝜑𝑛 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → ((𝐼𝑛)‘𝑗):𝑋⟶(ℝ × ℝ))
360357, 358, 19, 359hoiprodcl2 41248 . . . . . . . . 9 (((𝜑𝑛 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → (𝐿‘((𝐼𝑛)‘𝑗)) ∈ (0[,)+∞))
36115, 360sseldi 3793 . . . . . . . 8 (((𝜑𝑛 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → (𝐿‘((𝐼𝑛)‘𝑗)) ∈ (0[,]+∞))
3623613impa 1129 . . . . . . 7 ((𝜑𝑛 ∈ ℕ ∧ 𝑗 ∈ ℕ) → (𝐿‘((𝐼𝑛)‘𝑗)) ∈ (0[,]+∞))
363351, 356, 14, 14, 362sge0xp 41122 . . . . . 6 (𝜑 → (Σ^‘(𝑛 ∈ ℕ ↦ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘((𝐼𝑛)‘𝑗)))))) = (Σ^‘(𝑝 ∈ (ℕ × ℕ) ↦ (𝐿‘((𝐼‘(1st𝑝))‘(2nd𝑝))))))
364363eqcomd 2811 . . . . 5 (𝜑 → (Σ^‘(𝑝 ∈ (ℕ × ℕ) ↦ (𝐿‘((𝐼‘(1st𝑝))‘(2nd𝑝))))) = (Σ^‘(𝑛 ∈ ℕ ↦ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘((𝐼𝑛)‘𝑗)))))))
36513a1i 11 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → ℕ ∈ V)
366 eqid 2805 . . . . . . . 8 (𝑗 ∈ ℕ ↦ (𝐿‘((𝐼𝑛)‘𝑗))) = (𝑗 ∈ ℕ ↦ (𝐿‘((𝐼𝑛)‘𝑗)))
367361, 366fmptd 6603 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → (𝑗 ∈ ℕ ↦ (𝐿‘((𝐼𝑛)‘𝑗))):ℕ⟶(0[,]+∞))
368365, 367sge0cl 41074 . . . . . 6 ((𝜑𝑛 ∈ ℕ) → (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘((𝐼𝑛)‘𝑗)))) ∈ (0[,]+∞))
369 fveq1 6404 . . . . . . . . . . . . 13 (𝑖 = (𝐼𝑛) → (𝑖𝑗) = ((𝐼𝑛)‘𝑗))
370369fveq2d 6409 . . . . . . . . . . . 12 (𝑖 = (𝐼𝑛) → (𝐿‘(𝑖𝑗)) = (𝐿‘((𝐼𝑛)‘𝑗)))
371370mpteq2dv 4935 . . . . . . . . . . 11 (𝑖 = (𝐼𝑛) → (𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗))) = (𝑗 ∈ ℕ ↦ (𝐿‘((𝐼𝑛)‘𝑗))))
372371fveq2d 6409 . . . . . . . . . 10 (𝑖 = (𝐼𝑛) → (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) = (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘((𝐼𝑛)‘𝑗)))))
373372breq1d 4850 . . . . . . . . 9 (𝑖 = (𝐼𝑛) → ((Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛))) ↔ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘((𝐼𝑛)‘𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛)))))
374373elrab 3558 . . . . . . . 8 ((𝐼𝑛) ∈ {𝑖 ∈ (𝐶‘(𝐴𝑛)) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛)))} ↔ ((𝐼𝑛) ∈ (𝐶‘(𝐴𝑛)) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘((𝐼𝑛)‘𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛)))))
375246, 374sylib 209 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → ((𝐼𝑛) ∈ (𝐶‘(𝐴𝑛)) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘((𝐼𝑛)‘𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛)))))
376375simprd 485 . . . . . 6 ((𝜑𝑛 ∈ ℕ) → (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘((𝐼𝑛)‘𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛))))
377122, 14, 368, 179, 376sge0lempt 41103 . . . . 5 (𝜑 → (Σ^‘(𝑛 ∈ ℕ ↦ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘((𝐼𝑛)‘𝑗)))))) ≤ (Σ^‘(𝑛 ∈ ℕ ↦ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛))))))
378364, 377eqbrtrd 4862 . . . 4 (𝜑 → (Σ^‘(𝑝 ∈ (ℕ × ℕ) ↦ (𝐿‘((𝐼‘(1st𝑝))‘(2nd𝑝))))) ≤ (Σ^‘(𝑛 ∈ ℕ ↦ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛))))))
379350, 378eqbrtrd 4862 . . 3 (𝜑 → (Σ^‘(𝑚 ∈ ℕ ↦ (𝐿‘(𝐺𝑚)))) ≤ (Σ^‘(𝑛 ∈ ℕ ↦ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛))))))
38011, 121, 180, 314, 379xrletrd 12207 . 2 (𝜑 → ((voln*‘𝑋)‘ 𝑛 ∈ ℕ (𝐴𝑛)) ≤ (Σ^‘(𝑛 ∈ ℕ ↦ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛))))))
381122, 14, 166, 174sge0xadd 41128 . . 3 (𝜑 → (Σ^‘(𝑛 ∈ ℕ ↦ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛))))) = ((Σ^‘(𝑛 ∈ ℕ ↦ ((voln*‘𝑋)‘(𝐴𝑛)))) +𝑒^‘(𝑛 ∈ ℕ ↦ (𝐸 / (2↑𝑛))))))
382123a1i 11 . . . . . 6 (𝜑 → 0 ∈ ℝ*)
383125a1i 11 . . . . . 6 (𝜑 → +∞ ∈ ℝ*)
384151rexrd 10371 . . . . . 6 (𝜑𝐸 ∈ ℝ*)
38574rpge0d 12086 . . . . . 6 (𝜑 → 0 ≤ 𝐸)
386151ltpnfd 12167 . . . . . 6 (𝜑𝐸 < +∞)
387382, 383, 384, 385, 386elicod 12438 . . . . 5 (𝜑𝐸 ∈ (0[,)+∞))
388387sge0ad2en 41124 . . . 4 (𝜑 → (Σ^‘(𝑛 ∈ ℕ ↦ (𝐸 / (2↑𝑛)))) = 𝐸)
389388oveq2d 6887 . . 3 (𝜑 → ((Σ^‘(𝑛 ∈ ℕ ↦ ((voln*‘𝑋)‘(𝐴𝑛)))) +𝑒^‘(𝑛 ∈ ℕ ↦ (𝐸 / (2↑𝑛))))) = ((Σ^‘(𝑛 ∈ ℕ ↦ ((voln*‘𝑋)‘(𝐴𝑛)))) +𝑒 𝐸))
390381, 389eqtrd 2839 . 2 (𝜑 → (Σ^‘(𝑛 ∈ ℕ ↦ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛))))) = ((Σ^‘(𝑛 ∈ ℕ ↦ ((voln*‘𝑋)‘(𝐴𝑛)))) +𝑒 𝐸))
391380, 390breqtrd 4866 1 (𝜑 → ((voln*‘𝑋)‘ 𝑛 ∈ ℕ (𝐴𝑛)) ≤ ((Σ^‘(𝑛 ∈ ℕ ↦ ((voln*‘𝑋)‘(𝐴𝑛)))) +𝑒 𝐸))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1100   = wceq 1637  wcel 2158  wne 2977  wral 3095  wrex 3096  {crab 3099  Vcvv 3390  wss 3766  c0 4113  ifcif 4276  𝒫 cpw 4348  cop 4373   ciun 4708   class class class wbr 4840  cmpt 4919   × cxp 5306  ccom 5312   Fn wfn 6093  wf 6094  ontowfo 6096  1-1-ontowf1o 6097  cfv 6098  (class class class)co 6871  1st c1st 7393  2nd c2nd 7394  𝑚 cmap 8089  Xcixp 8142  Fincfn 8189  infcinf 8583  cr 10217  0cc0 10218  +∞cpnf 10353  *cxr 10355   < clt 10356  cle 10357   / cdiv 10966  cn 11302  2c2 11352  +crp 12042   +𝑒 cxad 12156  [,)cico 12391  [,]cicc 12392  cexp 13079  cprod 14852  volcvol 23440  Σ^csumge0 41055  voln*covoln 41229
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1880  ax-4 1897  ax-5 2004  ax-6 2070  ax-7 2106  ax-8 2160  ax-9 2167  ax-10 2187  ax-11 2203  ax-12 2216  ax-13 2422  ax-ext 2784  ax-rep 4960  ax-sep 4971  ax-nul 4980  ax-pow 5032  ax-pr 5093  ax-un 7176  ax-inf2 8782  ax-ac2 9567  ax-cnex 10274  ax-resscn 10275  ax-1cn 10276  ax-icn 10277  ax-addcl 10278  ax-addrcl 10279  ax-mulcl 10280  ax-mulrcl 10281  ax-mulcom 10282  ax-addass 10283  ax-mulass 10284  ax-distr 10285  ax-i2m1 10286  ax-1ne0 10287  ax-1rid 10288  ax-rnegex 10289  ax-rrecex 10290  ax-cnre 10291  ax-pre-lttri 10292  ax-pre-lttrn 10293  ax-pre-ltadd 10294  ax-pre-mulgt0 10295  ax-pre-sup 10296  ax-addf 10297  ax-mulf 10298
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-fal 1651  df-ex 1860  df-nf 1865  df-sb 2063  df-eu 2636  df-mo 2637  df-clab 2792  df-cleq 2798  df-clel 2801  df-nfc 2936  df-ne 2978  df-nel 3081  df-ral 3100  df-rex 3101  df-reu 3102  df-rmo 3103  df-rab 3104  df-v 3392  df-sbc 3631  df-csb 3726  df-dif 3769  df-un 3771  df-in 3773  df-ss 3780  df-pss 3782  df-nul 4114  df-if 4277  df-pw 4350  df-sn 4368  df-pr 4370  df-tp 4372  df-op 4374  df-uni 4627  df-int 4666  df-iun 4710  df-disj 4809  df-br 4841  df-opab 4903  df-mpt 4920  df-tr 4943  df-id 5216  df-eprel 5221  df-po 5229  df-so 5230  df-fr 5267  df-se 5268  df-we 5269  df-xp 5314  df-rel 5315  df-cnv 5316  df-co 5317  df-dm 5318  df-rn 5319  df-res 5320  df-ima 5321  df-pred 5890  df-ord 5936  df-on 5937  df-lim 5938  df-suc 5939  df-iota 6061  df-fun 6100  df-fn 6101  df-f 6102  df-f1 6103  df-fo 6104  df-f1o 6105  df-fv 6106  df-isom 6107  df-riota 6832  df-ov 6874  df-oprab 6875  df-mpt2 6876  df-of 7124  df-om 7293  df-1st 7395  df-2nd 7396  df-tpos 7584  df-wrecs 7639  df-recs 7701  df-rdg 7739  df-1o 7793  df-2o 7794  df-oadd 7797  df-er 7976  df-map 8091  df-pm 8092  df-ixp 8143  df-en 8190  df-dom 8191  df-sdom 8192  df-fin 8193  df-fi 8553  df-sup 8584  df-inf 8585  df-oi 8651  df-card 9045  df-acn 9048  df-ac 9219  df-cda 9272  df-pnf 10358  df-mnf 10359  df-xr 10360  df-ltxr 10361  df-le 10362  df-sub 10550  df-neg 10551  df-div 10967  df-nn 11303  df-2 11360  df-3 11361  df-4 11362  df-5 11363  df-6 11364  df-7 11365  df-8 11366  df-9 11367  df-n0 11556  df-z 11640  df-dec 11756  df-uz 11901  df-q 12004  df-rp 12043  df-xneg 12158  df-xadd 12159  df-xmul 12160  df-ioo 12393  df-ico 12395  df-icc 12396  df-fz 12546  df-fzo 12686  df-fl 12813  df-seq 13021  df-exp 13080  df-hash 13334  df-cj 14058  df-re 14059  df-im 14060  df-sqrt 14194  df-abs 14195  df-clim 14438  df-rlim 14439  df-sum 14636  df-prod 14853  df-struct 16066  df-ndx 16067  df-slot 16068  df-base 16070  df-sets 16071  df-ress 16072  df-plusg 16162  df-mulr 16163  df-starv 16164  df-tset 16168  df-ple 16169  df-ds 16171  df-unif 16172  df-rest 16284  df-0g 16303  df-topgen 16305  df-mgm 17443  df-sgrp 17485  df-mnd 17496  df-grp 17626  df-minusg 17627  df-subg 17789  df-cmn 18392  df-abl 18393  df-mgp 18688  df-ur 18700  df-ring 18747  df-cring 18748  df-oppr 18821  df-dvdsr 18839  df-unit 18840  df-invr 18870  df-dvr 18881  df-drng 18949  df-psmet 19942  df-xmet 19943  df-met 19944  df-bl 19945  df-mopn 19946  df-cnfld 19951  df-top 20908  df-topon 20925  df-bases 20960  df-cmp 21400  df-ovol 23441  df-vol 23442  df-sumge0 41056  df-ovoln 41230
This theorem is referenced by:  ovnsubaddlem2  41264
  Copyright terms: Public domain W3C validator