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

 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.z 𝑍 = (𝑎 ∈ 𝒫 (ℝ ↑𝑚 𝑋) ↦ {𝑧 ∈ ℝ* ∣ ∃𝑖 ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)(𝑎 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑖𝑗))‘𝑘) ∧ 𝑧 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘𝑋 (vol‘(([,) ∘ (𝑖𝑗))‘𝑘)))))})
ovnsubaddlem1.c 𝐶 = (𝑎 ∈ 𝒫 (ℝ ↑𝑚 𝑋) ↦ { ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∣ 𝑎 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘)})
ovnsubaddlem1.l 𝐿 = (𝑖 ∈ ((ℝ × ℝ) ↑𝑚 𝑋) ↦ ∏𝑘𝑋 (vol‘(([,) ∘ 𝑖)‘𝑘)))
ovnsubaddlem1.d 𝐷 = (𝑎 ∈ 𝒫 (ℝ ↑𝑚 𝑋) ↦ (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶𝑎) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘𝑎) +𝑒 𝑒)}))
ovnsubaddlem1.i ((𝜑𝑛 ∈ ℕ) → (𝐼𝑛) ∈ ((𝐷‘(𝐴𝑛))‘(𝐸 / (2↑𝑛))))
ovnsubaddlem1.g 𝐺 = (𝑚 ∈ ℕ ↦ ((𝐼‘(1st ‘(𝐹𝑚)))‘(2nd ‘(𝐹𝑚))))
Assertion
Ref Expression
ovnsubaddlem1 (𝜑 → ((voln*‘𝑋)‘ 𝑛 ∈ ℕ (𝐴𝑛)) ≤ ((Σ^‘(𝑛 ∈ ℕ ↦ ((voln*‘𝑋)‘(𝐴𝑛)))) +𝑒 𝐸))
Distinct variable groups:   𝐴,𝑎,𝑒,𝑖,𝑛   𝐴,,𝑎,𝑛   𝑧,𝐴,𝑎,𝑖,𝑛   𝐶,𝑎,𝑒,𝑖   𝐷,𝑛   𝑒,𝐸,𝑖,𝑛   𝐹,𝑎,𝑒,𝑖,𝑗,𝑚,𝑛   ,𝐹,𝑘,𝑎,𝑗,𝑚,𝑛   𝑖,𝑘,𝐺,𝑗,𝑚,𝑛   ,𝐼,𝑗,𝑘,𝑚,𝑛   𝑖,𝐼   𝐿,𝑎,𝑒,𝑖,𝑗,𝑚,𝑛   𝑋,𝑎,𝑒,𝑖,𝑗,𝑚,𝑛   ,𝑋,𝑘   𝑧,𝑋,𝑗,𝑘   𝜑,𝑎,𝑒,𝑖,𝑗,𝑚,𝑛   𝜑,𝑘
Allowed substitution hints:   𝜑(𝑧,)   𝐴(𝑗,𝑘,𝑚)   𝐶(𝑧,,𝑗,𝑘,𝑚,𝑛)   𝐷(𝑧,𝑒,,𝑖,𝑗,𝑘,𝑚,𝑎)   𝐸(𝑧,,𝑗,𝑘,𝑚,𝑎)   𝐹(𝑧)   𝐺(𝑧,𝑒,,𝑎)   𝐼(𝑧,𝑒,𝑎)   𝐿(𝑧,,𝑘)   𝑍(𝑧,𝑒,,𝑖,𝑗,𝑘,𝑚,𝑛,𝑎)

Dummy variable 𝑝 is distinct from all other variables.
StepHypRef Expression
1 ovnsubaddlem1.x . . . 4 (𝜑𝑋 ∈ Fin)
2 ovnsubaddlem1.a . . . . . . . . 9 (𝜑𝐴:ℕ⟶𝒫 (ℝ ↑𝑚 𝑋))
32adantr 480 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → 𝐴:ℕ⟶𝒫 (ℝ ↑𝑚 𝑋))
4 simpr 476 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → 𝑛 ∈ ℕ)
53, 4ffvelrnd 6268 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → (𝐴𝑛) ∈ 𝒫 (ℝ ↑𝑚 𝑋))
6 elpwi 4117 . . . . . . 7 ((𝐴𝑛) ∈ 𝒫 (ℝ ↑𝑚 𝑋) → (𝐴𝑛) ⊆ (ℝ ↑𝑚 𝑋))
75, 6syl 17 . . . . . 6 ((𝜑𝑛 ∈ ℕ) → (𝐴𝑛) ⊆ (ℝ ↑𝑚 𝑋))
87ralrimiva 2949 . . . . 5 (𝜑 → ∀𝑛 ∈ ℕ (𝐴𝑛) ⊆ (ℝ ↑𝑚 𝑋))
9 iunss 4497 . . . . 5 ( 𝑛 ∈ ℕ (𝐴𝑛) ⊆ (ℝ ↑𝑚 𝑋) ↔ ∀𝑛 ∈ ℕ (𝐴𝑛) ⊆ (ℝ ↑𝑚 𝑋))
108, 9sylibr 223 . . . 4 (𝜑 𝑛 ∈ ℕ (𝐴𝑛) ⊆ (ℝ ↑𝑚 𝑋))
111, 10ovnxrcl 39459 . . 3 (𝜑 → ((voln*‘𝑋)‘ 𝑛 ∈ ℕ (𝐴𝑛)) ∈ ℝ*)
12 nfv 1830 . . . 4 𝑚𝜑
13 nnex 10903 . . . . 5 ℕ ∈ V
1413a1i 11 . . . 4 (𝜑 → ℕ ∈ V)
15 icossicc 12131 . . . . 5 (0[,)+∞) ⊆ (0[,]+∞)
16 nfv 1830 . . . . . 6 𝑘(𝜑𝑚 ∈ ℕ)
17 simpl 472 . . . . . . 7 ((𝜑𝑚 ∈ ℕ) → 𝜑)
1817, 1syl 17 . . . . . 6 ((𝜑𝑚 ∈ ℕ) → 𝑋 ∈ Fin)
19 ovnsubaddlem1.l . . . . . 6 𝐿 = (𝑖 ∈ ((ℝ × ℝ) ↑𝑚 𝑋) ↦ ∏𝑘𝑋 (vol‘(([,) ∘ 𝑖)‘𝑘)))
20 ovnsubaddlem1.f . . . . . . . . . . . 12 (𝜑𝐹:ℕ–1-1-onto→(ℕ × ℕ))
21 f1of 6050 . . . . . . . . . . . 12 (𝐹:ℕ–1-1-onto→(ℕ × ℕ) → 𝐹:ℕ⟶(ℕ × ℕ))
2220, 21syl 17 . . . . . . . . . . 11 (𝜑𝐹:ℕ⟶(ℕ × ℕ))
2322adantr 480 . . . . . . . . . 10 ((𝜑𝑚 ∈ ℕ) → 𝐹:ℕ⟶(ℕ × ℕ))
24 simpr 476 . . . . . . . . . 10 ((𝜑𝑚 ∈ ℕ) → 𝑚 ∈ ℕ)
2523, 24ffvelrnd 6268 . . . . . . . . 9 ((𝜑𝑚 ∈ ℕ) → (𝐹𝑚) ∈ (ℕ × ℕ))
26 xp1st 7089 . . . . . . . . 9 ((𝐹𝑚) ∈ (ℕ × ℕ) → (1st ‘(𝐹𝑚)) ∈ ℕ)
2725, 26syl 17 . . . . . . . 8 ((𝜑𝑚 ∈ ℕ) → (1st ‘(𝐹𝑚)) ∈ ℕ)
28 xp2nd 7090 . . . . . . . . 9 ((𝐹𝑚) ∈ (ℕ × ℕ) → (2nd ‘(𝐹𝑚)) ∈ ℕ)
2925, 28syl 17 . . . . . . . 8 ((𝜑𝑚 ∈ ℕ) → (2nd ‘(𝐹𝑚)) ∈ ℕ)
30 fvex 6113 . . . . . . . . 9 (2nd ‘(𝐹𝑚)) ∈ V
31 eleq1 2676 . . . . . . . . . . 11 (𝑗 = (2nd ‘(𝐹𝑚)) → (𝑗 ∈ ℕ ↔ (2nd ‘(𝐹𝑚)) ∈ ℕ))
32313anbi3d 1397 . . . . . . . . . 10 (𝑗 = (2nd ‘(𝐹𝑚)) → ((𝜑 ∧ (1st ‘(𝐹𝑚)) ∈ ℕ ∧ 𝑗 ∈ ℕ) ↔ (𝜑 ∧ (1st ‘(𝐹𝑚)) ∈ ℕ ∧ (2nd ‘(𝐹𝑚)) ∈ ℕ)))
33 fveq2 6103 . . . . . . . . . . 11 (𝑗 = (2nd ‘(𝐹𝑚)) → ((𝐼‘(1st ‘(𝐹𝑚)))‘𝑗) = ((𝐼‘(1st ‘(𝐹𝑚)))‘(2nd ‘(𝐹𝑚))))
3433feq1d 5943 . . . . . . . . . 10 (𝑗 = (2nd ‘(𝐹𝑚)) → (((𝐼‘(1st ‘(𝐹𝑚)))‘𝑗):𝑋⟶(ℝ × ℝ) ↔ ((𝐼‘(1st ‘(𝐹𝑚)))‘(2nd ‘(𝐹𝑚))):𝑋⟶(ℝ × ℝ)))
3532, 34imbi12d 333 . . . . . . . . 9 (𝑗 = (2nd ‘(𝐹𝑚)) → (((𝜑 ∧ (1st ‘(𝐹𝑚)) ∈ ℕ ∧ 𝑗 ∈ ℕ) → ((𝐼‘(1st ‘(𝐹𝑚)))‘𝑗):𝑋⟶(ℝ × ℝ)) ↔ ((𝜑 ∧ (1st ‘(𝐹𝑚)) ∈ ℕ ∧ (2nd ‘(𝐹𝑚)) ∈ ℕ) → ((𝐼‘(1st ‘(𝐹𝑚)))‘(2nd ‘(𝐹𝑚))):𝑋⟶(ℝ × ℝ))))
36 fvex 6113 . . . . . . . . . 10 (1st ‘(𝐹𝑚)) ∈ V
37 eleq1 2676 . . . . . . . . . . . 12 (𝑛 = (1st ‘(𝐹𝑚)) → (𝑛 ∈ ℕ ↔ (1st ‘(𝐹𝑚)) ∈ ℕ))
38373anbi2d 1396 . . . . . . . . . . 11 (𝑛 = (1st ‘(𝐹𝑚)) → ((𝜑𝑛 ∈ ℕ ∧ 𝑗 ∈ ℕ) ↔ (𝜑 ∧ (1st ‘(𝐹𝑚)) ∈ ℕ ∧ 𝑗 ∈ ℕ)))
39 fveq2 6103 . . . . . . . . . . . . 13 (𝑛 = (1st ‘(𝐹𝑚)) → (𝐼𝑛) = (𝐼‘(1st ‘(𝐹𝑚))))
4039fveq1d 6105 . . . . . . . . . . . 12 (𝑛 = (1st ‘(𝐹𝑚)) → ((𝐼𝑛)‘𝑗) = ((𝐼‘(1st ‘(𝐹𝑚)))‘𝑗))
4140feq1d 5943 . . . . . . . . . . 11 (𝑛 = (1st ‘(𝐹𝑚)) → (((𝐼𝑛)‘𝑗):𝑋⟶(ℝ × ℝ) ↔ ((𝐼‘(1st ‘(𝐹𝑚)))‘𝑗):𝑋⟶(ℝ × ℝ)))
4238, 41imbi12d 333 . . . . . . . . . 10 (𝑛 = (1st ‘(𝐹𝑚)) → (((𝜑𝑛 ∈ ℕ ∧ 𝑗 ∈ ℕ) → ((𝐼𝑛)‘𝑗):𝑋⟶(ℝ × ℝ)) ↔ ((𝜑 ∧ (1st ‘(𝐹𝑚)) ∈ ℕ ∧ 𝑗 ∈ ℕ) → ((𝐼‘(1st ‘(𝐹𝑚)))‘𝑗):𝑋⟶(ℝ × ℝ))))
43 ovnsubaddlem1.c . . . . . . . . . . . . . . . . . . . 20 𝐶 = (𝑎 ∈ 𝒫 (ℝ ↑𝑚 𝑋) ↦ { ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∣ 𝑎 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘)})
4443a1i 11 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑛 ∈ ℕ) → 𝐶 = (𝑎 ∈ 𝒫 (ℝ ↑𝑚 𝑋) ↦ { ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∣ 𝑎 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘)}))
45 sseq1 3589 . . . . . . . . . . . . . . . . . . . . 21 (𝑎 = (𝐴𝑛) → (𝑎 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘) ↔ (𝐴𝑛) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘)))
4645rabbidv 3164 . . . . . . . . . . . . . . . . . . . 20 (𝑎 = (𝐴𝑛) → { ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∣ 𝑎 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘)} = { ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∣ (𝐴𝑛) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘)})
4746adantl 481 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑛 ∈ ℕ) ∧ 𝑎 = (𝐴𝑛)) → { ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∣ 𝑎 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘)} = { ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∣ (𝐴𝑛) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘)})
48 ovex 6577 . . . . . . . . . . . . . . . . . . . . 21 (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∈ V
4948rabex 4740 . . . . . . . . . . . . . . . . . . . 20 { ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∣ (𝐴𝑛) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘)} ∈ V
5049a1i 11 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑛 ∈ ℕ) → { ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∣ (𝐴𝑛) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘)} ∈ V)
5144, 47, 5, 50fvmptd 6197 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑛 ∈ ℕ) → (𝐶‘(𝐴𝑛)) = { ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∣ (𝐴𝑛) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘)})
52 ssrab2 3650 . . . . . . . . . . . . . . . . . . 19 { ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∣ (𝐴𝑛) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘)} ⊆ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)
5352a1i 11 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑛 ∈ ℕ) → { ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∣ (𝐴𝑛) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘)} ⊆ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ))
5451, 53eqsstrd 3602 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛 ∈ ℕ) → (𝐶‘(𝐴𝑛)) ⊆ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ))
55 ovnsubaddlem1.d . . . . . . . . . . . . . . . . . . . . . 22 𝐷 = (𝑎 ∈ 𝒫 (ℝ ↑𝑚 𝑋) ↦ (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶𝑎) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘𝑎) +𝑒 𝑒)}))
5655a1i 11 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑛 ∈ ℕ) → 𝐷 = (𝑎 ∈ 𝒫 (ℝ ↑𝑚 𝑋) ↦ (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶𝑎) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘𝑎) +𝑒 𝑒)})))
57 fveq2 6103 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑎 = (𝐴𝑛) → (𝐶𝑎) = (𝐶‘(𝐴𝑛)))
5857eleq2d 2673 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑎 = (𝐴𝑛) → (𝑖 ∈ (𝐶𝑎) ↔ 𝑖 ∈ (𝐶‘(𝐴𝑛))))
59 fveq2 6103 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑎 = (𝐴𝑛) → ((voln*‘𝑋)‘𝑎) = ((voln*‘𝑋)‘(𝐴𝑛)))
6059oveq1d 6564 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑎 = (𝐴𝑛) → (((voln*‘𝑋)‘𝑎) +𝑒 𝑒) = (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 𝑒))
6160breq2d 4595 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑎 = (𝐴𝑛) → ((Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘𝑎) +𝑒 𝑒) ↔ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 𝑒)))
6258, 61anbi12d 743 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑎 = (𝐴𝑛) → ((𝑖 ∈ (𝐶𝑎) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘𝑎) +𝑒 𝑒)) ↔ (𝑖 ∈ (𝐶‘(𝐴𝑛)) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 𝑒))))
6362rabbidva2 3162 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑎 = (𝐴𝑛) → {𝑖 ∈ (𝐶𝑎) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘𝑎) +𝑒 𝑒)} = {𝑖 ∈ (𝐶‘(𝐴𝑛)) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 𝑒)})
6463mpteq2dv 4673 . . . . . . . . . . . . . . . . . . . . . 22 (𝑎 = (𝐴𝑛) → (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶𝑎) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘𝑎) +𝑒 𝑒)}) = (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶‘(𝐴𝑛)) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 𝑒)}))
6564adantl 481 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑛 ∈ ℕ) ∧ 𝑎 = (𝐴𝑛)) → (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶𝑎) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘𝑎) +𝑒 𝑒)}) = (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶‘(𝐴𝑛)) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 𝑒)}))
66 rpex 38503 . . . . . . . . . . . . . . . . . . . . . . 23 + ∈ V
6766mptex 6390 . . . . . . . . . . . . . . . . . . . . . 22 (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶‘(𝐴𝑛)) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 𝑒)}) ∈ V
6867a1i 11 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑛 ∈ ℕ) → (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶‘(𝐴𝑛)) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 𝑒)}) ∈ V)
6956, 65, 5, 68fvmptd 6197 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑛 ∈ ℕ) → (𝐷‘(𝐴𝑛)) = (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶‘(𝐴𝑛)) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 𝑒)}))
70 oveq2 6557 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑒 = (𝐸 / (2↑𝑛)) → (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 𝑒) = (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛))))
7170breq2d 4595 . . . . . . . . . . . . . . . . . . . . . 22 (𝑒 = (𝐸 / (2↑𝑛)) → ((Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 𝑒) ↔ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛)))))
7271rabbidv 3164 . . . . . . . . . . . . . . . . . . . . 21 (𝑒 = (𝐸 / (2↑𝑛)) → {𝑖 ∈ (𝐶‘(𝐴𝑛)) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 𝑒)} = {𝑖 ∈ (𝐶‘(𝐴𝑛)) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛)))})
7372adantl 481 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑛 ∈ ℕ) ∧ 𝑒 = (𝐸 / (2↑𝑛))) → {𝑖 ∈ (𝐶‘(𝐴𝑛)) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 𝑒)} = {𝑖 ∈ (𝐶‘(𝐴𝑛)) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛)))})
74 ovnsubaddlem1.e . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝐸 ∈ ℝ+)
7574adantr 480 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑛 ∈ ℕ) → 𝐸 ∈ ℝ+)
76 2nn 11062 . . . . . . . . . . . . . . . . . . . . . . . . 25 2 ∈ ℕ
7776a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 ∈ ℕ → 2 ∈ ℕ)
78 nnnn0 11176 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 ∈ ℕ → 𝑛 ∈ ℕ0)
7977, 78nnexpcld 12892 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 ∈ ℕ → (2↑𝑛) ∈ ℕ)
8079nnrpd 11746 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 ∈ ℕ → (2↑𝑛) ∈ ℝ+)
8180adantl 481 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑛 ∈ ℕ) → (2↑𝑛) ∈ ℝ+)
8275, 81rpdivcld 11765 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑛 ∈ ℕ) → (𝐸 / (2↑𝑛)) ∈ ℝ+)
83 fvex 6113 . . . . . . . . . . . . . . . . . . . . . 22 (𝐶‘(𝐴𝑛)) ∈ V
8483rabex 4740 . . . . . . . . . . . . . . . . . . . . 21 {𝑖 ∈ (𝐶‘(𝐴𝑛)) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛)))} ∈ V
8584a1i 11 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑛 ∈ ℕ) → {𝑖 ∈ (𝐶‘(𝐴𝑛)) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛)))} ∈ V)
8669, 73, 82, 85fvmptd 6197 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑛 ∈ ℕ) → ((𝐷‘(𝐴𝑛))‘(𝐸 / (2↑𝑛))) = {𝑖 ∈ (𝐶‘(𝐴𝑛)) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛)))})
87 ssrab2 3650 . . . . . . . . . . . . . . . . . . . 20 {𝑖 ∈ (𝐶‘(𝐴𝑛)) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛)))} ⊆ (𝐶‘(𝐴𝑛))
8887a1i 11 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑛 ∈ ℕ) → {𝑖 ∈ (𝐶‘(𝐴𝑛)) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛)))} ⊆ (𝐶‘(𝐴𝑛)))
8986, 88eqsstrd 3602 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑛 ∈ ℕ) → ((𝐷‘(𝐴𝑛))‘(𝐸 / (2↑𝑛))) ⊆ (𝐶‘(𝐴𝑛)))
90 ovnsubaddlem1.i . . . . . . . . . . . . . . . . . 18 ((𝜑𝑛 ∈ ℕ) → (𝐼𝑛) ∈ ((𝐷‘(𝐴𝑛))‘(𝐸 / (2↑𝑛))))
9189, 90sseldd 3569 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛 ∈ ℕ) → (𝐼𝑛) ∈ (𝐶‘(𝐴𝑛)))
9254, 91sseldd 3569 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ ℕ) → (𝐼𝑛) ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ))
93 elmapfn 7766 . . . . . . . . . . . . . . . 16 ((𝐼𝑛) ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) → (𝐼𝑛) Fn ℕ)
9492, 93syl 17 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ) → (𝐼𝑛) Fn ℕ)
95 elmapi 7765 . . . . . . . . . . . . . . . . . 18 ((𝐼𝑛) ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) → (𝐼𝑛):ℕ⟶((ℝ × ℝ) ↑𝑚 𝑋))
9692, 95syl 17 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛 ∈ ℕ) → (𝐼𝑛):ℕ⟶((ℝ × ℝ) ↑𝑚 𝑋))
9796ffvelrnda 6267 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → ((𝐼𝑛)‘𝑗) ∈ ((ℝ × ℝ) ↑𝑚 𝑋))
9897ralrimiva 2949 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ) → ∀𝑗 ∈ ℕ ((𝐼𝑛)‘𝑗) ∈ ((ℝ × ℝ) ↑𝑚 𝑋))
9994, 98jca 553 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ ℕ) → ((𝐼𝑛) Fn ℕ ∧ ∀𝑗 ∈ ℕ ((𝐼𝑛)‘𝑗) ∈ ((ℝ × ℝ) ↑𝑚 𝑋)))
100993adant3 1074 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ ℕ ∧ 𝑗 ∈ ℕ) → ((𝐼𝑛) Fn ℕ ∧ ∀𝑗 ∈ ℕ ((𝐼𝑛)‘𝑗) ∈ ((ℝ × ℝ) ↑𝑚 𝑋)))
101 ffnfv 6295 . . . . . . . . . . . . 13 ((𝐼𝑛):ℕ⟶((ℝ × ℝ) ↑𝑚 𝑋) ↔ ((𝐼𝑛) Fn ℕ ∧ ∀𝑗 ∈ ℕ ((𝐼𝑛)‘𝑗) ∈ ((ℝ × ℝ) ↑𝑚 𝑋)))
102100, 101sylibr 223 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ ∧ 𝑗 ∈ ℕ) → (𝐼𝑛):ℕ⟶((ℝ × ℝ) ↑𝑚 𝑋))
103 simp3 1056 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ ℕ)
104102, 103ffvelrnd 6268 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ ∧ 𝑗 ∈ ℕ) → ((𝐼𝑛)‘𝑗) ∈ ((ℝ × ℝ) ↑𝑚 𝑋))
105 elmapi 7765 . . . . . . . . . . 11 (((𝐼𝑛)‘𝑗) ∈ ((ℝ × ℝ) ↑𝑚 𝑋) → ((𝐼𝑛)‘𝑗):𝑋⟶(ℝ × ℝ))
106104, 105syl 17 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ ∧ 𝑗 ∈ ℕ) → ((𝐼𝑛)‘𝑗):𝑋⟶(ℝ × ℝ))
10736, 42, 106vtocl 3232 . . . . . . . . 9 ((𝜑 ∧ (1st ‘(𝐹𝑚)) ∈ ℕ ∧ 𝑗 ∈ ℕ) → ((𝐼‘(1st ‘(𝐹𝑚)))‘𝑗):𝑋⟶(ℝ × ℝ))
10830, 35, 107vtocl 3232 . . . . . . . 8 ((𝜑 ∧ (1st ‘(𝐹𝑚)) ∈ ℕ ∧ (2nd ‘(𝐹𝑚)) ∈ ℕ) → ((𝐼‘(1st ‘(𝐹𝑚)))‘(2nd ‘(𝐹𝑚))):𝑋⟶(ℝ × ℝ))
10917, 27, 29, 108syl3anc 1318 . . . . . . 7 ((𝜑𝑚 ∈ ℕ) → ((𝐼‘(1st ‘(𝐹𝑚)))‘(2nd ‘(𝐹𝑚))):𝑋⟶(ℝ × ℝ))
110 id 22 . . . . . . . . . 10 (𝑚 ∈ ℕ → 𝑚 ∈ ℕ)
111 fvex 6113 . . . . . . . . . . 11 ((𝐼‘(1st ‘(𝐹𝑚)))‘(2nd ‘(𝐹𝑚))) ∈ V
112111a1i 11 . . . . . . . . . 10 (𝑚 ∈ ℕ → ((𝐼‘(1st ‘(𝐹𝑚)))‘(2nd ‘(𝐹𝑚))) ∈ V)
113 ovnsubaddlem1.g . . . . . . . . . . 11 𝐺 = (𝑚 ∈ ℕ ↦ ((𝐼‘(1st ‘(𝐹𝑚)))‘(2nd ‘(𝐹𝑚))))
114113fvmpt2 6200 . . . . . . . . . 10 ((𝑚 ∈ ℕ ∧ ((𝐼‘(1st ‘(𝐹𝑚)))‘(2nd ‘(𝐹𝑚))) ∈ V) → (𝐺𝑚) = ((𝐼‘(1st ‘(𝐹𝑚)))‘(2nd ‘(𝐹𝑚))))
115110, 112, 114syl2anc 691 . . . . . . . . 9 (𝑚 ∈ ℕ → (𝐺𝑚) = ((𝐼‘(1st ‘(𝐹𝑚)))‘(2nd ‘(𝐹𝑚))))
116115adantl 481 . . . . . . . 8 ((𝜑𝑚 ∈ ℕ) → (𝐺𝑚) = ((𝐼‘(1st ‘(𝐹𝑚)))‘(2nd ‘(𝐹𝑚))))
117116feq1d 5943 . . . . . . 7 ((𝜑𝑚 ∈ ℕ) → ((𝐺𝑚):𝑋⟶(ℝ × ℝ) ↔ ((𝐼‘(1st ‘(𝐹𝑚)))‘(2nd ‘(𝐹𝑚))):𝑋⟶(ℝ × ℝ)))
118109, 117mpbird 246 . . . . . 6 ((𝜑𝑚 ∈ ℕ) → (𝐺𝑚):𝑋⟶(ℝ × ℝ))
11916, 18, 19, 118hoiprodcl2 39445 . . . . 5 ((𝜑𝑚 ∈ ℕ) → (𝐿‘(𝐺𝑚)) ∈ (0[,)+∞))
12015, 119sseldi 3566 . . . 4 ((𝜑𝑚 ∈ ℕ) → (𝐿‘(𝐺𝑚)) ∈ (0[,]+∞))
12112, 14, 120sge0xrclmpt 39321 . . 3 (𝜑 → (Σ^‘(𝑚 ∈ ℕ ↦ (𝐿‘(𝐺𝑚)))) ∈ ℝ*)
122 nfv 1830 . . . 4 𝑛𝜑
123 0xr 9965 . . . . . 6 0 ∈ ℝ*
124123a1i 11 . . . . 5 ((𝜑𝑛 ∈ ℕ) → 0 ∈ ℝ*)
125 pnfxr 9971 . . . . . 6 +∞ ∈ ℝ*
126125a1i 11 . . . . 5 ((𝜑𝑛 ∈ ℕ) → +∞ ∈ ℝ*)
1271adantr 480 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → 𝑋 ∈ Fin)
128 ovnsubaddlem1.z . . . . . . . . 9 𝑍 = (𝑎 ∈ 𝒫 (ℝ ↑𝑚 𝑋) ↦ {𝑧 ∈ ℝ* ∣ ∃𝑖 ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)(𝑎 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑖𝑗))‘𝑘) ∧ 𝑧 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘𝑋 (vol‘(([,) ∘ (𝑖𝑗))‘𝑘)))))})
129127, 7, 128ovnval2b 39442 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → ((voln*‘𝑋)‘(𝐴𝑛)) = if(𝑋 = ∅, 0, inf((𝑍‘(𝐴𝑛)), ℝ*, < )))
130 ovnsubaddlem1.n0 . . . . . . . . . . 11 (𝜑𝑋 ≠ ∅)
131130neneqd 2787 . . . . . . . . . 10 (𝜑 → ¬ 𝑋 = ∅)
132131iffalsed 4047 . . . . . . . . 9 (𝜑 → if(𝑋 = ∅, 0, inf((𝑍‘(𝐴𝑛)), ℝ*, < )) = inf((𝑍‘(𝐴𝑛)), ℝ*, < ))
133132adantr 480 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → if(𝑋 = ∅, 0, inf((𝑍‘(𝐴𝑛)), ℝ*, < )) = inf((𝑍‘(𝐴𝑛)), ℝ*, < ))
134129, 133eqtrd 2644 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → ((voln*‘𝑋)‘(𝐴𝑛)) = inf((𝑍‘(𝐴𝑛)), ℝ*, < ))
135128a1i 11 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → 𝑍 = (𝑎 ∈ 𝒫 (ℝ ↑𝑚 𝑋) ↦ {𝑧 ∈ ℝ* ∣ ∃𝑖 ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)(𝑎 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑖𝑗))‘𝑘) ∧ 𝑧 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘𝑋 (vol‘(([,) ∘ (𝑖𝑗))‘𝑘)))))}))
136 sseq1 3589 . . . . . . . . . . . . . 14 (𝑎 = (𝐴𝑛) → (𝑎 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑖𝑗))‘𝑘) ↔ (𝐴𝑛) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑖𝑗))‘𝑘)))
137136anbi1d 737 . . . . . . . . . . . . 13 (𝑎 = (𝐴𝑛) → ((𝑎 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑖𝑗))‘𝑘) ∧ 𝑧 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘𝑋 (vol‘(([,) ∘ (𝑖𝑗))‘𝑘))))) ↔ ((𝐴𝑛) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑖𝑗))‘𝑘) ∧ 𝑧 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘𝑋 (vol‘(([,) ∘ (𝑖𝑗))‘𝑘)))))))
138137rexbidv 3034 . . . . . . . . . . . 12 (𝑎 = (𝐴𝑛) → (∃𝑖 ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)(𝑎 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑖𝑗))‘𝑘) ∧ 𝑧 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘𝑋 (vol‘(([,) ∘ (𝑖𝑗))‘𝑘))))) ↔ ∃𝑖 ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)((𝐴𝑛) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑖𝑗))‘𝑘) ∧ 𝑧 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘𝑋 (vol‘(([,) ∘ (𝑖𝑗))‘𝑘)))))))
139138rabbidv 3164 . . . . . . . . . . 11 (𝑎 = (𝐴𝑛) → {𝑧 ∈ ℝ* ∣ ∃𝑖 ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)(𝑎 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑖𝑗))‘𝑘) ∧ 𝑧 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘𝑋 (vol‘(([,) ∘ (𝑖𝑗))‘𝑘)))))} = {𝑧 ∈ ℝ* ∣ ∃𝑖 ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)((𝐴𝑛) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑖𝑗))‘𝑘) ∧ 𝑧 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘𝑋 (vol‘(([,) ∘ (𝑖𝑗))‘𝑘)))))})
140139adantl 481 . . . . . . . . . 10 (((𝜑𝑛 ∈ ℕ) ∧ 𝑎 = (𝐴𝑛)) → {𝑧 ∈ ℝ* ∣ ∃𝑖 ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)(𝑎 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑖𝑗))‘𝑘) ∧ 𝑧 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘𝑋 (vol‘(([,) ∘ (𝑖𝑗))‘𝑘)))))} = {𝑧 ∈ ℝ* ∣ ∃𝑖 ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)((𝐴𝑛) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑖𝑗))‘𝑘) ∧ 𝑧 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘𝑋 (vol‘(([,) ∘ (𝑖𝑗))‘𝑘)))))})
141 xrex 11705 . . . . . . . . . . . 12 * ∈ V
142141rabex 4740 . . . . . . . . . . 11 {𝑧 ∈ ℝ* ∣ ∃𝑖 ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)((𝐴𝑛) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑖𝑗))‘𝑘) ∧ 𝑧 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘𝑋 (vol‘(([,) ∘ (𝑖𝑗))‘𝑘)))))} ∈ V
143142a1i 11 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → {𝑧 ∈ ℝ* ∣ ∃𝑖 ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)((𝐴𝑛) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑖𝑗))‘𝑘) ∧ 𝑧 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘𝑋 (vol‘(([,) ∘ (𝑖𝑗))‘𝑘)))))} ∈ V)
144135, 140, 5, 143fvmptd 6197 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → (𝑍‘(𝐴𝑛)) = {𝑧 ∈ ℝ* ∣ ∃𝑖 ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)((𝐴𝑛) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑖𝑗))‘𝑘) ∧ 𝑧 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘𝑋 (vol‘(([,) ∘ (𝑖𝑗))‘𝑘)))))})
145 ssrab2 3650 . . . . . . . . . 10 {𝑧 ∈ ℝ* ∣ ∃𝑖 ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)((𝐴𝑛) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑖𝑗))‘𝑘) ∧ 𝑧 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘𝑋 (vol‘(([,) ∘ (𝑖𝑗))‘𝑘)))))} ⊆ ℝ*
146145a1i 11 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → {𝑧 ∈ ℝ* ∣ ∃𝑖 ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)((𝐴𝑛) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑖𝑗))‘𝑘) ∧ 𝑧 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘𝑋 (vol‘(([,) ∘ (𝑖𝑗))‘𝑘)))))} ⊆ ℝ*)
147144, 146eqsstrd 3602 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → (𝑍‘(𝐴𝑛)) ⊆ ℝ*)
148 infxrcl 12035 . . . . . . . 8 ((𝑍‘(𝐴𝑛)) ⊆ ℝ* → inf((𝑍‘(𝐴𝑛)), ℝ*, < ) ∈ ℝ*)
149147, 148syl 17 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → inf((𝑍‘(𝐴𝑛)), ℝ*, < ) ∈ ℝ*)
150134, 149eqeltrd 2688 . . . . . 6 ((𝜑𝑛 ∈ ℕ) → ((voln*‘𝑋)‘(𝐴𝑛)) ∈ ℝ*)
15174rpred 11748 . . . . . . . . 9 (𝜑𝐸 ∈ ℝ)
152151adantr 480 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → 𝐸 ∈ ℝ)
153 2re 10967 . . . . . . . . . . 11 2 ∈ ℝ
154153a1i 11 . . . . . . . . . 10 (𝑛 ∈ ℕ → 2 ∈ ℝ)
155154, 78reexpcld 12887 . . . . . . . . 9 (𝑛 ∈ ℕ → (2↑𝑛) ∈ ℝ)
156155adantl 481 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → (2↑𝑛) ∈ ℝ)
157154recnd 9947 . . . . . . . . . 10 (𝑛 ∈ ℕ → 2 ∈ ℂ)
158 2ne0 10990 . . . . . . . . . . 11 2 ≠ 0
159158a1i 11 . . . . . . . . . 10 (𝑛 ∈ ℕ → 2 ≠ 0)
160 nnz 11276 . . . . . . . . . 10 (𝑛 ∈ ℕ → 𝑛 ∈ ℤ)
161157, 159, 160expne0d 12876 . . . . . . . . 9 (𝑛 ∈ ℕ → (2↑𝑛) ≠ 0)
162161adantl 481 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → (2↑𝑛) ≠ 0)
163152, 156, 162redivcld 10732 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → (𝐸 / (2↑𝑛)) ∈ ℝ)
164163rexrd 9968 . . . . . 6 ((𝜑𝑛 ∈ ℕ) → (𝐸 / (2↑𝑛)) ∈ ℝ*)
165150, 164xaddcld 12003 . . . . 5 ((𝜑𝑛 ∈ ℕ) → (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛))) ∈ ℝ*)
166127, 7ovncl 39457 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → ((voln*‘𝑋)‘(𝐴𝑛)) ∈ (0[,]+∞))
167 xrge0ge0 38504 . . . . . . 7 (((voln*‘𝑋)‘(𝐴𝑛)) ∈ (0[,]+∞) → 0 ≤ ((voln*‘𝑋)‘(𝐴𝑛)))
168166, 167syl 17 . . . . . 6 ((𝜑𝑛 ∈ ℕ) → 0 ≤ ((voln*‘𝑋)‘(𝐴𝑛)))
169 0red 9920 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → 0 ∈ ℝ)
17082rpgt0d 11751 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → 0 < (𝐸 / (2↑𝑛)))
171169, 163, 170ltled 10064 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → 0 ≤ (𝐸 / (2↑𝑛)))
172163ltpnfd 11831 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → (𝐸 / (2↑𝑛)) < +∞)
173164, 126, 172xrltled 38427 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → (𝐸 / (2↑𝑛)) ≤ +∞)
174124, 126, 164, 171, 173eliccxrd 38600 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → (𝐸 / (2↑𝑛)) ∈ (0[,]+∞))
175150, 174xadd0ge 38477 . . . . . 6 ((𝜑𝑛 ∈ ℕ) → ((voln*‘𝑋)‘(𝐴𝑛)) ≤ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛))))
176124, 150, 165, 168, 175xrletrd 11869 . . . . 5 ((𝜑𝑛 ∈ ℕ) → 0 ≤ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛))))
177 pnfge 11840 . . . . . 6 ((((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛))) ∈ ℝ* → (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛))) ≤ +∞)
178165, 177syl 17 . . . . 5 ((𝜑𝑛 ∈ ℕ) → (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛))) ≤ +∞)
179124, 126, 165, 176, 178eliccxrd 38600 . . . 4 ((𝜑𝑛 ∈ ℕ) → (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛))) ∈ (0[,]+∞))
180122, 14, 179sge0xrclmpt 39321 . . 3 (𝜑 → (Σ^‘(𝑛 ∈ ℕ ↦ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛))))) ∈ ℝ*)
18143a1i 11 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ ℕ) → 𝐶 = (𝑎 ∈ 𝒫 (ℝ ↑𝑚 𝑋) ↦ { ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∣ 𝑎 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘)}))
182 sseq1 3589 . . . . . . . . . . . . . 14 (𝑎 = (𝐴‘(1st ‘(𝐹𝑚))) → (𝑎 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘) ↔ (𝐴‘(1st ‘(𝐹𝑚))) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘)))
183182rabbidv 3164 . . . . . . . . . . . . 13 (𝑎 = (𝐴‘(1st ‘(𝐹𝑚))) → { ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∣ 𝑎 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘)} = { ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∣ (𝐴‘(1st ‘(𝐹𝑚))) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘)})
184183adantl 481 . . . . . . . . . . . 12 (((𝜑𝑚 ∈ ℕ) ∧ 𝑎 = (𝐴‘(1st ‘(𝐹𝑚)))) → { ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∣ 𝑎 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘)} = { ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∣ (𝐴‘(1st ‘(𝐹𝑚))) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘)})
1852adantr 480 . . . . . . . . . . . . 13 ((𝜑𝑚 ∈ ℕ) → 𝐴:ℕ⟶𝒫 (ℝ ↑𝑚 𝑋))
186185, 27ffvelrnd 6268 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ ℕ) → (𝐴‘(1st ‘(𝐹𝑚))) ∈ 𝒫 (ℝ ↑𝑚 𝑋))
18748rabex 4740 . . . . . . . . . . . . 13 { ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∣ (𝐴‘(1st ‘(𝐹𝑚))) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘)} ∈ V
188187a1i 11 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ ℕ) → { ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∣ (𝐴‘(1st ‘(𝐹𝑚))) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘)} ∈ V)
189181, 184, 186, 188fvmptd 6197 . . . . . . . . . . 11 ((𝜑𝑚 ∈ ℕ) → (𝐶‘(𝐴‘(1st ‘(𝐹𝑚)))) = { ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∣ (𝐴‘(1st ‘(𝐹𝑚))) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘)})
190 ssrab2 3650 . . . . . . . . . . . 12 { ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∣ (𝐴‘(1st ‘(𝐹𝑚))) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘)} ⊆ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)
191190a1i 11 . . . . . . . . . . 11 ((𝜑𝑚 ∈ ℕ) → { ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∣ (𝐴‘(1st ‘(𝐹𝑚))) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘)} ⊆ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ))
192189, 191eqsstrd 3602 . . . . . . . . . 10 ((𝜑𝑚 ∈ ℕ) → (𝐶‘(𝐴‘(1st ‘(𝐹𝑚)))) ⊆ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ))
19355a1i 11 . . . . . . . . . . . . . 14 ((𝜑𝑚 ∈ ℕ) → 𝐷 = (𝑎 ∈ 𝒫 (ℝ ↑𝑚 𝑋) ↦ (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶𝑎) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘𝑎) +𝑒 𝑒)})))
194 fveq2 6103 . . . . . . . . . . . . . . . . . . 19 (𝑎 = (𝐴‘(1st ‘(𝐹𝑚))) → (𝐶𝑎) = (𝐶‘(𝐴‘(1st ‘(𝐹𝑚)))))
195194eleq2d 2673 . . . . . . . . . . . . . . . . . 18 (𝑎 = (𝐴‘(1st ‘(𝐹𝑚))) → (𝑖 ∈ (𝐶𝑎) ↔ 𝑖 ∈ (𝐶‘(𝐴‘(1st ‘(𝐹𝑚))))))
196 fveq2 6103 . . . . . . . . . . . . . . . . . . . 20 (𝑎 = (𝐴‘(1st ‘(𝐹𝑚))) → ((voln*‘𝑋)‘𝑎) = ((voln*‘𝑋)‘(𝐴‘(1st ‘(𝐹𝑚)))))
197196oveq1d 6564 . . . . . . . . . . . . . . . . . . 19 (𝑎 = (𝐴‘(1st ‘(𝐹𝑚))) → (((voln*‘𝑋)‘𝑎) +𝑒 𝑒) = (((voln*‘𝑋)‘(𝐴‘(1st ‘(𝐹𝑚)))) +𝑒 𝑒))
198197breq2d 4595 . . . . . . . . . . . . . . . . . 18 (𝑎 = (𝐴‘(1st ‘(𝐹𝑚))) → ((Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘𝑎) +𝑒 𝑒) ↔ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴‘(1st ‘(𝐹𝑚)))) +𝑒 𝑒)))
199195, 198anbi12d 743 . . . . . . . . . . . . . . . . 17 (𝑎 = (𝐴‘(1st ‘(𝐹𝑚))) → ((𝑖 ∈ (𝐶𝑎) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘𝑎) +𝑒 𝑒)) ↔ (𝑖 ∈ (𝐶‘(𝐴‘(1st ‘(𝐹𝑚)))) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴‘(1st ‘(𝐹𝑚)))) +𝑒 𝑒))))
200199rabbidva2 3162 . . . . . . . . . . . . . . . 16 (𝑎 = (𝐴‘(1st ‘(𝐹𝑚))) → {𝑖 ∈ (𝐶𝑎) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘𝑎) +𝑒 𝑒)} = {𝑖 ∈ (𝐶‘(𝐴‘(1st ‘(𝐹𝑚)))) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴‘(1st ‘(𝐹𝑚)))) +𝑒 𝑒)})
201200mpteq2dv 4673 . . . . . . . . . . . . . . 15 (𝑎 = (𝐴‘(1st ‘(𝐹𝑚))) → (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶𝑎) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘𝑎) +𝑒 𝑒)}) = (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶‘(𝐴‘(1st ‘(𝐹𝑚)))) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴‘(1st ‘(𝐹𝑚)))) +𝑒 𝑒)}))
202201adantl 481 . . . . . . . . . . . . . 14 (((𝜑𝑚 ∈ ℕ) ∧ 𝑎 = (𝐴‘(1st ‘(𝐹𝑚)))) → (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶𝑎) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘𝑎) +𝑒 𝑒)}) = (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶‘(𝐴‘(1st ‘(𝐹𝑚)))) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴‘(1st ‘(𝐹𝑚)))) +𝑒 𝑒)}))
20366mptex 6390 . . . . . . . . . . . . . . 15 (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶‘(𝐴‘(1st ‘(𝐹𝑚)))) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴‘(1st ‘(𝐹𝑚)))) +𝑒 𝑒)}) ∈ V
204203a1i 11 . . . . . . . . . . . . . 14 ((𝜑𝑚 ∈ ℕ) → (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶‘(𝐴‘(1st ‘(𝐹𝑚)))) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴‘(1st ‘(𝐹𝑚)))) +𝑒 𝑒)}) ∈ V)
205193, 202, 186, 204fvmptd 6197 . . . . . . . . . . . . 13 ((𝜑𝑚 ∈ ℕ) → (𝐷‘(𝐴‘(1st ‘(𝐹𝑚)))) = (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶‘(𝐴‘(1st ‘(𝐹𝑚)))) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴‘(1st ‘(𝐹𝑚)))) +𝑒 𝑒)}))
206 oveq2 6557 . . . . . . . . . . . . . . . 16 (𝑒 = (𝐸 / (2↑(1st ‘(𝐹𝑚)))) → (((voln*‘𝑋)‘(𝐴‘(1st ‘(𝐹𝑚)))) +𝑒 𝑒) = (((voln*‘𝑋)‘(𝐴‘(1st ‘(𝐹𝑚)))) +𝑒 (𝐸 / (2↑(1st ‘(𝐹𝑚))))))
207206breq2d 4595 . . . . . . . . . . . . . . 15 (𝑒 = (𝐸 / (2↑(1st ‘(𝐹𝑚)))) → ((Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴‘(1st ‘(𝐹𝑚)))) +𝑒 𝑒) ↔ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴‘(1st ‘(𝐹𝑚)))) +𝑒 (𝐸 / (2↑(1st ‘(𝐹𝑚)))))))
208207rabbidv 3164 . . . . . . . . . . . . . 14 (𝑒 = (𝐸 / (2↑(1st ‘(𝐹𝑚)))) → {𝑖 ∈ (𝐶‘(𝐴‘(1st ‘(𝐹𝑚)))) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴‘(1st ‘(𝐹𝑚)))) +𝑒 𝑒)} = {𝑖 ∈ (𝐶‘(𝐴‘(1st ‘(𝐹𝑚)))) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴‘(1st ‘(𝐹𝑚)))) +𝑒 (𝐸 / (2↑(1st ‘(𝐹𝑚)))))})
209208adantl 481 . . . . . . . . . . . . 13 (((𝜑𝑚 ∈ ℕ) ∧ 𝑒 = (𝐸 / (2↑(1st ‘(𝐹𝑚))))) → {𝑖 ∈ (𝐶‘(𝐴‘(1st ‘(𝐹𝑚)))) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴‘(1st ‘(𝐹𝑚)))) +𝑒 𝑒)} = {𝑖 ∈ (𝐶‘(𝐴‘(1st ‘(𝐹𝑚)))) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴‘(1st ‘(𝐹𝑚)))) +𝑒 (𝐸 / (2↑(1st ‘(𝐹𝑚)))))})
21017, 74syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑚 ∈ ℕ) → 𝐸 ∈ ℝ+)
211 2rp 11713 . . . . . . . . . . . . . . . 16 2 ∈ ℝ+
212211a1i 11 . . . . . . . . . . . . . . 15 ((𝜑𝑚 ∈ ℕ) → 2 ∈ ℝ+)
21327nnzd 11357 . . . . . . . . . . . . . . 15 ((𝜑𝑚 ∈ ℕ) → (1st ‘(𝐹𝑚)) ∈ ℤ)
214212, 213rpexpcld 12894 . . . . . . . . . . . . . 14 ((𝜑𝑚 ∈ ℕ) → (2↑(1st ‘(𝐹𝑚))) ∈ ℝ+)
215210, 214rpdivcld 11765 . . . . . . . . . . . . 13 ((𝜑𝑚 ∈ ℕ) → (𝐸 / (2↑(1st ‘(𝐹𝑚)))) ∈ ℝ+)
216 fvex 6113 . . . . . . . . . . . . . . 15 (𝐶‘(𝐴‘(1st ‘(𝐹𝑚)))) ∈ V
217216rabex 4740 . . . . . . . . . . . . . 14 {𝑖 ∈ (𝐶‘(𝐴‘(1st ‘(𝐹𝑚)))) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴‘(1st ‘(𝐹𝑚)))) +𝑒 (𝐸 / (2↑(1st ‘(𝐹𝑚)))))} ∈ V
218217a1i 11 . . . . . . . . . . . . 13 ((𝜑𝑚 ∈ ℕ) → {𝑖 ∈ (𝐶‘(𝐴‘(1st ‘(𝐹𝑚)))) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴‘(1st ‘(𝐹𝑚)))) +𝑒 (𝐸 / (2↑(1st ‘(𝐹𝑚)))))} ∈ V)
219205, 209, 215, 218fvmptd 6197 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ ℕ) → ((𝐷‘(𝐴‘(1st ‘(𝐹𝑚))))‘(𝐸 / (2↑(1st ‘(𝐹𝑚))))) = {𝑖 ∈ (𝐶‘(𝐴‘(1st ‘(𝐹𝑚)))) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴‘(1st ‘(𝐹𝑚)))) +𝑒 (𝐸 / (2↑(1st ‘(𝐹𝑚)))))})
220 ssrab2 3650 . . . . . . . . . . . . 13 {𝑖 ∈ (𝐶‘(𝐴‘(1st ‘(𝐹𝑚)))) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴‘(1st ‘(𝐹𝑚)))) +𝑒 (𝐸 / (2↑(1st ‘(𝐹𝑚)))))} ⊆ (𝐶‘(𝐴‘(1st ‘(𝐹𝑚))))
221220a1i 11 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ ℕ) → {𝑖 ∈ (𝐶‘(𝐴‘(1st ‘(𝐹𝑚)))) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴‘(1st ‘(𝐹𝑚)))) +𝑒 (𝐸 / (2↑(1st ‘(𝐹𝑚)))))} ⊆ (𝐶‘(𝐴‘(1st ‘(𝐹𝑚)))))
222219, 221eqsstrd 3602 . . . . . . . . . . 11 ((𝜑𝑚 ∈ ℕ) → ((𝐷‘(𝐴‘(1st ‘(𝐹𝑚))))‘(𝐸 / (2↑(1st ‘(𝐹𝑚))))) ⊆ (𝐶‘(𝐴‘(1st ‘(𝐹𝑚)))))
22337anbi2d 736 . . . . . . . . . . . . . 14 (𝑛 = (1st ‘(𝐹𝑚)) → ((𝜑𝑛 ∈ ℕ) ↔ (𝜑 ∧ (1st ‘(𝐹𝑚)) ∈ ℕ)))
224 fveq2 6103 . . . . . . . . . . . . . . . . 17 (𝑛 = (1st ‘(𝐹𝑚)) → (𝐴𝑛) = (𝐴‘(1st ‘(𝐹𝑚))))
225224fveq2d 6107 . . . . . . . . . . . . . . . 16 (𝑛 = (1st ‘(𝐹𝑚)) → (𝐷‘(𝐴𝑛)) = (𝐷‘(𝐴‘(1st ‘(𝐹𝑚)))))
226 oveq2 6557 . . . . . . . . . . . . . . . . 17 (𝑛 = (1st ‘(𝐹𝑚)) → (2↑𝑛) = (2↑(1st ‘(𝐹𝑚))))
227226oveq2d 6565 . . . . . . . . . . . . . . . 16 (𝑛 = (1st ‘(𝐹𝑚)) → (𝐸 / (2↑𝑛)) = (𝐸 / (2↑(1st ‘(𝐹𝑚)))))
228225, 227fveq12d 6109 . . . . . . . . . . . . . . 15 (𝑛 = (1st ‘(𝐹𝑚)) → ((𝐷‘(𝐴𝑛))‘(𝐸 / (2↑𝑛))) = ((𝐷‘(𝐴‘(1st ‘(𝐹𝑚))))‘(𝐸 / (2↑(1st ‘(𝐹𝑚))))))
22939, 228eleq12d 2682 . . . . . . . . . . . . . 14 (𝑛 = (1st ‘(𝐹𝑚)) → ((𝐼𝑛) ∈ ((𝐷‘(𝐴𝑛))‘(𝐸 / (2↑𝑛))) ↔ (𝐼‘(1st ‘(𝐹𝑚))) ∈ ((𝐷‘(𝐴‘(1st ‘(𝐹𝑚))))‘(𝐸 / (2↑(1st ‘(𝐹𝑚)))))))
230223, 229imbi12d 333 . . . . . . . . . . . . 13 (𝑛 = (1st ‘(𝐹𝑚)) → (((𝜑𝑛 ∈ ℕ) → (𝐼𝑛) ∈ ((𝐷‘(𝐴𝑛))‘(𝐸 / (2↑𝑛)))) ↔ ((𝜑 ∧ (1st ‘(𝐹𝑚)) ∈ ℕ) → (𝐼‘(1st ‘(𝐹𝑚))) ∈ ((𝐷‘(𝐴‘(1st ‘(𝐹𝑚))))‘(𝐸 / (2↑(1st ‘(𝐹𝑚))))))))
23136, 230, 90vtocl 3232 . . . . . . . . . . . 12 ((𝜑 ∧ (1st ‘(𝐹𝑚)) ∈ ℕ) → (𝐼‘(1st ‘(𝐹𝑚))) ∈ ((𝐷‘(𝐴‘(1st ‘(𝐹𝑚))))‘(𝐸 / (2↑(1st ‘(𝐹𝑚))))))
23217, 27, 231syl2anc 691 . . . . . . . . . . 11 ((𝜑𝑚 ∈ ℕ) → (𝐼‘(1st ‘(𝐹𝑚))) ∈ ((𝐷‘(𝐴‘(1st ‘(𝐹𝑚))))‘(𝐸 / (2↑(1st ‘(𝐹𝑚))))))
233222, 232sseldd 3569 . . . . . . . . . 10 ((𝜑𝑚 ∈ ℕ) → (𝐼‘(1st ‘(𝐹𝑚))) ∈ (𝐶‘(𝐴‘(1st ‘(𝐹𝑚)))))
234192, 233sseldd 3569 . . . . . . . . 9 ((𝜑𝑚 ∈ ℕ) → (𝐼‘(1st ‘(𝐹𝑚))) ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ))
235 elmapfn 7766 . . . . . . . . 9 ((𝐼‘(1st ‘(𝐹𝑚))) ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) → (𝐼‘(1st ‘(𝐹𝑚))) Fn ℕ)
236234, 235syl 17 . . . . . . . 8 ((𝜑𝑚 ∈ ℕ) → (𝐼‘(1st ‘(𝐹𝑚))) Fn ℕ)
237 elmapi 7765 . . . . . . . . . . 11 ((𝐼‘(1st ‘(𝐹𝑚))) ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) → (𝐼‘(1st ‘(𝐹𝑚))):ℕ⟶((ℝ × ℝ) ↑𝑚 𝑋))
238234, 237syl 17 . . . . . . . . . 10 ((𝜑𝑚 ∈ ℕ) → (𝐼‘(1st ‘(𝐹𝑚))):ℕ⟶((ℝ × ℝ) ↑𝑚 𝑋))
239238ffvelrnda 6267 . . . . . . . . 9 (((𝜑𝑚 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → ((𝐼‘(1st ‘(𝐹𝑚)))‘𝑗) ∈ ((ℝ × ℝ) ↑𝑚 𝑋))
240239ralrimiva 2949 . . . . . . . 8 ((𝜑𝑚 ∈ ℕ) → ∀𝑗 ∈ ℕ ((𝐼‘(1st ‘(𝐹𝑚)))‘𝑗) ∈ ((ℝ × ℝ) ↑𝑚 𝑋))
241236, 240jca 553 . . . . . . 7 ((𝜑𝑚 ∈ ℕ) → ((𝐼‘(1st ‘(𝐹𝑚))) Fn ℕ ∧ ∀𝑗 ∈ ℕ ((𝐼‘(1st ‘(𝐹𝑚)))‘𝑗) ∈ ((ℝ × ℝ) ↑𝑚 𝑋)))
242 ffnfv 6295 . . . . . . 7 ((𝐼‘(1st ‘(𝐹𝑚))):ℕ⟶((ℝ × ℝ) ↑𝑚 𝑋) ↔ ((𝐼‘(1st ‘(𝐹𝑚))) Fn ℕ ∧ ∀𝑗 ∈ ℕ ((𝐼‘(1st ‘(𝐹𝑚)))‘𝑗) ∈ ((ℝ × ℝ) ↑𝑚 𝑋)))
243241, 242sylibr 223 . . . . . 6 ((𝜑𝑚 ∈ ℕ) → (𝐼‘(1st ‘(𝐹𝑚))):ℕ⟶((ℝ × ℝ) ↑𝑚 𝑋))
244243, 29ffvelrnd 6268 . . . . 5 ((𝜑𝑚 ∈ ℕ) → ((𝐼‘(1st ‘(𝐹𝑚)))‘(2nd ‘(𝐹𝑚))) ∈ ((ℝ × ℝ) ↑𝑚 𝑋))
245244, 113fmptd 6292 . . . 4 (𝜑𝐺:ℕ⟶((ℝ × ℝ) ↑𝑚 𝑋))
246 simpl 472 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → 𝜑)
24790, 86eleqtrd 2690 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → (𝐼𝑛) ∈ {𝑖 ∈ (𝐶‘(𝐴𝑛)) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛)))})
24887, 247sseldi 3566 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → (𝐼𝑛) ∈ (𝐶‘(𝐴𝑛)))
249 simp3 1056 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ ∧ (𝐼𝑛) ∈ (𝐶‘(𝐴𝑛))) → (𝐼𝑛) ∈ (𝐶‘(𝐴𝑛)))
250513adant3 1074 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ ∧ (𝐼𝑛) ∈ (𝐶‘(𝐴𝑛))) → (𝐶‘(𝐴𝑛)) = { ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∣ (𝐴𝑛) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘)})
251249, 250eleqtrd 2690 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ ∧ (𝐼𝑛) ∈ (𝐶‘(𝐴𝑛))) → (𝐼𝑛) ∈ { ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∣ (𝐴𝑛) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘)})
252 fveq1 6102 . . . . . . . . . . . . . . . . 17 ( = (𝐼𝑛) → (𝑗) = ((𝐼𝑛)‘𝑗))
253252coeq2d 5206 . . . . . . . . . . . . . . . 16 ( = (𝐼𝑛) → ([,) ∘ (𝑗)) = ([,) ∘ ((𝐼𝑛)‘𝑗)))
254253fveq1d 6105 . . . . . . . . . . . . . . 15 ( = (𝐼𝑛) → (([,) ∘ (𝑗))‘𝑘) = (([,) ∘ ((𝐼𝑛)‘𝑗))‘𝑘))
255254ixpeq2dv 7810 . . . . . . . . . . . . . 14 ( = (𝐼𝑛) → X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘) = X𝑘𝑋 (([,) ∘ ((𝐼𝑛)‘𝑗))‘𝑘))
256255iuneq2d 4483 . . . . . . . . . . . . 13 ( = (𝐼𝑛) → 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘) = 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ ((𝐼𝑛)‘𝑗))‘𝑘))
257256sseq2d 3596 . . . . . . . . . . . 12 ( = (𝐼𝑛) → ((𝐴𝑛) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘) ↔ (𝐴𝑛) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ ((𝐼𝑛)‘𝑗))‘𝑘)))
258257elrab 3331 . . . . . . . . . . 11 ((𝐼𝑛) ∈ { ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∣ (𝐴𝑛) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘)} ↔ ((𝐼𝑛) ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∧ (𝐴𝑛) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ ((𝐼𝑛)‘𝑗))‘𝑘)))
259251, 258sylib 207 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ ∧ (𝐼𝑛) ∈ (𝐶‘(𝐴𝑛))) → ((𝐼𝑛) ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∧ (𝐴𝑛) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ ((𝐼𝑛)‘𝑗))‘𝑘)))
260259simprd 478 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ ∧ (𝐼𝑛) ∈ (𝐶‘(𝐴𝑛))) → (𝐴𝑛) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ ((𝐼𝑛)‘𝑗))‘𝑘))
261246, 4, 248, 260syl3anc 1318 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → (𝐴𝑛) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ ((𝐼𝑛)‘𝑗))‘𝑘))
262 f1ofo 6057 . . . . . . . . . . . . . 14 (𝐹:ℕ–1-1-onto→(ℕ × ℕ) → 𝐹:ℕ–onto→(ℕ × ℕ))
26320, 262syl 17 . . . . . . . . . . . . 13 (𝜑𝐹:ℕ–onto→(ℕ × ℕ))
264263ad2antrr 758 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → 𝐹:ℕ–onto→(ℕ × ℕ))
265 opelxpi 5072 . . . . . . . . . . . . 13 ((𝑛 ∈ ℕ ∧ 𝑗 ∈ ℕ) → ⟨𝑛, 𝑗⟩ ∈ (ℕ × ℕ))
2664, 265sylan 487 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → ⟨𝑛, 𝑗⟩ ∈ (ℕ × ℕ))
267 foelrni 6154 . . . . . . . . . . . 12 ((𝐹:ℕ–onto→(ℕ × ℕ) ∧ ⟨𝑛, 𝑗⟩ ∈ (ℕ × ℕ)) → ∃𝑚 ∈ ℕ (𝐹𝑚) = ⟨𝑛, 𝑗⟩)
268264, 266, 267syl2anc 691 . . . . . . . . . . 11 (((𝜑𝑛 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → ∃𝑚 ∈ ℕ (𝐹𝑚) = ⟨𝑛, 𝑗⟩)
269 nfv 1830 . . . . . . . . . . . 12 𝑚((𝜑𝑛 ∈ ℕ) ∧ 𝑗 ∈ ℕ)
270 nfre1 2988 . . . . . . . . . . . 12 𝑚𝑚 ∈ {𝑖 ∈ ℕ ∣ (1st ‘(𝐹𝑖)) = 𝑛}X𝑘𝑋 (([,) ∘ ((𝐼𝑛)‘𝑗))‘𝑘) ⊆ X𝑘𝑋 (([,) ∘ (𝐺𝑚))‘𝑘)
271 simpl 472 . . . . . . . . . . . . . . . . 17 ((𝑚 ∈ ℕ ∧ (𝐹𝑚) = ⟨𝑛, 𝑗⟩) → 𝑚 ∈ ℕ)
272 fveq2 6103 . . . . . . . . . . . . . . . . . . 19 ((𝐹𝑚) = ⟨𝑛, 𝑗⟩ → (1st ‘(𝐹𝑚)) = (1st ‘⟨𝑛, 𝑗⟩))
273 vex 3176 . . . . . . . . . . . . . . . . . . . . 21 𝑛 ∈ V
274 vex 3176 . . . . . . . . . . . . . . . . . . . . 21 𝑗 ∈ V
275 op1stg 7071 . . . . . . . . . . . . . . . . . . . . 21 ((𝑛 ∈ V ∧ 𝑗 ∈ V) → (1st ‘⟨𝑛, 𝑗⟩) = 𝑛)
276273, 274, 275mp2an 704 . . . . . . . . . . . . . . . . . . . 20 (1st ‘⟨𝑛, 𝑗⟩) = 𝑛
277276a1i 11 . . . . . . . . . . . . . . . . . . 19 ((𝐹𝑚) = ⟨𝑛, 𝑗⟩ → (1st ‘⟨𝑛, 𝑗⟩) = 𝑛)
278272, 277eqtrd 2644 . . . . . . . . . . . . . . . . . 18 ((𝐹𝑚) = ⟨𝑛, 𝑗⟩ → (1st ‘(𝐹𝑚)) = 𝑛)
279278adantl 481 . . . . . . . . . . . . . . . . 17 ((𝑚 ∈ ℕ ∧ (𝐹𝑚) = ⟨𝑛, 𝑗⟩) → (1st ‘(𝐹𝑚)) = 𝑛)
280271, 279jca 553 . . . . . . . . . . . . . . . 16 ((𝑚 ∈ ℕ ∧ (𝐹𝑚) = ⟨𝑛, 𝑗⟩) → (𝑚 ∈ ℕ ∧ (1st ‘(𝐹𝑚)) = 𝑛))
281 fveq2 6103 . . . . . . . . . . . . . . . . . . 19 (𝑖 = 𝑚 → (𝐹𝑖) = (𝐹𝑚))
282281fveq2d 6107 . . . . . . . . . . . . . . . . . 18 (𝑖 = 𝑚 → (1st ‘(𝐹𝑖)) = (1st ‘(𝐹𝑚)))
283282eqeq1d 2612 . . . . . . . . . . . . . . . . 17 (𝑖 = 𝑚 → ((1st ‘(𝐹𝑖)) = 𝑛 ↔ (1st ‘(𝐹𝑚)) = 𝑛))
284283elrab 3331 . . . . . . . . . . . . . . . 16 (𝑚 ∈ {𝑖 ∈ ℕ ∣ (1st ‘(𝐹𝑖)) = 𝑛} ↔ (𝑚 ∈ ℕ ∧ (1st ‘(𝐹𝑚)) = 𝑛))
285280, 284sylibr 223 . . . . . . . . . . . . . . 15 ((𝑚 ∈ ℕ ∧ (𝐹𝑚) = ⟨𝑛, 𝑗⟩) → 𝑚 ∈ {𝑖 ∈ ℕ ∣ (1st ‘(𝐹𝑖)) = 𝑛})
2862853adant1 1072 . . . . . . . . . . . . . 14 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑗 ∈ ℕ) ∧ 𝑚 ∈ ℕ ∧ (𝐹𝑚) = ⟨𝑛, 𝑗⟩) → 𝑚 ∈ {𝑖 ∈ ℕ ∣ (1st ‘(𝐹𝑖)) = 𝑛})
287271, 115syl 17 . . . . . . . . . . . . . . . . . . . 20 ((𝑚 ∈ ℕ ∧ (𝐹𝑚) = ⟨𝑛, 𝑗⟩) → (𝐺𝑚) = ((𝐼‘(1st ‘(𝐹𝑚)))‘(2nd ‘(𝐹𝑚))))
288278fveq2d 6107 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐹𝑚) = ⟨𝑛, 𝑗⟩ → (𝐼‘(1st ‘(𝐹𝑚))) = (𝐼𝑛))
289273, 274op2ndd 7070 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐹𝑚) = ⟨𝑛, 𝑗⟩ → (2nd ‘(𝐹𝑚)) = 𝑗)
290288, 289fveq12d 6109 . . . . . . . . . . . . . . . . . . . . 21 ((𝐹𝑚) = ⟨𝑛, 𝑗⟩ → ((𝐼‘(1st ‘(𝐹𝑚)))‘(2nd ‘(𝐹𝑚))) = ((𝐼𝑛)‘𝑗))
291290adantl 481 . . . . . . . . . . . . . . . . . . . 20 ((𝑚 ∈ ℕ ∧ (𝐹𝑚) = ⟨𝑛, 𝑗⟩) → ((𝐼‘(1st ‘(𝐹𝑚)))‘(2nd ‘(𝐹𝑚))) = ((𝐼𝑛)‘𝑗))
292287, 291eqtr2d 2645 . . . . . . . . . . . . . . . . . . 19 ((𝑚 ∈ ℕ ∧ (𝐹𝑚) = ⟨𝑛, 𝑗⟩) → ((𝐼𝑛)‘𝑗) = (𝐺𝑚))
293292coeq2d 5206 . . . . . . . . . . . . . . . . . 18 ((𝑚 ∈ ℕ ∧ (𝐹𝑚) = ⟨𝑛, 𝑗⟩) → ([,) ∘ ((𝐼𝑛)‘𝑗)) = ([,) ∘ (𝐺𝑚)))
294293fveq1d 6105 . . . . . . . . . . . . . . . . 17 ((𝑚 ∈ ℕ ∧ (𝐹𝑚) = ⟨𝑛, 𝑗⟩) → (([,) ∘ ((𝐼𝑛)‘𝑗))‘𝑘) = (([,) ∘ (𝐺𝑚))‘𝑘))
295294ixpeq2dv 7810 . . . . . . . . . . . . . . . 16 ((𝑚 ∈ ℕ ∧ (𝐹𝑚) = ⟨𝑛, 𝑗⟩) → X𝑘𝑋 (([,) ∘ ((𝐼𝑛)‘𝑗))‘𝑘) = X𝑘𝑋 (([,) ∘ (𝐺𝑚))‘𝑘))
296 eqimss 3620 . . . . . . . . . . . . . . . 16 (X𝑘𝑋 (([,) ∘ ((𝐼𝑛)‘𝑗))‘𝑘) = X𝑘𝑋 (([,) ∘ (𝐺𝑚))‘𝑘) → X𝑘𝑋 (([,) ∘ ((𝐼𝑛)‘𝑗))‘𝑘) ⊆ X𝑘𝑋 (([,) ∘ (𝐺𝑚))‘𝑘))
297295, 296syl 17 . . . . . . . . . . . . . . 15 ((𝑚 ∈ ℕ ∧ (𝐹𝑚) = ⟨𝑛, 𝑗⟩) → X𝑘𝑋 (([,) ∘ ((𝐼𝑛)‘𝑗))‘𝑘) ⊆ X𝑘𝑋 (([,) ∘ (𝐺𝑚))‘𝑘))
2982973adant1 1072 . . . . . . . . . . . . . 14 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑗 ∈ ℕ) ∧ 𝑚 ∈ ℕ ∧ (𝐹𝑚) = ⟨𝑛, 𝑗⟩) → X𝑘𝑋 (([,) ∘ ((𝐼𝑛)‘𝑗))‘𝑘) ⊆ X𝑘𝑋 (([,) ∘ (𝐺𝑚))‘𝑘))
299 rspe 2986 . . . . . . . . . . . . . 14 ((𝑚 ∈ {𝑖 ∈ ℕ ∣ (1st ‘(𝐹𝑖)) = 𝑛} ∧ X𝑘𝑋 (([,) ∘ ((𝐼𝑛)‘𝑗))‘𝑘) ⊆ X𝑘𝑋 (([,) ∘ (𝐺𝑚))‘𝑘)) → ∃𝑚 ∈ {𝑖 ∈ ℕ ∣ (1st ‘(𝐹𝑖)) = 𝑛}X𝑘𝑋 (([,) ∘ ((𝐼𝑛)‘𝑗))‘𝑘) ⊆ X𝑘𝑋 (([,) ∘ (𝐺𝑚))‘𝑘))
300286, 298, 299syl2anc 691 . . . . . . . . . . . . 13 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑗 ∈ ℕ) ∧ 𝑚 ∈ ℕ ∧ (𝐹𝑚) = ⟨𝑛, 𝑗⟩) → ∃𝑚 ∈ {𝑖 ∈ ℕ ∣ (1st ‘(𝐹𝑖)) = 𝑛}X𝑘𝑋 (([,) ∘ ((𝐼𝑛)‘𝑗))‘𝑘) ⊆ X𝑘𝑋 (([,) ∘ (𝐺𝑚))‘𝑘))
3013003exp 1256 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → (𝑚 ∈ ℕ → ((𝐹𝑚) = ⟨𝑛, 𝑗⟩ → ∃𝑚 ∈ {𝑖 ∈ ℕ ∣ (1st ‘(𝐹𝑖)) = 𝑛}X𝑘𝑋 (([,) ∘ ((𝐼𝑛)‘𝑗))‘𝑘) ⊆ X𝑘𝑋 (([,) ∘ (𝐺𝑚))‘𝑘))))
302269, 270, 301rexlimd 3008 . . . . . . . . . . 11 (((𝜑𝑛 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → (∃𝑚 ∈ ℕ (𝐹𝑚) = ⟨𝑛, 𝑗⟩ → ∃𝑚 ∈ {𝑖 ∈ ℕ ∣ (1st ‘(𝐹𝑖)) = 𝑛}X𝑘𝑋 (([,) ∘ ((𝐼𝑛)‘𝑗))‘𝑘) ⊆ X𝑘𝑋 (([,) ∘ (𝐺𝑚))‘𝑘)))
303268, 302mpd 15 . . . . . . . . . 10 (((𝜑𝑛 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → ∃𝑚 ∈ {𝑖 ∈ ℕ ∣ (1st ‘(𝐹𝑖)) = 𝑛}X𝑘𝑋 (([,) ∘ ((𝐼𝑛)‘𝑗))‘𝑘) ⊆ X𝑘𝑋 (([,) ∘ (𝐺𝑚))‘𝑘))
304303ralrimiva 2949 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → ∀𝑗 ∈ ℕ ∃𝑚 ∈ {𝑖 ∈ ℕ ∣ (1st ‘(𝐹𝑖)) = 𝑛}X𝑘𝑋 (([,) ∘ ((𝐼𝑛)‘𝑗))‘𝑘) ⊆ X𝑘𝑋 (([,) ∘ (𝐺𝑚))‘𝑘))
305 iunss2 4501 . . . . . . . . 9 (∀𝑗 ∈ ℕ ∃𝑚 ∈ {𝑖 ∈ ℕ ∣ (1st ‘(𝐹𝑖)) = 𝑛}X𝑘𝑋 (([,) ∘ ((𝐼𝑛)‘𝑗))‘𝑘) ⊆ X𝑘𝑋 (([,) ∘ (𝐺𝑚))‘𝑘) → 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ ((𝐼𝑛)‘𝑗))‘𝑘) ⊆ 𝑚 ∈ {𝑖 ∈ ℕ ∣ (1st ‘(𝐹𝑖)) = 𝑛}X𝑘𝑋 (([,) ∘ (𝐺𝑚))‘𝑘))
306304, 305syl 17 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ ((𝐼𝑛)‘𝑗))‘𝑘) ⊆ 𝑚 ∈ {𝑖 ∈ ℕ ∣ (1st ‘(𝐹𝑖)) = 𝑛}X𝑘𝑋 (([,) ∘ (𝐺𝑚))‘𝑘))
307261, 306sstrd 3578 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → (𝐴𝑛) ⊆ 𝑚 ∈ {𝑖 ∈ ℕ ∣ (1st ‘(𝐹𝑖)) = 𝑛}X𝑘𝑋 (([,) ∘ (𝐺𝑚))‘𝑘))
308 ssrab2 3650 . . . . . . . . 9 {𝑖 ∈ ℕ ∣ (1st ‘(𝐹𝑖)) = 𝑛} ⊆ ℕ
309 iunss1 4468 . . . . . . . . 9 ({𝑖 ∈ ℕ ∣ (1st ‘(𝐹𝑖)) = 𝑛} ⊆ ℕ → 𝑚 ∈ {𝑖 ∈ ℕ ∣ (1st ‘(𝐹𝑖)) = 𝑛}X𝑘𝑋 (([,) ∘ (𝐺𝑚))‘𝑘) ⊆ 𝑚 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝐺𝑚))‘𝑘))
310308, 309ax-mp 5 . . . . . . . 8 𝑚 ∈ {𝑖 ∈ ℕ ∣ (1st ‘(𝐹𝑖)) = 𝑛}X𝑘𝑋 (([,) ∘ (𝐺𝑚))‘𝑘) ⊆ 𝑚 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝐺𝑚))‘𝑘)
311310a1i 11 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → 𝑚 ∈ {𝑖 ∈ ℕ ∣ (1st ‘(𝐹𝑖)) = 𝑛}X𝑘𝑋 (([,) ∘ (𝐺𝑚))‘𝑘) ⊆ 𝑚 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝐺𝑚))‘𝑘))
312307, 311sstrd 3578 . . . . . 6 ((𝜑𝑛 ∈ ℕ) → (𝐴𝑛) ⊆ 𝑚 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝐺𝑚))‘𝑘))
313312ralrimiva 2949 . . . . 5 (𝜑 → ∀𝑛 ∈ ℕ (𝐴𝑛) ⊆ 𝑚 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝐺𝑚))‘𝑘))
314 iunss 4497 . . . . 5 ( 𝑛 ∈ ℕ (𝐴𝑛) ⊆ 𝑚 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝐺𝑚))‘𝑘) ↔ ∀𝑛 ∈ ℕ (𝐴𝑛) ⊆ 𝑚 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝐺𝑚))‘𝑘))
315313, 314sylibr 223 . . . 4 (𝜑 𝑛 ∈ ℕ (𝐴𝑛) ⊆ 𝑚 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝐺𝑚))‘𝑘))
3161, 130, 19, 245, 315ovnlecvr 39448 . . 3 (𝜑 → ((voln*‘𝑋)‘ 𝑛 ∈ ℕ (𝐴𝑛)) ≤ (Σ^‘(𝑚 ∈ ℕ ↦ (𝐿‘(𝐺𝑚)))))
317116fveq2d 6107 . . . . . . 7 ((𝜑𝑚 ∈ ℕ) → (𝐿‘(𝐺𝑚)) = (𝐿‘((𝐼‘(1st ‘(𝐹𝑚)))‘(2nd ‘(𝐹𝑚)))))
318317mpteq2dva 4672 . . . . . 6 (𝜑 → (𝑚 ∈ ℕ ↦ (𝐿‘(𝐺𝑚))) = (𝑚 ∈ ℕ ↦ (𝐿‘((𝐼‘(1st ‘(𝐹𝑚)))‘(2nd ‘(𝐹𝑚))))))
319318fveq2d 6107 . . . . 5 (𝜑 → (Σ^‘(𝑚 ∈ ℕ ↦ (𝐿‘(𝐺𝑚)))) = (Σ^‘(𝑚 ∈ ℕ ↦ (𝐿‘((𝐼‘(1st ‘(𝐹𝑚)))‘(2nd ‘(𝐹𝑚)))))))
320 nfv 1830 . . . . . 6 𝑝𝜑
321 fveq2 6103 . . . . . . . . 9 (𝑝 = (𝐹𝑚) → (1st𝑝) = (1st ‘(𝐹𝑚)))
322321fveq2d 6107 . . . . . . . 8 (𝑝 = (𝐹𝑚) → (𝐼‘(1st𝑝)) = (𝐼‘(1st ‘(𝐹𝑚))))
323 fveq2 6103 . . . . . . . 8 (𝑝 = (𝐹𝑚) → (2nd𝑝) = (2nd ‘(𝐹𝑚)))
324322, 323fveq12d 6109 . . . . . . 7 (𝑝 = (𝐹𝑚) → ((𝐼‘(1st𝑝))‘(2nd𝑝)) = ((𝐼‘(1st ‘(𝐹𝑚)))‘(2nd ‘(𝐹𝑚))))
325324fveq2d 6107 . . . . . 6 (𝑝 = (𝐹𝑚) → (𝐿‘((𝐼‘(1st𝑝))‘(2nd𝑝))) = (𝐿‘((𝐼‘(1st ‘(𝐹𝑚)))‘(2nd ‘(𝐹𝑚)))))
326 eqidd 2611 . . . . . 6 ((𝜑𝑚 ∈ ℕ) → (𝐹𝑚) = (𝐹𝑚))
327 nfv 1830 . . . . . . . 8 𝑘(𝜑𝑝 ∈ (ℕ × ℕ))
3281adantr 480 . . . . . . . 8 ((𝜑𝑝 ∈ (ℕ × ℕ)) → 𝑋 ∈ Fin)
329 simpl 472 . . . . . . . . 9 ((𝜑𝑝 ∈ (ℕ × ℕ)) → 𝜑)
330 xp1st 7089 . . . . . . . . . 10 (𝑝 ∈ (ℕ × ℕ) → (1st𝑝) ∈ ℕ)
331330adantl 481 . . . . . . . . 9 ((𝜑𝑝 ∈ (ℕ × ℕ)) → (1st𝑝) ∈ ℕ)
332 xp2nd 7090 . . . . . . . . . 10 (𝑝 ∈ (ℕ × ℕ) → (2nd𝑝) ∈ ℕ)
333332adantl 481 . . . . . . . . 9 ((𝜑𝑝 ∈ (ℕ × ℕ)) → (2nd𝑝) ∈ ℕ)
334 fvex 6113 . . . . . . . . . 10 (2nd𝑝) ∈ V
335 eleq1 2676 . . . . . . . . . . . 12 (𝑗 = (2nd𝑝) → (𝑗 ∈ ℕ ↔ (2nd𝑝) ∈ ℕ))
3363353anbi3d 1397 . . . . . . . . . . 11 (𝑗 = (2nd𝑝) → ((𝜑 ∧ (1st𝑝) ∈ ℕ ∧ 𝑗 ∈ ℕ) ↔ (𝜑 ∧ (1st𝑝) ∈ ℕ ∧ (2nd𝑝) ∈ ℕ)))
337 fveq2 6103 . . . . . . . . . . . 12 (𝑗 = (2nd𝑝) → ((𝐼‘(1st𝑝))‘𝑗) = ((𝐼‘(1st𝑝))‘(2nd𝑝)))
338337feq1d 5943 . . . . . . . . . . 11 (𝑗 = (2nd𝑝) → (((𝐼‘(1st𝑝))‘𝑗):𝑋⟶(ℝ × ℝ) ↔ ((𝐼‘(1st𝑝))‘(2nd𝑝)):𝑋⟶(ℝ × ℝ)))
339336, 338imbi12d 333 . . . . . . . . . 10 (𝑗 = (2nd𝑝) → (((𝜑 ∧ (1st𝑝) ∈ ℕ ∧ 𝑗 ∈ ℕ) → ((𝐼‘(1st𝑝))‘𝑗):𝑋⟶(ℝ × ℝ)) ↔ ((𝜑 ∧ (1st𝑝) ∈ ℕ ∧ (2nd𝑝) ∈ ℕ) → ((𝐼‘(1st𝑝))‘(2nd𝑝)):𝑋⟶(ℝ × ℝ))))
340 fvex 6113 . . . . . . . . . . 11 (1st𝑝) ∈ V
341 eleq1 2676 . . . . . . . . . . . . 13 (𝑛 = (1st𝑝) → (𝑛 ∈ ℕ ↔ (1st𝑝) ∈ ℕ))
3423413anbi2d 1396 . . . . . . . . . . . 12 (𝑛 = (1st𝑝) → ((𝜑𝑛 ∈ ℕ ∧ 𝑗 ∈ ℕ) ↔ (𝜑 ∧ (1st𝑝) ∈ ℕ ∧ 𝑗 ∈ ℕ)))
343 fveq2 6103 . . . . . . . . . . . . . 14 (𝑛 = (1st𝑝) → (𝐼𝑛) = (𝐼‘(1st𝑝)))
344343fveq1d 6105 . . . . . . . . . . . . 13 (𝑛 = (1st𝑝) → ((𝐼𝑛)‘𝑗) = ((𝐼‘(1st𝑝))‘𝑗))
345344feq1d 5943 . . . . . . . . . . . 12 (𝑛 = (1st𝑝) → (((𝐼𝑛)‘𝑗):𝑋⟶(ℝ × ℝ) ↔ ((𝐼‘(1st𝑝))‘𝑗):𝑋⟶(ℝ × ℝ)))
346342, 345imbi12d 333 . . . . . . . . . . 11 (𝑛 = (1st𝑝) → (((𝜑𝑛 ∈ ℕ ∧ 𝑗 ∈ ℕ) → ((𝐼𝑛)‘𝑗):𝑋⟶(ℝ × ℝ)) ↔ ((𝜑 ∧ (1st𝑝) ∈ ℕ ∧ 𝑗 ∈ ℕ) → ((𝐼‘(1st𝑝))‘𝑗):𝑋⟶(ℝ × ℝ))))
347340, 346, 106vtocl 3232 . . . . . . . . . 10 ((𝜑 ∧ (1st𝑝) ∈ ℕ ∧ 𝑗 ∈ ℕ) → ((𝐼‘(1st𝑝))‘𝑗):𝑋⟶(ℝ × ℝ))
348334, 339, 347vtocl 3232 . . . . . . . . 9 ((𝜑 ∧ (1st𝑝) ∈ ℕ ∧ (2nd𝑝) ∈ ℕ) → ((𝐼‘(1st𝑝))‘(2nd𝑝)):𝑋⟶(ℝ × ℝ))
349329, 331, 333, 348syl3anc 1318 . . . . . . . 8 ((𝜑𝑝 ∈ (ℕ × ℕ)) → ((𝐼‘(1st𝑝))‘(2nd𝑝)):𝑋⟶(ℝ × ℝ))
350327, 328, 19, 349hoiprodcl2 39445 . . . . . . 7 ((𝜑𝑝 ∈ (ℕ × ℕ)) → (𝐿‘((𝐼‘(1st𝑝))‘(2nd𝑝))) ∈ (0[,)+∞))
35115, 350sseldi 3566 . . . . . 6 ((𝜑𝑝 ∈ (ℕ × ℕ)) → (𝐿‘((𝐼‘(1st𝑝))‘(2nd𝑝))) ∈ (0[,]+∞))
352320, 12, 325, 14, 20, 326, 351sge0f1o 39275 . . . . 5 (𝜑 → (Σ^‘(𝑝 ∈ (ℕ × ℕ) ↦ (𝐿‘((𝐼‘(1st𝑝))‘(2nd𝑝))))) = (Σ^‘(𝑚 ∈ ℕ ↦ (𝐿‘((𝐼‘(1st ‘(𝐹𝑚)))‘(2nd ‘(𝐹𝑚)))))))
353319, 352eqtr4d 2647 . . . 4 (𝜑 → (Σ^‘(𝑚 ∈ ℕ ↦ (𝐿‘(𝐺𝑚)))) = (Σ^‘(𝑝 ∈ (ℕ × ℕ) ↦ (𝐿‘((𝐼‘(1st𝑝))‘(2nd𝑝))))))
354 nfv 1830 . . . . . . 7 𝑗𝜑
355273, 274op1std 7069 . . . . . . . . . 10 (𝑝 = ⟨𝑛, 𝑗⟩ → (1st𝑝) = 𝑛)
356355fveq2d 6107 . . . . . . . . 9 (𝑝 = ⟨𝑛, 𝑗⟩ → (𝐼‘(1st𝑝)) = (𝐼𝑛))
357273, 274op2ndd 7070 . . . . . . . . 9 (𝑝 = ⟨𝑛, 𝑗⟩ → (2nd𝑝) = 𝑗)
358356, 357fveq12d 6109 . . . . . . . 8 (𝑝 = ⟨𝑛, 𝑗⟩ → ((𝐼‘(1st𝑝))‘(2nd𝑝)) = ((𝐼𝑛)‘𝑗))
359358fveq2d 6107 . . . . . . 7 (𝑝 = ⟨𝑛, 𝑗⟩ → (𝐿‘((𝐼‘(1st𝑝))‘(2nd𝑝))) = (𝐿‘((𝐼𝑛)‘𝑗)))
360 nfv 1830 . . . . . . . . . 10 𝑘((𝜑𝑛 ∈ ℕ) ∧ 𝑗 ∈ ℕ)
361127adantr 480 . . . . . . . . . 10 (((𝜑𝑛 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → 𝑋 ∈ Fin)
36297, 105syl 17 . . . . . . . . . 10 (((𝜑𝑛 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → ((𝐼𝑛)‘𝑗):𝑋⟶(ℝ × ℝ))
363360, 361, 19, 362hoiprodcl2 39445 . . . . . . . . 9 (((𝜑𝑛 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → (𝐿‘((𝐼𝑛)‘𝑗)) ∈ (0[,)+∞))
36415, 363sseldi 3566 . . . . . . . 8 (((𝜑𝑛 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → (𝐿‘((𝐼𝑛)‘𝑗)) ∈ (0[,]+∞))
3653643impa 1251 . . . . . . 7 ((𝜑𝑛 ∈ ℕ ∧ 𝑗 ∈ ℕ) → (𝐿‘((𝐼𝑛)‘𝑗)) ∈ (0[,]+∞))
366354, 359, 14, 14, 365sge0xp 39322 . . . . . 6 (𝜑 → (Σ^‘(𝑛 ∈ ℕ ↦ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘((𝐼𝑛)‘𝑗)))))) = (Σ^‘(𝑝 ∈ (ℕ × ℕ) ↦ (𝐿‘((𝐼‘(1st𝑝))‘(2nd𝑝))))))
367366eqcomd 2616 . . . . 5 (𝜑 → (Σ^‘(𝑝 ∈ (ℕ × ℕ) ↦ (𝐿‘((𝐼‘(1st𝑝))‘(2nd𝑝))))) = (Σ^‘(𝑛 ∈ ℕ ↦ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘((𝐼𝑛)‘𝑗)))))))
36813a1i 11 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → ℕ ∈ V)
369 eqid 2610 . . . . . . . 8 (𝑗 ∈ ℕ ↦ (𝐿‘((𝐼𝑛)‘𝑗))) = (𝑗 ∈ ℕ ↦ (𝐿‘((𝐼𝑛)‘𝑗)))
370364, 369fmptd 6292 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → (𝑗 ∈ ℕ ↦ (𝐿‘((𝐼𝑛)‘𝑗))):ℕ⟶(0[,]+∞))
371368, 370sge0cl 39274 . . . . . 6 ((𝜑𝑛 ∈ ℕ) → (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘((𝐼𝑛)‘𝑗)))) ∈ (0[,]+∞))
372 fveq1 6102 . . . . . . . . . . . . 13 (𝑖 = (𝐼𝑛) → (𝑖𝑗) = ((𝐼𝑛)‘𝑗))
373372fveq2d 6107 . . . . . . . . . . . 12 (𝑖 = (𝐼𝑛) → (𝐿‘(𝑖𝑗)) = (𝐿‘((𝐼𝑛)‘𝑗)))
374373mpteq2dv 4673 . . . . . . . . . . 11 (𝑖 = (𝐼𝑛) → (𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗))) = (𝑗 ∈ ℕ ↦ (𝐿‘((𝐼𝑛)‘𝑗))))
375374fveq2d 6107 . . . . . . . . . 10 (𝑖 = (𝐼𝑛) → (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) = (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘((𝐼𝑛)‘𝑗)))))
376375breq1d 4593 . . . . . . . . 9 (𝑖 = (𝐼𝑛) → ((Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛))) ↔ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘((𝐼𝑛)‘𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛)))))
377376elrab 3331 . . . . . . . 8 ((𝐼𝑛) ∈ {𝑖 ∈ (𝐶‘(𝐴𝑛)) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛)))} ↔ ((𝐼𝑛) ∈ (𝐶‘(𝐴𝑛)) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘((𝐼𝑛)‘𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛)))))
378247, 377sylib 207 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → ((𝐼𝑛) ∈ (𝐶‘(𝐴𝑛)) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘((𝐼𝑛)‘𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛)))))
379378simprd 478 . . . . . 6 ((𝜑𝑛 ∈ ℕ) → (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘((𝐼𝑛)‘𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛))))
380122, 14, 371, 179, 379sge0lempt 39303 . . . . 5 (𝜑 → (Σ^‘(𝑛 ∈ ℕ ↦ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘((𝐼𝑛)‘𝑗)))))) ≤ (Σ^‘(𝑛 ∈ ℕ ↦ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛))))))
381367, 380eqbrtrd 4605 . . . 4 (𝜑 → (Σ^‘(𝑝 ∈ (ℕ × ℕ) ↦ (𝐿‘((𝐼‘(1st𝑝))‘(2nd𝑝))))) ≤ (Σ^‘(𝑛 ∈ ℕ ↦ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛))))))
382353, 381eqbrtrd 4605 . . 3 (𝜑 → (Σ^‘(𝑚 ∈ ℕ ↦ (𝐿‘(𝐺𝑚)))) ≤ (Σ^‘(𝑛 ∈ ℕ ↦ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛))))))
38311, 121, 180, 316, 382xrletrd 11869 . 2 (𝜑 → ((voln*‘𝑋)‘ 𝑛 ∈ ℕ (𝐴𝑛)) ≤ (Σ^‘(𝑛 ∈ ℕ ↦ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛))))))
384122, 14, 166, 174sge0xadd 39328 . . 3 (𝜑 → (Σ^‘(𝑛 ∈ ℕ ↦ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛))))) = ((Σ^‘(𝑛 ∈ ℕ ↦ ((voln*‘𝑋)‘(𝐴𝑛)))) +𝑒^‘(𝑛 ∈ ℕ ↦ (𝐸 / (2↑𝑛))))))
385123a1i 11 . . . . . 6 (𝜑 → 0 ∈ ℝ*)
386125a1i 11 . . . . . 6 (𝜑 → +∞ ∈ ℝ*)
387151rexrd 9968 . . . . . 6 (𝜑𝐸 ∈ ℝ*)
38874rpge0d 11752 . . . . . 6 (𝜑 → 0 ≤ 𝐸)
389151ltpnfd 11831 . . . . . 6 (𝜑𝐸 < +∞)
390385, 386, 387, 388, 389elicod 12095 . . . . 5 (𝜑𝐸 ∈ (0[,)+∞))
391390sge0ad2en 39324 . . . 4 (𝜑 → (Σ^‘(𝑛 ∈ ℕ ↦ (𝐸 / (2↑𝑛)))) = 𝐸)
392391oveq2d 6565 . . 3 (𝜑 → ((Σ^‘(𝑛 ∈ ℕ ↦ ((voln*‘𝑋)‘(𝐴𝑛)))) +𝑒^‘(𝑛 ∈ ℕ ↦ (𝐸 / (2↑𝑛))))) = ((Σ^‘(𝑛 ∈ ℕ ↦ ((voln*‘𝑋)‘(𝐴𝑛)))) +𝑒 𝐸))
393384, 392eqtrd 2644 . 2 (𝜑 → (Σ^‘(𝑛 ∈ ℕ ↦ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛))))) = ((Σ^‘(𝑛 ∈ ℕ ↦ ((voln*‘𝑋)‘(𝐴𝑛)))) +𝑒 𝐸))
394383, 393breqtrd 4609 1 (𝜑 → ((voln*‘𝑋)‘ 𝑛 ∈ ℕ (𝐴𝑛)) ≤ ((Σ^‘(𝑛 ∈ ℕ ↦ ((voln*‘𝑋)‘(𝐴𝑛)))) +𝑒 𝐸))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1031   = wceq 1475   ∈ wcel 1977   ≠ wne 2780  ∀wral 2896  ∃wrex 2897  {crab 2900  Vcvv 3173   ⊆ wss 3540  ∅c0 3874  ifcif 4036  𝒫 cpw 4108  ⟨cop 4131  ∪ ciun 4455   class class class wbr 4583   ↦ cmpt 4643   × cxp 5036   ∘ ccom 5042   Fn wfn 5799  ⟶wf 5800  –onto→wfo 5802  –1-1-onto→wf1o 5803  ‘cfv 5804  (class class class)co 6549  1st c1st 7057  2nd c2nd 7058   ↑𝑚 cmap 7744  Xcixp 7794  Fincfn 7841  infcinf 8230  ℝcr 9814  0cc0 9815  +∞cpnf 9950  ℝ*cxr 9952   < clt 9953   ≤ cle 9954   / cdiv 10563  ℕcn 10897  2c2 10947  ℝ+crp 11708   +𝑒 cxad 11820  [,)cico 12048  [,]cicc 12049  ↑cexp 12722  ∏cprod 14474  volcvol 23039  Σ^csumge0 39255  voln*covoln 39426 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-inf2 8421  ax-ac2 9168  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892  ax-pre-sup 9893  ax-addf 9894  ax-mulf 9895 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-fal 1481  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-disj 4554  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-se 4998  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-isom 5813  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-of 6795  df-om 6958  df-1st 7059  df-2nd 7060  df-tpos 7239  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-2o 7448  df-oadd 7451  df-er 7629  df-map 7746  df-pm 7747  df-ixp 7795  df-en 7842  df-dom 7843  df-sdom 7844  df-fin 7845  df-fi 8200  df-sup 8231  df-inf 8232  df-oi 8298  df-card 8648  df-acn 8651  df-ac 8822  df-cda 8873  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-div 10564  df-nn 10898  df-2 10956  df-3 10957  df-4 10958  df-5 10959  df-6 10960  df-7 10961  df-8 10962  df-9 10963  df-n0 11170  df-z 11255  df-dec 11370  df-uz 11564  df-q 11665  df-rp 11709  df-xneg 11822  df-xadd 11823  df-xmul 11824  df-ioo 12050  df-ico 12052  df-icc 12053  df-fz 12198  df-fzo 12335  df-fl 12455  df-seq 12664  df-exp 12723  df-hash 12980  df-cj 13687  df-re 13688  df-im 13689  df-sqrt 13823  df-abs 13824  df-clim 14067  df-rlim 14068  df-sum 14265  df-prod 14475  df-struct 15697  df-ndx 15698  df-slot 15699  df-base 15700  df-sets 15701  df-ress 15702  df-plusg 15781  df-mulr 15782  df-starv 15783  df-tset 15787  df-ple 15788  df-ds 15791  df-unif 15792  df-rest 15906  df-0g 15925  df-topgen 15927  df-mgm 17065  df-sgrp 17107  df-mnd 17118  df-grp 17248  df-minusg 17249  df-subg 17414  df-cmn 18018  df-abl 18019  df-mgp 18313  df-ur 18325  df-ring 18372  df-cring 18373  df-oppr 18446  df-dvdsr 18464  df-unit 18465  df-invr 18495  df-dvr 18506  df-drng 18572  df-psmet 19559  df-xmet 19560  df-met 19561  df-bl 19562  df-mopn 19563  df-cnfld 19568  df-top 20521  df-bases 20522  df-topon 20523  df-cmp 21000  df-ovol 23040  df-vol 23041  df-sumge0 39256  df-ovoln 39427 This theorem is referenced by:  ovnsubaddlem2  39461
 Copyright terms: Public domain W3C validator