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 42729
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 (𝜑𝐴:ℕ⟶𝒫 (ℝ ↑m 𝑋))
ovnsubaddlem1.e (𝜑𝐸 ∈ ℝ+)
ovnsubaddlem1.z 𝑍 = (𝑎 ∈ 𝒫 (ℝ ↑m 𝑋) ↦ {𝑧 ∈ ℝ* ∣ ∃𝑖 ∈ (((ℝ × ℝ) ↑m 𝑋) ↑m ℕ)(𝑎 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑖𝑗))‘𝑘) ∧ 𝑧 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘𝑋 (vol‘(([,) ∘ (𝑖𝑗))‘𝑘)))))})
ovnsubaddlem1.c 𝐶 = (𝑎 ∈ 𝒫 (ℝ ↑m 𝑋) ↦ { ∈ (((ℝ × ℝ) ↑m 𝑋) ↑m ℕ) ∣ 𝑎 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘)})
ovnsubaddlem1.l 𝐿 = (𝑖 ∈ ((ℝ × ℝ) ↑m 𝑋) ↦ ∏𝑘𝑋 (vol‘(([,) ∘ 𝑖)‘𝑘)))
ovnsubaddlem1.d 𝐷 = (𝑎 ∈ 𝒫 (ℝ ↑m 𝑋) ↦ (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶𝑎) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((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 (𝜑𝐴:ℕ⟶𝒫 (ℝ ↑m 𝑋))
32adantr 481 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → 𝐴:ℕ⟶𝒫 (ℝ ↑m 𝑋))
4 simpr 485 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → 𝑛 ∈ ℕ)
53, 4ffvelrnd 6844 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → (𝐴𝑛) ∈ 𝒫 (ℝ ↑m 𝑋))
6 elpwi 4547 . . . . . . 7 ((𝐴𝑛) ∈ 𝒫 (ℝ ↑m 𝑋) → (𝐴𝑛) ⊆ (ℝ ↑m 𝑋))
75, 6syl 17 . . . . . 6 ((𝜑𝑛 ∈ ℕ) → (𝐴𝑛) ⊆ (ℝ ↑m 𝑋))
87ralrimiva 3179 . . . . 5 (𝜑 → ∀𝑛 ∈ ℕ (𝐴𝑛) ⊆ (ℝ ↑m 𝑋))
9 iunss 4960 . . . . 5 ( 𝑛 ∈ ℕ (𝐴𝑛) ⊆ (ℝ ↑m 𝑋) ↔ ∀𝑛 ∈ ℕ (𝐴𝑛) ⊆ (ℝ ↑m 𝑋))
108, 9sylibr 235 . . . 4 (𝜑 𝑛 ∈ ℕ (𝐴𝑛) ⊆ (ℝ ↑m 𝑋))
111, 10ovnxrcl 42728 . . 3 (𝜑 → ((voln*‘𝑋)‘ 𝑛 ∈ ℕ (𝐴𝑛)) ∈ ℝ*)
12 nfv 1906 . . . 4 𝑚𝜑
13 nnex 11632 . . . . 5 ℕ ∈ V
1413a1i 11 . . . 4 (𝜑 → ℕ ∈ V)
15 icossicc 12812 . . . . 5 (0[,)+∞) ⊆ (0[,]+∞)
16 nfv 1906 . . . . . 6 𝑘(𝜑𝑚 ∈ ℕ)
17 simpl 483 . . . . . . 7 ((𝜑𝑚 ∈ ℕ) → 𝜑)
1817, 1syl 17 . . . . . 6 ((𝜑𝑚 ∈ ℕ) → 𝑋 ∈ Fin)
19 ovnsubaddlem1.l . . . . . 6 𝐿 = (𝑖 ∈ ((ℝ × ℝ) ↑m 𝑋) ↦ ∏𝑘𝑋 (vol‘(([,) ∘ 𝑖)‘𝑘)))
20 ovnsubaddlem1.f . . . . . . . . . . . 12 (𝜑𝐹:ℕ–1-1-onto→(ℕ × ℕ))
21 f1of 6608 . . . . . . . . . . . 12 (𝐹:ℕ–1-1-onto→(ℕ × ℕ) → 𝐹:ℕ⟶(ℕ × ℕ))
2220, 21syl 17 . . . . . . . . . . 11 (𝜑𝐹:ℕ⟶(ℕ × ℕ))
2322adantr 481 . . . . . . . . . 10 ((𝜑𝑚 ∈ ℕ) → 𝐹:ℕ⟶(ℕ × ℕ))
24 simpr 485 . . . . . . . . . 10 ((𝜑𝑚 ∈ ℕ) → 𝑚 ∈ ℕ)
2523, 24ffvelrnd 6844 . . . . . . . . 9 ((𝜑𝑚 ∈ ℕ) → (𝐹𝑚) ∈ (ℕ × ℕ))
26 xp1st 7710 . . . . . . . . 9 ((𝐹𝑚) ∈ (ℕ × ℕ) → (1st ‘(𝐹𝑚)) ∈ ℕ)
2725, 26syl 17 . . . . . . . 8 ((𝜑𝑚 ∈ ℕ) → (1st ‘(𝐹𝑚)) ∈ ℕ)
28 xp2nd 7711 . . . . . . . . 9 ((𝐹𝑚) ∈ (ℕ × ℕ) → (2nd ‘(𝐹𝑚)) ∈ ℕ)
2925, 28syl 17 . . . . . . . 8 ((𝜑𝑚 ∈ ℕ) → (2nd ‘(𝐹𝑚)) ∈ ℕ)
30 fvex 6676 . . . . . . . . 9 (2nd ‘(𝐹𝑚)) ∈ V
31 eleq1 2897 . . . . . . . . . . 11 (𝑗 = (2nd ‘(𝐹𝑚)) → (𝑗 ∈ ℕ ↔ (2nd ‘(𝐹𝑚)) ∈ ℕ))
32313anbi3d 1433 . . . . . . . . . 10 (𝑗 = (2nd ‘(𝐹𝑚)) → ((𝜑 ∧ (1st ‘(𝐹𝑚)) ∈ ℕ ∧ 𝑗 ∈ ℕ) ↔ (𝜑 ∧ (1st ‘(𝐹𝑚)) ∈ ℕ ∧ (2nd ‘(𝐹𝑚)) ∈ ℕ)))
33 fveq2 6663 . . . . . . . . . . 11 (𝑗 = (2nd ‘(𝐹𝑚)) → ((𝐼‘(1st ‘(𝐹𝑚)))‘𝑗) = ((𝐼‘(1st ‘(𝐹𝑚)))‘(2nd ‘(𝐹𝑚))))
3433feq1d 6492 . . . . . . . . . 10 (𝑗 = (2nd ‘(𝐹𝑚)) → (((𝐼‘(1st ‘(𝐹𝑚)))‘𝑗):𝑋⟶(ℝ × ℝ) ↔ ((𝐼‘(1st ‘(𝐹𝑚)))‘(2nd ‘(𝐹𝑚))):𝑋⟶(ℝ × ℝ)))
3532, 34imbi12d 346 . . . . . . . . 9 (𝑗 = (2nd ‘(𝐹𝑚)) → (((𝜑 ∧ (1st ‘(𝐹𝑚)) ∈ ℕ ∧ 𝑗 ∈ ℕ) → ((𝐼‘(1st ‘(𝐹𝑚)))‘𝑗):𝑋⟶(ℝ × ℝ)) ↔ ((𝜑 ∧ (1st ‘(𝐹𝑚)) ∈ ℕ ∧ (2nd ‘(𝐹𝑚)) ∈ ℕ) → ((𝐼‘(1st ‘(𝐹𝑚)))‘(2nd ‘(𝐹𝑚))):𝑋⟶(ℝ × ℝ))))
36 fvex 6676 . . . . . . . . . 10 (1st ‘(𝐹𝑚)) ∈ V
37 eleq1 2897 . . . . . . . . . . . 12 (𝑛 = (1st ‘(𝐹𝑚)) → (𝑛 ∈ ℕ ↔ (1st ‘(𝐹𝑚)) ∈ ℕ))
38373anbi2d 1432 . . . . . . . . . . 11 (𝑛 = (1st ‘(𝐹𝑚)) → ((𝜑𝑛 ∈ ℕ ∧ 𝑗 ∈ ℕ) ↔ (𝜑 ∧ (1st ‘(𝐹𝑚)) ∈ ℕ ∧ 𝑗 ∈ ℕ)))
39 fveq2 6663 . . . . . . . . . . . . 13 (𝑛 = (1st ‘(𝐹𝑚)) → (𝐼𝑛) = (𝐼‘(1st ‘(𝐹𝑚))))
4039fveq1d 6665 . . . . . . . . . . . 12 (𝑛 = (1st ‘(𝐹𝑚)) → ((𝐼𝑛)‘𝑗) = ((𝐼‘(1st ‘(𝐹𝑚)))‘𝑗))
4140feq1d 6492 . . . . . . . . . . 11 (𝑛 = (1st ‘(𝐹𝑚)) → (((𝐼𝑛)‘𝑗):𝑋⟶(ℝ × ℝ) ↔ ((𝐼‘(1st ‘(𝐹𝑚)))‘𝑗):𝑋⟶(ℝ × ℝ)))
4238, 41imbi12d 346 . . . . . . . . . 10 (𝑛 = (1st ‘(𝐹𝑚)) → (((𝜑𝑛 ∈ ℕ ∧ 𝑗 ∈ ℕ) → ((𝐼𝑛)‘𝑗):𝑋⟶(ℝ × ℝ)) ↔ ((𝜑 ∧ (1st ‘(𝐹𝑚)) ∈ ℕ ∧ 𝑗 ∈ ℕ) → ((𝐼‘(1st ‘(𝐹𝑚)))‘𝑗):𝑋⟶(ℝ × ℝ))))
43 ovnsubaddlem1.c . . . . . . . . . . . . . . . . . . 19 𝐶 = (𝑎 ∈ 𝒫 (ℝ ↑m 𝑋) ↦ { ∈ (((ℝ × ℝ) ↑m 𝑋) ↑m ℕ) ∣ 𝑎 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘)})
44 sseq1 3989 . . . . . . . . . . . . . . . . . . . 20 (𝑎 = (𝐴𝑛) → (𝑎 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘) ↔ (𝐴𝑛) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘)))
4544rabbidv 3478 . . . . . . . . . . . . . . . . . . 19 (𝑎 = (𝐴𝑛) → { ∈ (((ℝ × ℝ) ↑m 𝑋) ↑m ℕ) ∣ 𝑎 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘)} = { ∈ (((ℝ × ℝ) ↑m 𝑋) ↑m ℕ) ∣ (𝐴𝑛) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘)})
46 ovex 7178 . . . . . . . . . . . . . . . . . . . . 21 (((ℝ × ℝ) ↑m 𝑋) ↑m ℕ) ∈ V
4746rabex 5226 . . . . . . . . . . . . . . . . . . . 20 { ∈ (((ℝ × ℝ) ↑m 𝑋) ↑m ℕ) ∣ (𝐴𝑛) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘)} ∈ V
4847a1i 11 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑛 ∈ ℕ) → { ∈ (((ℝ × ℝ) ↑m 𝑋) ↑m ℕ) ∣ (𝐴𝑛) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘)} ∈ V)
4943, 45, 5, 48fvmptd3 6783 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑛 ∈ ℕ) → (𝐶‘(𝐴𝑛)) = { ∈ (((ℝ × ℝ) ↑m 𝑋) ↑m ℕ) ∣ (𝐴𝑛) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘)})
50 ssrab2 4053 . . . . . . . . . . . . . . . . . . 19 { ∈ (((ℝ × ℝ) ↑m 𝑋) ↑m ℕ) ∣ (𝐴𝑛) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘)} ⊆ (((ℝ × ℝ) ↑m 𝑋) ↑m ℕ)
5150a1i 11 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑛 ∈ ℕ) → { ∈ (((ℝ × ℝ) ↑m 𝑋) ↑m ℕ) ∣ (𝐴𝑛) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘)} ⊆ (((ℝ × ℝ) ↑m 𝑋) ↑m ℕ))
5249, 51eqsstrd 4002 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛 ∈ ℕ) → (𝐶‘(𝐴𝑛)) ⊆ (((ℝ × ℝ) ↑m 𝑋) ↑m ℕ))
53 ovnsubaddlem1.d . . . . . . . . . . . . . . . . . . . . 21 𝐷 = (𝑎 ∈ 𝒫 (ℝ ↑m 𝑋) ↦ (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶𝑎) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘𝑎) +𝑒 𝑒)}))
54 fveq2 6663 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑎 = (𝐴𝑛) → (𝐶𝑎) = (𝐶‘(𝐴𝑛)))
5554eleq2d 2895 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑎 = (𝐴𝑛) → (𝑖 ∈ (𝐶𝑎) ↔ 𝑖 ∈ (𝐶‘(𝐴𝑛))))
56 fveq2 6663 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑎 = (𝐴𝑛) → ((voln*‘𝑋)‘𝑎) = ((voln*‘𝑋)‘(𝐴𝑛)))
5756oveq1d 7160 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑎 = (𝐴𝑛) → (((voln*‘𝑋)‘𝑎) +𝑒 𝑒) = (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 𝑒))
5857breq2d 5069 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑎 = (𝐴𝑛) → ((Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘𝑎) +𝑒 𝑒) ↔ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 𝑒)))
5955, 58anbi12d 630 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑎 = (𝐴𝑛) → ((𝑖 ∈ (𝐶𝑎) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘𝑎) +𝑒 𝑒)) ↔ (𝑖 ∈ (𝐶‘(𝐴𝑛)) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 𝑒))))
6059rabbidva2 3474 . . . . . . . . . . . . . . . . . . . . . 22 (𝑎 = (𝐴𝑛) → {𝑖 ∈ (𝐶𝑎) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘𝑎) +𝑒 𝑒)} = {𝑖 ∈ (𝐶‘(𝐴𝑛)) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 𝑒)})
6160mpteq2dv 5153 . . . . . . . . . . . . . . . . . . . . 21 (𝑎 = (𝐴𝑛) → (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶𝑎) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘𝑎) +𝑒 𝑒)}) = (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶‘(𝐴𝑛)) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 𝑒)}))
62 rpex 41490 . . . . . . . . . . . . . . . . . . . . . . 23 + ∈ V
6362mptex 6977 . . . . . . . . . . . . . . . . . . . . . 22 (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶‘(𝐴𝑛)) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 𝑒)}) ∈ V
6463a1i 11 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑛 ∈ ℕ) → (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶‘(𝐴𝑛)) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 𝑒)}) ∈ V)
6553, 61, 5, 64fvmptd3 6783 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑛 ∈ ℕ) → (𝐷‘(𝐴𝑛)) = (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶‘(𝐴𝑛)) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 𝑒)}))
66 oveq2 7153 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑒 = (𝐸 / (2↑𝑛)) → (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 𝑒) = (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛))))
6766breq2d 5069 . . . . . . . . . . . . . . . . . . . . . 22 (𝑒 = (𝐸 / (2↑𝑛)) → ((Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 𝑒) ↔ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛)))))
6867rabbidv 3478 . . . . . . . . . . . . . . . . . . . . 21 (𝑒 = (𝐸 / (2↑𝑛)) → {𝑖 ∈ (𝐶‘(𝐴𝑛)) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 𝑒)} = {𝑖 ∈ (𝐶‘(𝐴𝑛)) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛)))})
6968adantl 482 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑛 ∈ ℕ) ∧ 𝑒 = (𝐸 / (2↑𝑛))) → {𝑖 ∈ (𝐶‘(𝐴𝑛)) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 𝑒)} = {𝑖 ∈ (𝐶‘(𝐴𝑛)) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛)))})
70 ovnsubaddlem1.e . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝐸 ∈ ℝ+)
7170adantr 481 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑛 ∈ ℕ) → 𝐸 ∈ ℝ+)
72 2nn 11698 . . . . . . . . . . . . . . . . . . . . . . . . 25 2 ∈ ℕ
7372a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 ∈ ℕ → 2 ∈ ℕ)
74 nnnn0 11892 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 ∈ ℕ → 𝑛 ∈ ℕ0)
7573, 74nnexpcld 13594 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 ∈ ℕ → (2↑𝑛) ∈ ℕ)
7675nnrpd 12417 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 ∈ ℕ → (2↑𝑛) ∈ ℝ+)
7776adantl 482 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑛 ∈ ℕ) → (2↑𝑛) ∈ ℝ+)
7871, 77rpdivcld 12436 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑛 ∈ ℕ) → (𝐸 / (2↑𝑛)) ∈ ℝ+)
79 fvex 6676 . . . . . . . . . . . . . . . . . . . . . 22 (𝐶‘(𝐴𝑛)) ∈ V
8079rabex 5226 . . . . . . . . . . . . . . . . . . . . 21 {𝑖 ∈ (𝐶‘(𝐴𝑛)) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛)))} ∈ V
8180a1i 11 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑛 ∈ ℕ) → {𝑖 ∈ (𝐶‘(𝐴𝑛)) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛)))} ∈ V)
8265, 69, 78, 81fvmptd 6767 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑛 ∈ ℕ) → ((𝐷‘(𝐴𝑛))‘(𝐸 / (2↑𝑛))) = {𝑖 ∈ (𝐶‘(𝐴𝑛)) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛)))})
83 ssrab2 4053 . . . . . . . . . . . . . . . . . . . 20 {𝑖 ∈ (𝐶‘(𝐴𝑛)) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛)))} ⊆ (𝐶‘(𝐴𝑛))
8483a1i 11 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑛 ∈ ℕ) → {𝑖 ∈ (𝐶‘(𝐴𝑛)) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛)))} ⊆ (𝐶‘(𝐴𝑛)))
8582, 84eqsstrd 4002 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑛 ∈ ℕ) → ((𝐷‘(𝐴𝑛))‘(𝐸 / (2↑𝑛))) ⊆ (𝐶‘(𝐴𝑛)))
86 ovnsubaddlem1.i . . . . . . . . . . . . . . . . . 18 ((𝜑𝑛 ∈ ℕ) → (𝐼𝑛) ∈ ((𝐷‘(𝐴𝑛))‘(𝐸 / (2↑𝑛))))
8785, 86sseldd 3965 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛 ∈ ℕ) → (𝐼𝑛) ∈ (𝐶‘(𝐴𝑛)))
8852, 87sseldd 3965 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ ℕ) → (𝐼𝑛) ∈ (((ℝ × ℝ) ↑m 𝑋) ↑m ℕ))
89 elmapfn 8418 . . . . . . . . . . . . . . . 16 ((𝐼𝑛) ∈ (((ℝ × ℝ) ↑m 𝑋) ↑m ℕ) → (𝐼𝑛) Fn ℕ)
9088, 89syl 17 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ) → (𝐼𝑛) Fn ℕ)
91 elmapi 8417 . . . . . . . . . . . . . . . . . 18 ((𝐼𝑛) ∈ (((ℝ × ℝ) ↑m 𝑋) ↑m ℕ) → (𝐼𝑛):ℕ⟶((ℝ × ℝ) ↑m 𝑋))
9288, 91syl 17 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛 ∈ ℕ) → (𝐼𝑛):ℕ⟶((ℝ × ℝ) ↑m 𝑋))
9392ffvelrnda 6843 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → ((𝐼𝑛)‘𝑗) ∈ ((ℝ × ℝ) ↑m 𝑋))
9493ralrimiva 3179 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ) → ∀𝑗 ∈ ℕ ((𝐼𝑛)‘𝑗) ∈ ((ℝ × ℝ) ↑m 𝑋))
9590, 94jca 512 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ ℕ) → ((𝐼𝑛) Fn ℕ ∧ ∀𝑗 ∈ ℕ ((𝐼𝑛)‘𝑗) ∈ ((ℝ × ℝ) ↑m 𝑋)))
96953adant3 1124 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ ℕ ∧ 𝑗 ∈ ℕ) → ((𝐼𝑛) Fn ℕ ∧ ∀𝑗 ∈ ℕ ((𝐼𝑛)‘𝑗) ∈ ((ℝ × ℝ) ↑m 𝑋)))
97 ffnfv 6874 . . . . . . . . . . . . 13 ((𝐼𝑛):ℕ⟶((ℝ × ℝ) ↑m 𝑋) ↔ ((𝐼𝑛) Fn ℕ ∧ ∀𝑗 ∈ ℕ ((𝐼𝑛)‘𝑗) ∈ ((ℝ × ℝ) ↑m 𝑋)))
9896, 97sylibr 235 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ ∧ 𝑗 ∈ ℕ) → (𝐼𝑛):ℕ⟶((ℝ × ℝ) ↑m 𝑋))
99 simp3 1130 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ ℕ)
10098, 99ffvelrnd 6844 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ ∧ 𝑗 ∈ ℕ) → ((𝐼𝑛)‘𝑗) ∈ ((ℝ × ℝ) ↑m 𝑋))
101 elmapi 8417 . . . . . . . . . . 11 (((𝐼𝑛)‘𝑗) ∈ ((ℝ × ℝ) ↑m 𝑋) → ((𝐼𝑛)‘𝑗):𝑋⟶(ℝ × ℝ))
102100, 101syl 17 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ ∧ 𝑗 ∈ ℕ) → ((𝐼𝑛)‘𝑗):𝑋⟶(ℝ × ℝ))
10336, 42, 102vtocl 3557 . . . . . . . . 9 ((𝜑 ∧ (1st ‘(𝐹𝑚)) ∈ ℕ ∧ 𝑗 ∈ ℕ) → ((𝐼‘(1st ‘(𝐹𝑚)))‘𝑗):𝑋⟶(ℝ × ℝ))
10430, 35, 103vtocl 3557 . . . . . . . 8 ((𝜑 ∧ (1st ‘(𝐹𝑚)) ∈ ℕ ∧ (2nd ‘(𝐹𝑚)) ∈ ℕ) → ((𝐼‘(1st ‘(𝐹𝑚)))‘(2nd ‘(𝐹𝑚))):𝑋⟶(ℝ × ℝ))
10517, 27, 29, 104syl3anc 1363 . . . . . . 7 ((𝜑𝑚 ∈ ℕ) → ((𝐼‘(1st ‘(𝐹𝑚)))‘(2nd ‘(𝐹𝑚))):𝑋⟶(ℝ × ℝ))
106 id 22 . . . . . . . . . 10 (𝑚 ∈ ℕ → 𝑚 ∈ ℕ)
107 fvex 6676 . . . . . . . . . . 11 ((𝐼‘(1st ‘(𝐹𝑚)))‘(2nd ‘(𝐹𝑚))) ∈ V
108107a1i 11 . . . . . . . . . 10 (𝑚 ∈ ℕ → ((𝐼‘(1st ‘(𝐹𝑚)))‘(2nd ‘(𝐹𝑚))) ∈ V)
109 ovnsubaddlem1.g . . . . . . . . . . 11 𝐺 = (𝑚 ∈ ℕ ↦ ((𝐼‘(1st ‘(𝐹𝑚)))‘(2nd ‘(𝐹𝑚))))
110109fvmpt2 6771 . . . . . . . . . 10 ((𝑚 ∈ ℕ ∧ ((𝐼‘(1st ‘(𝐹𝑚)))‘(2nd ‘(𝐹𝑚))) ∈ V) → (𝐺𝑚) = ((𝐼‘(1st ‘(𝐹𝑚)))‘(2nd ‘(𝐹𝑚))))
111106, 108, 110syl2anc 584 . . . . . . . . 9 (𝑚 ∈ ℕ → (𝐺𝑚) = ((𝐼‘(1st ‘(𝐹𝑚)))‘(2nd ‘(𝐹𝑚))))
112111adantl 482 . . . . . . . 8 ((𝜑𝑚 ∈ ℕ) → (𝐺𝑚) = ((𝐼‘(1st ‘(𝐹𝑚)))‘(2nd ‘(𝐹𝑚))))
113112feq1d 6492 . . . . . . 7 ((𝜑𝑚 ∈ ℕ) → ((𝐺𝑚):𝑋⟶(ℝ × ℝ) ↔ ((𝐼‘(1st ‘(𝐹𝑚)))‘(2nd ‘(𝐹𝑚))):𝑋⟶(ℝ × ℝ)))
114105, 113mpbird 258 . . . . . 6 ((𝜑𝑚 ∈ ℕ) → (𝐺𝑚):𝑋⟶(ℝ × ℝ))
11516, 18, 19, 114hoiprodcl2 42714 . . . . 5 ((𝜑𝑚 ∈ ℕ) → (𝐿‘(𝐺𝑚)) ∈ (0[,)+∞))
11615, 115sseldi 3962 . . . 4 ((𝜑𝑚 ∈ ℕ) → (𝐿‘(𝐺𝑚)) ∈ (0[,]+∞))
11712, 14, 116sge0xrclmpt 42587 . . 3 (𝜑 → (Σ^‘(𝑚 ∈ ℕ ↦ (𝐿‘(𝐺𝑚)))) ∈ ℝ*)
118 nfv 1906 . . . 4 𝑛𝜑
119 0xr 10676 . . . . . 6 0 ∈ ℝ*
120119a1i 11 . . . . 5 ((𝜑𝑛 ∈ ℕ) → 0 ∈ ℝ*)
121 pnfxr 10683 . . . . . 6 +∞ ∈ ℝ*
122121a1i 11 . . . . 5 ((𝜑𝑛 ∈ ℕ) → +∞ ∈ ℝ*)
1231adantr 481 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → 𝑋 ∈ Fin)
124 ovnsubaddlem1.z . . . . . . . . 9 𝑍 = (𝑎 ∈ 𝒫 (ℝ ↑m 𝑋) ↦ {𝑧 ∈ ℝ* ∣ ∃𝑖 ∈ (((ℝ × ℝ) ↑m 𝑋) ↑m ℕ)(𝑎 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑖𝑗))‘𝑘) ∧ 𝑧 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘𝑋 (vol‘(([,) ∘ (𝑖𝑗))‘𝑘)))))})
125123, 7, 124ovnval2b 42711 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → ((voln*‘𝑋)‘(𝐴𝑛)) = if(𝑋 = ∅, 0, inf((𝑍‘(𝐴𝑛)), ℝ*, < )))
126 ovnsubaddlem1.n0 . . . . . . . . . . 11 (𝜑𝑋 ≠ ∅)
127126neneqd 3018 . . . . . . . . . 10 (𝜑 → ¬ 𝑋 = ∅)
128127iffalsed 4474 . . . . . . . . 9 (𝜑 → if(𝑋 = ∅, 0, inf((𝑍‘(𝐴𝑛)), ℝ*, < )) = inf((𝑍‘(𝐴𝑛)), ℝ*, < ))
129128adantr 481 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → if(𝑋 = ∅, 0, inf((𝑍‘(𝐴𝑛)), ℝ*, < )) = inf((𝑍‘(𝐴𝑛)), ℝ*, < ))
130125, 129eqtrd 2853 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → ((voln*‘𝑋)‘(𝐴𝑛)) = inf((𝑍‘(𝐴𝑛)), ℝ*, < ))
131 sseq1 3989 . . . . . . . . . . . . 13 (𝑎 = (𝐴𝑛) → (𝑎 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑖𝑗))‘𝑘) ↔ (𝐴𝑛) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑖𝑗))‘𝑘)))
132131anbi1d 629 . . . . . . . . . . . 12 (𝑎 = (𝐴𝑛) → ((𝑎 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑖𝑗))‘𝑘) ∧ 𝑧 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘𝑋 (vol‘(([,) ∘ (𝑖𝑗))‘𝑘))))) ↔ ((𝐴𝑛) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑖𝑗))‘𝑘) ∧ 𝑧 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘𝑋 (vol‘(([,) ∘ (𝑖𝑗))‘𝑘)))))))
133132rexbidv 3294 . . . . . . . . . . 11 (𝑎 = (𝐴𝑛) → (∃𝑖 ∈ (((ℝ × ℝ) ↑m 𝑋) ↑m ℕ)(𝑎 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑖𝑗))‘𝑘) ∧ 𝑧 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘𝑋 (vol‘(([,) ∘ (𝑖𝑗))‘𝑘))))) ↔ ∃𝑖 ∈ (((ℝ × ℝ) ↑m 𝑋) ↑m ℕ)((𝐴𝑛) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑖𝑗))‘𝑘) ∧ 𝑧 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘𝑋 (vol‘(([,) ∘ (𝑖𝑗))‘𝑘)))))))
134133rabbidv 3478 . . . . . . . . . 10 (𝑎 = (𝐴𝑛) → {𝑧 ∈ ℝ* ∣ ∃𝑖 ∈ (((ℝ × ℝ) ↑m 𝑋) ↑m ℕ)(𝑎 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑖𝑗))‘𝑘) ∧ 𝑧 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘𝑋 (vol‘(([,) ∘ (𝑖𝑗))‘𝑘)))))} = {𝑧 ∈ ℝ* ∣ ∃𝑖 ∈ (((ℝ × ℝ) ↑m 𝑋) ↑m ℕ)((𝐴𝑛) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑖𝑗))‘𝑘) ∧ 𝑧 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘𝑋 (vol‘(([,) ∘ (𝑖𝑗))‘𝑘)))))})
135 xrex 12374 . . . . . . . . . . . 12 * ∈ V
136135rabex 5226 . . . . . . . . . . 11 {𝑧 ∈ ℝ* ∣ ∃𝑖 ∈ (((ℝ × ℝ) ↑m 𝑋) ↑m ℕ)((𝐴𝑛) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑖𝑗))‘𝑘) ∧ 𝑧 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘𝑋 (vol‘(([,) ∘ (𝑖𝑗))‘𝑘)))))} ∈ V
137136a1i 11 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → {𝑧 ∈ ℝ* ∣ ∃𝑖 ∈ (((ℝ × ℝ) ↑m 𝑋) ↑m ℕ)((𝐴𝑛) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑖𝑗))‘𝑘) ∧ 𝑧 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘𝑋 (vol‘(([,) ∘ (𝑖𝑗))‘𝑘)))))} ∈ V)
138124, 134, 5, 137fvmptd3 6783 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → (𝑍‘(𝐴𝑛)) = {𝑧 ∈ ℝ* ∣ ∃𝑖 ∈ (((ℝ × ℝ) ↑m 𝑋) ↑m ℕ)((𝐴𝑛) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑖𝑗))‘𝑘) ∧ 𝑧 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘𝑋 (vol‘(([,) ∘ (𝑖𝑗))‘𝑘)))))})
139 ssrab2 4053 . . . . . . . . . 10 {𝑧 ∈ ℝ* ∣ ∃𝑖 ∈ (((ℝ × ℝ) ↑m 𝑋) ↑m ℕ)((𝐴𝑛) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑖𝑗))‘𝑘) ∧ 𝑧 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘𝑋 (vol‘(([,) ∘ (𝑖𝑗))‘𝑘)))))} ⊆ ℝ*
140139a1i 11 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → {𝑧 ∈ ℝ* ∣ ∃𝑖 ∈ (((ℝ × ℝ) ↑m 𝑋) ↑m ℕ)((𝐴𝑛) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑖𝑗))‘𝑘) ∧ 𝑧 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘𝑋 (vol‘(([,) ∘ (𝑖𝑗))‘𝑘)))))} ⊆ ℝ*)
141138, 140eqsstrd 4002 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → (𝑍‘(𝐴𝑛)) ⊆ ℝ*)
142 infxrcl 12714 . . . . . . . 8 ((𝑍‘(𝐴𝑛)) ⊆ ℝ* → inf((𝑍‘(𝐴𝑛)), ℝ*, < ) ∈ ℝ*)
143141, 142syl 17 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → inf((𝑍‘(𝐴𝑛)), ℝ*, < ) ∈ ℝ*)
144130, 143eqeltrd 2910 . . . . . 6 ((𝜑𝑛 ∈ ℕ) → ((voln*‘𝑋)‘(𝐴𝑛)) ∈ ℝ*)
14570rpred 12419 . . . . . . . . 9 (𝜑𝐸 ∈ ℝ)
146145adantr 481 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → 𝐸 ∈ ℝ)
147 2re 11699 . . . . . . . . . . 11 2 ∈ ℝ
148147a1i 11 . . . . . . . . . 10 (𝑛 ∈ ℕ → 2 ∈ ℝ)
149148, 74reexpcld 13515 . . . . . . . . 9 (𝑛 ∈ ℕ → (2↑𝑛) ∈ ℝ)
150149adantl 482 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → (2↑𝑛) ∈ ℝ)
151148recnd 10657 . . . . . . . . . 10 (𝑛 ∈ ℕ → 2 ∈ ℂ)
152 2ne0 11729 . . . . . . . . . . 11 2 ≠ 0
153152a1i 11 . . . . . . . . . 10 (𝑛 ∈ ℕ → 2 ≠ 0)
154 nnz 11992 . . . . . . . . . 10 (𝑛 ∈ ℕ → 𝑛 ∈ ℤ)
155151, 153, 154expne0d 13504 . . . . . . . . 9 (𝑛 ∈ ℕ → (2↑𝑛) ≠ 0)
156155adantl 482 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → (2↑𝑛) ≠ 0)
157146, 150, 156redivcld 11456 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → (𝐸 / (2↑𝑛)) ∈ ℝ)
158157rexrd 10679 . . . . . 6 ((𝜑𝑛 ∈ ℕ) → (𝐸 / (2↑𝑛)) ∈ ℝ*)
159144, 158xaddcld 12682 . . . . 5 ((𝜑𝑛 ∈ ℕ) → (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛))) ∈ ℝ*)
160123, 7ovncl 42726 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → ((voln*‘𝑋)‘(𝐴𝑛)) ∈ (0[,]+∞))
161 xrge0ge0 41491 . . . . . . 7 (((voln*‘𝑋)‘(𝐴𝑛)) ∈ (0[,]+∞) → 0 ≤ ((voln*‘𝑋)‘(𝐴𝑛)))
162160, 161syl 17 . . . . . 6 ((𝜑𝑛 ∈ ℕ) → 0 ≤ ((voln*‘𝑋)‘(𝐴𝑛)))
163 0red 10632 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → 0 ∈ ℝ)
16478rpgt0d 12422 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → 0 < (𝐸 / (2↑𝑛)))
165163, 157, 164ltled 10776 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → 0 ≤ (𝐸 / (2↑𝑛)))
166157ltpnfd 12504 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → (𝐸 / (2↑𝑛)) < +∞)
167158, 122, 166xrltled 12531 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → (𝐸 / (2↑𝑛)) ≤ +∞)
168120, 122, 158, 165, 167eliccxrd 41679 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → (𝐸 / (2↑𝑛)) ∈ (0[,]+∞))
169144, 168xadd0ge 41464 . . . . . 6 ((𝜑𝑛 ∈ ℕ) → ((voln*‘𝑋)‘(𝐴𝑛)) ≤ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛))))
170120, 144, 159, 162, 169xrletrd 12543 . . . . 5 ((𝜑𝑛 ∈ ℕ) → 0 ≤ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛))))
171 pnfge 12513 . . . . . 6 ((((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛))) ∈ ℝ* → (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛))) ≤ +∞)
172159, 171syl 17 . . . . 5 ((𝜑𝑛 ∈ ℕ) → (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛))) ≤ +∞)
173120, 122, 159, 170, 172eliccxrd 41679 . . . 4 ((𝜑𝑛 ∈ ℕ) → (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛))) ∈ (0[,]+∞))
174118, 14, 173sge0xrclmpt 42587 . . 3 (𝜑 → (Σ^‘(𝑛 ∈ ℕ ↦ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛))))) ∈ ℝ*)
175 sseq1 3989 . . . . . . . . . . . . 13 (𝑎 = (𝐴‘(1st ‘(𝐹𝑚))) → (𝑎 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘) ↔ (𝐴‘(1st ‘(𝐹𝑚))) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘)))
176175rabbidv 3478 . . . . . . . . . . . 12 (𝑎 = (𝐴‘(1st ‘(𝐹𝑚))) → { ∈ (((ℝ × ℝ) ↑m 𝑋) ↑m ℕ) ∣ 𝑎 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘)} = { ∈ (((ℝ × ℝ) ↑m 𝑋) ↑m ℕ) ∣ (𝐴‘(1st ‘(𝐹𝑚))) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘)})
1772adantr 481 . . . . . . . . . . . . 13 ((𝜑𝑚 ∈ ℕ) → 𝐴:ℕ⟶𝒫 (ℝ ↑m 𝑋))
178177, 27ffvelrnd 6844 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ ℕ) → (𝐴‘(1st ‘(𝐹𝑚))) ∈ 𝒫 (ℝ ↑m 𝑋))
17946rabex 5226 . . . . . . . . . . . . 13 { ∈ (((ℝ × ℝ) ↑m 𝑋) ↑m ℕ) ∣ (𝐴‘(1st ‘(𝐹𝑚))) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘)} ∈ V
180179a1i 11 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ ℕ) → { ∈ (((ℝ × ℝ) ↑m 𝑋) ↑m ℕ) ∣ (𝐴‘(1st ‘(𝐹𝑚))) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘)} ∈ V)
18143, 176, 178, 180fvmptd3 6783 . . . . . . . . . . 11 ((𝜑𝑚 ∈ ℕ) → (𝐶‘(𝐴‘(1st ‘(𝐹𝑚)))) = { ∈ (((ℝ × ℝ) ↑m 𝑋) ↑m ℕ) ∣ (𝐴‘(1st ‘(𝐹𝑚))) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘)})
182 ssrab2 4053 . . . . . . . . . . . 12 { ∈ (((ℝ × ℝ) ↑m 𝑋) ↑m ℕ) ∣ (𝐴‘(1st ‘(𝐹𝑚))) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘)} ⊆ (((ℝ × ℝ) ↑m 𝑋) ↑m ℕ)
183182a1i 11 . . . . . . . . . . 11 ((𝜑𝑚 ∈ ℕ) → { ∈ (((ℝ × ℝ) ↑m 𝑋) ↑m ℕ) ∣ (𝐴‘(1st ‘(𝐹𝑚))) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘)} ⊆ (((ℝ × ℝ) ↑m 𝑋) ↑m ℕ))
184181, 183eqsstrd 4002 . . . . . . . . . 10 ((𝜑𝑚 ∈ ℕ) → (𝐶‘(𝐴‘(1st ‘(𝐹𝑚)))) ⊆ (((ℝ × ℝ) ↑m 𝑋) ↑m ℕ))
185 fveq2 6663 . . . . . . . . . . . . . . . . . 18 (𝑎 = (𝐴‘(1st ‘(𝐹𝑚))) → (𝐶𝑎) = (𝐶‘(𝐴‘(1st ‘(𝐹𝑚)))))
186185eleq2d 2895 . . . . . . . . . . . . . . . . 17 (𝑎 = (𝐴‘(1st ‘(𝐹𝑚))) → (𝑖 ∈ (𝐶𝑎) ↔ 𝑖 ∈ (𝐶‘(𝐴‘(1st ‘(𝐹𝑚))))))
187 fveq2 6663 . . . . . . . . . . . . . . . . . . 19 (𝑎 = (𝐴‘(1st ‘(𝐹𝑚))) → ((voln*‘𝑋)‘𝑎) = ((voln*‘𝑋)‘(𝐴‘(1st ‘(𝐹𝑚)))))
188187oveq1d 7160 . . . . . . . . . . . . . . . . . 18 (𝑎 = (𝐴‘(1st ‘(𝐹𝑚))) → (((voln*‘𝑋)‘𝑎) +𝑒 𝑒) = (((voln*‘𝑋)‘(𝐴‘(1st ‘(𝐹𝑚)))) +𝑒 𝑒))
189188breq2d 5069 . . . . . . . . . . . . . . . . 17 (𝑎 = (𝐴‘(1st ‘(𝐹𝑚))) → ((Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘𝑎) +𝑒 𝑒) ↔ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴‘(1st ‘(𝐹𝑚)))) +𝑒 𝑒)))
190186, 189anbi12d 630 . . . . . . . . . . . . . . . 16 (𝑎 = (𝐴‘(1st ‘(𝐹𝑚))) → ((𝑖 ∈ (𝐶𝑎) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘𝑎) +𝑒 𝑒)) ↔ (𝑖 ∈ (𝐶‘(𝐴‘(1st ‘(𝐹𝑚)))) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴‘(1st ‘(𝐹𝑚)))) +𝑒 𝑒))))
191190rabbidva2 3474 . . . . . . . . . . . . . . 15 (𝑎 = (𝐴‘(1st ‘(𝐹𝑚))) → {𝑖 ∈ (𝐶𝑎) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘𝑎) +𝑒 𝑒)} = {𝑖 ∈ (𝐶‘(𝐴‘(1st ‘(𝐹𝑚)))) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴‘(1st ‘(𝐹𝑚)))) +𝑒 𝑒)})
192191mpteq2dv 5153 . . . . . . . . . . . . . 14 (𝑎 = (𝐴‘(1st ‘(𝐹𝑚))) → (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶𝑎) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘𝑎) +𝑒 𝑒)}) = (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶‘(𝐴‘(1st ‘(𝐹𝑚)))) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴‘(1st ‘(𝐹𝑚)))) +𝑒 𝑒)}))
19362mptex 6977 . . . . . . . . . . . . . . 15 (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶‘(𝐴‘(1st ‘(𝐹𝑚)))) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴‘(1st ‘(𝐹𝑚)))) +𝑒 𝑒)}) ∈ V
194193a1i 11 . . . . . . . . . . . . . 14 ((𝜑𝑚 ∈ ℕ) → (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶‘(𝐴‘(1st ‘(𝐹𝑚)))) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴‘(1st ‘(𝐹𝑚)))) +𝑒 𝑒)}) ∈ V)
19553, 192, 178, 194fvmptd3 6783 . . . . . . . . . . . . 13 ((𝜑𝑚 ∈ ℕ) → (𝐷‘(𝐴‘(1st ‘(𝐹𝑚)))) = (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶‘(𝐴‘(1st ‘(𝐹𝑚)))) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴‘(1st ‘(𝐹𝑚)))) +𝑒 𝑒)}))
196 oveq2 7153 . . . . . . . . . . . . . . . 16 (𝑒 = (𝐸 / (2↑(1st ‘(𝐹𝑚)))) → (((voln*‘𝑋)‘(𝐴‘(1st ‘(𝐹𝑚)))) +𝑒 𝑒) = (((voln*‘𝑋)‘(𝐴‘(1st ‘(𝐹𝑚)))) +𝑒 (𝐸 / (2↑(1st ‘(𝐹𝑚))))))
197196breq2d 5069 . . . . . . . . . . . . . . 15 (𝑒 = (𝐸 / (2↑(1st ‘(𝐹𝑚)))) → ((Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴‘(1st ‘(𝐹𝑚)))) +𝑒 𝑒) ↔ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴‘(1st ‘(𝐹𝑚)))) +𝑒 (𝐸 / (2↑(1st ‘(𝐹𝑚)))))))
198197rabbidv 3478 . . . . . . . . . . . . . 14 (𝑒 = (𝐸 / (2↑(1st ‘(𝐹𝑚)))) → {𝑖 ∈ (𝐶‘(𝐴‘(1st ‘(𝐹𝑚)))) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴‘(1st ‘(𝐹𝑚)))) +𝑒 𝑒)} = {𝑖 ∈ (𝐶‘(𝐴‘(1st ‘(𝐹𝑚)))) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴‘(1st ‘(𝐹𝑚)))) +𝑒 (𝐸 / (2↑(1st ‘(𝐹𝑚)))))})
199198adantl 482 . . . . . . . . . . . . 13 (((𝜑𝑚 ∈ ℕ) ∧ 𝑒 = (𝐸 / (2↑(1st ‘(𝐹𝑚))))) → {𝑖 ∈ (𝐶‘(𝐴‘(1st ‘(𝐹𝑚)))) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴‘(1st ‘(𝐹𝑚)))) +𝑒 𝑒)} = {𝑖 ∈ (𝐶‘(𝐴‘(1st ‘(𝐹𝑚)))) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴‘(1st ‘(𝐹𝑚)))) +𝑒 (𝐸 / (2↑(1st ‘(𝐹𝑚)))))})
20017, 70syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑚 ∈ ℕ) → 𝐸 ∈ ℝ+)
201 2rp 12382 . . . . . . . . . . . . . . . 16 2 ∈ ℝ+
202201a1i 11 . . . . . . . . . . . . . . 15 ((𝜑𝑚 ∈ ℕ) → 2 ∈ ℝ+)
20327nnzd 12074 . . . . . . . . . . . . . . 15 ((𝜑𝑚 ∈ ℕ) → (1st ‘(𝐹𝑚)) ∈ ℤ)
204202, 203rpexpcld 13596 . . . . . . . . . . . . . 14 ((𝜑𝑚 ∈ ℕ) → (2↑(1st ‘(𝐹𝑚))) ∈ ℝ+)
205200, 204rpdivcld 12436 . . . . . . . . . . . . 13 ((𝜑𝑚 ∈ ℕ) → (𝐸 / (2↑(1st ‘(𝐹𝑚)))) ∈ ℝ+)
206 fvex 6676 . . . . . . . . . . . . . . 15 (𝐶‘(𝐴‘(1st ‘(𝐹𝑚)))) ∈ V
207206rabex 5226 . . . . . . . . . . . . . 14 {𝑖 ∈ (𝐶‘(𝐴‘(1st ‘(𝐹𝑚)))) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴‘(1st ‘(𝐹𝑚)))) +𝑒 (𝐸 / (2↑(1st ‘(𝐹𝑚)))))} ∈ V
208207a1i 11 . . . . . . . . . . . . 13 ((𝜑𝑚 ∈ ℕ) → {𝑖 ∈ (𝐶‘(𝐴‘(1st ‘(𝐹𝑚)))) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴‘(1st ‘(𝐹𝑚)))) +𝑒 (𝐸 / (2↑(1st ‘(𝐹𝑚)))))} ∈ V)
209195, 199, 205, 208fvmptd 6767 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ ℕ) → ((𝐷‘(𝐴‘(1st ‘(𝐹𝑚))))‘(𝐸 / (2↑(1st ‘(𝐹𝑚))))) = {𝑖 ∈ (𝐶‘(𝐴‘(1st ‘(𝐹𝑚)))) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴‘(1st ‘(𝐹𝑚)))) +𝑒 (𝐸 / (2↑(1st ‘(𝐹𝑚)))))})
210 ssrab2 4053 . . . . . . . . . . . . 13 {𝑖 ∈ (𝐶‘(𝐴‘(1st ‘(𝐹𝑚)))) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴‘(1st ‘(𝐹𝑚)))) +𝑒 (𝐸 / (2↑(1st ‘(𝐹𝑚)))))} ⊆ (𝐶‘(𝐴‘(1st ‘(𝐹𝑚))))
211210a1i 11 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ ℕ) → {𝑖 ∈ (𝐶‘(𝐴‘(1st ‘(𝐹𝑚)))) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴‘(1st ‘(𝐹𝑚)))) +𝑒 (𝐸 / (2↑(1st ‘(𝐹𝑚)))))} ⊆ (𝐶‘(𝐴‘(1st ‘(𝐹𝑚)))))
212209, 211eqsstrd 4002 . . . . . . . . . . 11 ((𝜑𝑚 ∈ ℕ) → ((𝐷‘(𝐴‘(1st ‘(𝐹𝑚))))‘(𝐸 / (2↑(1st ‘(𝐹𝑚))))) ⊆ (𝐶‘(𝐴‘(1st ‘(𝐹𝑚)))))
21337anbi2d 628 . . . . . . . . . . . . . 14 (𝑛 = (1st ‘(𝐹𝑚)) → ((𝜑𝑛 ∈ ℕ) ↔ (𝜑 ∧ (1st ‘(𝐹𝑚)) ∈ ℕ)))
214 2fveq3 6668 . . . . . . . . . . . . . . . 16 (𝑛 = (1st ‘(𝐹𝑚)) → (𝐷‘(𝐴𝑛)) = (𝐷‘(𝐴‘(1st ‘(𝐹𝑚)))))
215 oveq2 7153 . . . . . . . . . . . . . . . . 17 (𝑛 = (1st ‘(𝐹𝑚)) → (2↑𝑛) = (2↑(1st ‘(𝐹𝑚))))
216215oveq2d 7161 . . . . . . . . . . . . . . . 16 (𝑛 = (1st ‘(𝐹𝑚)) → (𝐸 / (2↑𝑛)) = (𝐸 / (2↑(1st ‘(𝐹𝑚)))))
217214, 216fveq12d 6670 . . . . . . . . . . . . . . 15 (𝑛 = (1st ‘(𝐹𝑚)) → ((𝐷‘(𝐴𝑛))‘(𝐸 / (2↑𝑛))) = ((𝐷‘(𝐴‘(1st ‘(𝐹𝑚))))‘(𝐸 / (2↑(1st ‘(𝐹𝑚))))))
21839, 217eleq12d 2904 . . . . . . . . . . . . . 14 (𝑛 = (1st ‘(𝐹𝑚)) → ((𝐼𝑛) ∈ ((𝐷‘(𝐴𝑛))‘(𝐸 / (2↑𝑛))) ↔ (𝐼‘(1st ‘(𝐹𝑚))) ∈ ((𝐷‘(𝐴‘(1st ‘(𝐹𝑚))))‘(𝐸 / (2↑(1st ‘(𝐹𝑚)))))))
219213, 218imbi12d 346 . . . . . . . . . . . . 13 (𝑛 = (1st ‘(𝐹𝑚)) → (((𝜑𝑛 ∈ ℕ) → (𝐼𝑛) ∈ ((𝐷‘(𝐴𝑛))‘(𝐸 / (2↑𝑛)))) ↔ ((𝜑 ∧ (1st ‘(𝐹𝑚)) ∈ ℕ) → (𝐼‘(1st ‘(𝐹𝑚))) ∈ ((𝐷‘(𝐴‘(1st ‘(𝐹𝑚))))‘(𝐸 / (2↑(1st ‘(𝐹𝑚))))))))
22036, 219, 86vtocl 3557 . . . . . . . . . . . 12 ((𝜑 ∧ (1st ‘(𝐹𝑚)) ∈ ℕ) → (𝐼‘(1st ‘(𝐹𝑚))) ∈ ((𝐷‘(𝐴‘(1st ‘(𝐹𝑚))))‘(𝐸 / (2↑(1st ‘(𝐹𝑚))))))
22117, 27, 220syl2anc 584 . . . . . . . . . . 11 ((𝜑𝑚 ∈ ℕ) → (𝐼‘(1st ‘(𝐹𝑚))) ∈ ((𝐷‘(𝐴‘(1st ‘(𝐹𝑚))))‘(𝐸 / (2↑(1st ‘(𝐹𝑚))))))
222212, 221sseldd 3965 . . . . . . . . . 10 ((𝜑𝑚 ∈ ℕ) → (𝐼‘(1st ‘(𝐹𝑚))) ∈ (𝐶‘(𝐴‘(1st ‘(𝐹𝑚)))))
223184, 222sseldd 3965 . . . . . . . . 9 ((𝜑𝑚 ∈ ℕ) → (𝐼‘(1st ‘(𝐹𝑚))) ∈ (((ℝ × ℝ) ↑m 𝑋) ↑m ℕ))
224 elmapfn 8418 . . . . . . . . 9 ((𝐼‘(1st ‘(𝐹𝑚))) ∈ (((ℝ × ℝ) ↑m 𝑋) ↑m ℕ) → (𝐼‘(1st ‘(𝐹𝑚))) Fn ℕ)
225223, 224syl 17 . . . . . . . 8 ((𝜑𝑚 ∈ ℕ) → (𝐼‘(1st ‘(𝐹𝑚))) Fn ℕ)
226 elmapi 8417 . . . . . . . . . . 11 ((𝐼‘(1st ‘(𝐹𝑚))) ∈ (((ℝ × ℝ) ↑m 𝑋) ↑m ℕ) → (𝐼‘(1st ‘(𝐹𝑚))):ℕ⟶((ℝ × ℝ) ↑m 𝑋))
227223, 226syl 17 . . . . . . . . . 10 ((𝜑𝑚 ∈ ℕ) → (𝐼‘(1st ‘(𝐹𝑚))):ℕ⟶((ℝ × ℝ) ↑m 𝑋))
228227ffvelrnda 6843 . . . . . . . . 9 (((𝜑𝑚 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → ((𝐼‘(1st ‘(𝐹𝑚)))‘𝑗) ∈ ((ℝ × ℝ) ↑m 𝑋))
229228ralrimiva 3179 . . . . . . . 8 ((𝜑𝑚 ∈ ℕ) → ∀𝑗 ∈ ℕ ((𝐼‘(1st ‘(𝐹𝑚)))‘𝑗) ∈ ((ℝ × ℝ) ↑m 𝑋))
230225, 229jca 512 . . . . . . 7 ((𝜑𝑚 ∈ ℕ) → ((𝐼‘(1st ‘(𝐹𝑚))) Fn ℕ ∧ ∀𝑗 ∈ ℕ ((𝐼‘(1st ‘(𝐹𝑚)))‘𝑗) ∈ ((ℝ × ℝ) ↑m 𝑋)))
231 ffnfv 6874 . . . . . . 7 ((𝐼‘(1st ‘(𝐹𝑚))):ℕ⟶((ℝ × ℝ) ↑m 𝑋) ↔ ((𝐼‘(1st ‘(𝐹𝑚))) Fn ℕ ∧ ∀𝑗 ∈ ℕ ((𝐼‘(1st ‘(𝐹𝑚)))‘𝑗) ∈ ((ℝ × ℝ) ↑m 𝑋)))
232230, 231sylibr 235 . . . . . 6 ((𝜑𝑚 ∈ ℕ) → (𝐼‘(1st ‘(𝐹𝑚))):ℕ⟶((ℝ × ℝ) ↑m 𝑋))
233232, 29ffvelrnd 6844 . . . . 5 ((𝜑𝑚 ∈ ℕ) → ((𝐼‘(1st ‘(𝐹𝑚)))‘(2nd ‘(𝐹𝑚))) ∈ ((ℝ × ℝ) ↑m 𝑋))
234233, 109fmptd 6870 . . . 4 (𝜑𝐺:ℕ⟶((ℝ × ℝ) ↑m 𝑋))
235 simpl 483 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → 𝜑)
23686, 82eleqtrd 2912 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → (𝐼𝑛) ∈ {𝑖 ∈ (𝐶‘(𝐴𝑛)) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛)))})
23783, 236sseldi 3962 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → (𝐼𝑛) ∈ (𝐶‘(𝐴𝑛)))
238 simp3 1130 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ ∧ (𝐼𝑛) ∈ (𝐶‘(𝐴𝑛))) → (𝐼𝑛) ∈ (𝐶‘(𝐴𝑛)))
239493adant3 1124 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ ∧ (𝐼𝑛) ∈ (𝐶‘(𝐴𝑛))) → (𝐶‘(𝐴𝑛)) = { ∈ (((ℝ × ℝ) ↑m 𝑋) ↑m ℕ) ∣ (𝐴𝑛) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘)})
240238, 239eleqtrd 2912 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ ∧ (𝐼𝑛) ∈ (𝐶‘(𝐴𝑛))) → (𝐼𝑛) ∈ { ∈ (((ℝ × ℝ) ↑m 𝑋) ↑m ℕ) ∣ (𝐴𝑛) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘)})
241 fveq1 6662 . . . . . . . . . . . . . . . . 17 ( = (𝐼𝑛) → (𝑗) = ((𝐼𝑛)‘𝑗))
242241coeq2d 5726 . . . . . . . . . . . . . . . 16 ( = (𝐼𝑛) → ([,) ∘ (𝑗)) = ([,) ∘ ((𝐼𝑛)‘𝑗)))
243242fveq1d 6665 . . . . . . . . . . . . . . 15 ( = (𝐼𝑛) → (([,) ∘ (𝑗))‘𝑘) = (([,) ∘ ((𝐼𝑛)‘𝑗))‘𝑘))
244243ixpeq2dv 8465 . . . . . . . . . . . . . 14 ( = (𝐼𝑛) → X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘) = X𝑘𝑋 (([,) ∘ ((𝐼𝑛)‘𝑗))‘𝑘))
245244iuneq2d 4939 . . . . . . . . . . . . 13 ( = (𝐼𝑛) → 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘) = 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ ((𝐼𝑛)‘𝑗))‘𝑘))
246245sseq2d 3996 . . . . . . . . . . . 12 ( = (𝐼𝑛) → ((𝐴𝑛) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘) ↔ (𝐴𝑛) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ ((𝐼𝑛)‘𝑗))‘𝑘)))
247246elrab 3677 . . . . . . . . . . 11 ((𝐼𝑛) ∈ { ∈ (((ℝ × ℝ) ↑m 𝑋) ↑m ℕ) ∣ (𝐴𝑛) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘)} ↔ ((𝐼𝑛) ∈ (((ℝ × ℝ) ↑m 𝑋) ↑m ℕ) ∧ (𝐴𝑛) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ ((𝐼𝑛)‘𝑗))‘𝑘)))
248240, 247sylib 219 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ ∧ (𝐼𝑛) ∈ (𝐶‘(𝐴𝑛))) → ((𝐼𝑛) ∈ (((ℝ × ℝ) ↑m 𝑋) ↑m ℕ) ∧ (𝐴𝑛) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ ((𝐼𝑛)‘𝑗))‘𝑘)))
249248simprd 496 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ ∧ (𝐼𝑛) ∈ (𝐶‘(𝐴𝑛))) → (𝐴𝑛) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ ((𝐼𝑛)‘𝑗))‘𝑘))
250235, 4, 237, 249syl3anc 1363 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → (𝐴𝑛) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ ((𝐼𝑛)‘𝑗))‘𝑘))
251 f1ofo 6615 . . . . . . . . . . . . . 14 (𝐹:ℕ–1-1-onto→(ℕ × ℕ) → 𝐹:ℕ–onto→(ℕ × ℕ))
25220, 251syl 17 . . . . . . . . . . . . 13 (𝜑𝐹:ℕ–onto→(ℕ × ℕ))
253252ad2antrr 722 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → 𝐹:ℕ–onto→(ℕ × ℕ))
254 opelxpi 5585 . . . . . . . . . . . . 13 ((𝑛 ∈ ℕ ∧ 𝑗 ∈ ℕ) → ⟨𝑛, 𝑗⟩ ∈ (ℕ × ℕ))
2554, 254sylan 580 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → ⟨𝑛, 𝑗⟩ ∈ (ℕ × ℕ))
256 foelrni 6720 . . . . . . . . . . . 12 ((𝐹:ℕ–onto→(ℕ × ℕ) ∧ ⟨𝑛, 𝑗⟩ ∈ (ℕ × ℕ)) → ∃𝑚 ∈ ℕ (𝐹𝑚) = ⟨𝑛, 𝑗⟩)
257253, 255, 256syl2anc 584 . . . . . . . . . . 11 (((𝜑𝑛 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → ∃𝑚 ∈ ℕ (𝐹𝑚) = ⟨𝑛, 𝑗⟩)
258 nfv 1906 . . . . . . . . . . . 12 𝑚((𝜑𝑛 ∈ ℕ) ∧ 𝑗 ∈ ℕ)
259 nfre1 3303 . . . . . . . . . . . 12 𝑚𝑚 ∈ {𝑖 ∈ ℕ ∣ (1st ‘(𝐹𝑖)) = 𝑛}X𝑘𝑋 (([,) ∘ ((𝐼𝑛)‘𝑗))‘𝑘) ⊆ X𝑘𝑋 (([,) ∘ (𝐺𝑚))‘𝑘)
260 simpl 483 . . . . . . . . . . . . . . . . 17 ((𝑚 ∈ ℕ ∧ (𝐹𝑚) = ⟨𝑛, 𝑗⟩) → 𝑚 ∈ ℕ)
261 fveq2 6663 . . . . . . . . . . . . . . . . . . 19 ((𝐹𝑚) = ⟨𝑛, 𝑗⟩ → (1st ‘(𝐹𝑚)) = (1st ‘⟨𝑛, 𝑗⟩))
262 op1stg 7690 . . . . . . . . . . . . . . . . . . . . 21 ((𝑛 ∈ V ∧ 𝑗 ∈ V) → (1st ‘⟨𝑛, 𝑗⟩) = 𝑛)
263262el2v 3499 . . . . . . . . . . . . . . . . . . . 20 (1st ‘⟨𝑛, 𝑗⟩) = 𝑛
264263a1i 11 . . . . . . . . . . . . . . . . . . 19 ((𝐹𝑚) = ⟨𝑛, 𝑗⟩ → (1st ‘⟨𝑛, 𝑗⟩) = 𝑛)
265261, 264eqtrd 2853 . . . . . . . . . . . . . . . . . 18 ((𝐹𝑚) = ⟨𝑛, 𝑗⟩ → (1st ‘(𝐹𝑚)) = 𝑛)
266265adantl 482 . . . . . . . . . . . . . . . . 17 ((𝑚 ∈ ℕ ∧ (𝐹𝑚) = ⟨𝑛, 𝑗⟩) → (1st ‘(𝐹𝑚)) = 𝑛)
267260, 266jca 512 . . . . . . . . . . . . . . . 16 ((𝑚 ∈ ℕ ∧ (𝐹𝑚) = ⟨𝑛, 𝑗⟩) → (𝑚 ∈ ℕ ∧ (1st ‘(𝐹𝑚)) = 𝑛))
268 2fveq3 6668 . . . . . . . . . . . . . . . . . 18 (𝑖 = 𝑚 → (1st ‘(𝐹𝑖)) = (1st ‘(𝐹𝑚)))
269268eqeq1d 2820 . . . . . . . . . . . . . . . . 17 (𝑖 = 𝑚 → ((1st ‘(𝐹𝑖)) = 𝑛 ↔ (1st ‘(𝐹𝑚)) = 𝑛))
270269elrab 3677 . . . . . . . . . . . . . . . 16 (𝑚 ∈ {𝑖 ∈ ℕ ∣ (1st ‘(𝐹𝑖)) = 𝑛} ↔ (𝑚 ∈ ℕ ∧ (1st ‘(𝐹𝑚)) = 𝑛))
271267, 270sylibr 235 . . . . . . . . . . . . . . 15 ((𝑚 ∈ ℕ ∧ (𝐹𝑚) = ⟨𝑛, 𝑗⟩) → 𝑚 ∈ {𝑖 ∈ ℕ ∣ (1st ‘(𝐹𝑖)) = 𝑛})
2722713adant1 1122 . . . . . . . . . . . . . 14 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑗 ∈ ℕ) ∧ 𝑚 ∈ ℕ ∧ (𝐹𝑚) = ⟨𝑛, 𝑗⟩) → 𝑚 ∈ {𝑖 ∈ ℕ ∣ (1st ‘(𝐹𝑖)) = 𝑛})
273260, 111syl 17 . . . . . . . . . . . . . . . . . . . 20 ((𝑚 ∈ ℕ ∧ (𝐹𝑚) = ⟨𝑛, 𝑗⟩) → (𝐺𝑚) = ((𝐼‘(1st ‘(𝐹𝑚)))‘(2nd ‘(𝐹𝑚))))
274265fveq2d 6667 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐹𝑚) = ⟨𝑛, 𝑗⟩ → (𝐼‘(1st ‘(𝐹𝑚))) = (𝐼𝑛))
275 vex 3495 . . . . . . . . . . . . . . . . . . . . . . 23 𝑛 ∈ V
276 vex 3495 . . . . . . . . . . . . . . . . . . . . . . 23 𝑗 ∈ V
277275, 276op2ndd 7689 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐹𝑚) = ⟨𝑛, 𝑗⟩ → (2nd ‘(𝐹𝑚)) = 𝑗)
278274, 277fveq12d 6670 . . . . . . . . . . . . . . . . . . . . 21 ((𝐹𝑚) = ⟨𝑛, 𝑗⟩ → ((𝐼‘(1st ‘(𝐹𝑚)))‘(2nd ‘(𝐹𝑚))) = ((𝐼𝑛)‘𝑗))
279278adantl 482 . . . . . . . . . . . . . . . . . . . 20 ((𝑚 ∈ ℕ ∧ (𝐹𝑚) = ⟨𝑛, 𝑗⟩) → ((𝐼‘(1st ‘(𝐹𝑚)))‘(2nd ‘(𝐹𝑚))) = ((𝐼𝑛)‘𝑗))
280273, 279eqtr2d 2854 . . . . . . . . . . . . . . . . . . 19 ((𝑚 ∈ ℕ ∧ (𝐹𝑚) = ⟨𝑛, 𝑗⟩) → ((𝐼𝑛)‘𝑗) = (𝐺𝑚))
281280coeq2d 5726 . . . . . . . . . . . . . . . . . 18 ((𝑚 ∈ ℕ ∧ (𝐹𝑚) = ⟨𝑛, 𝑗⟩) → ([,) ∘ ((𝐼𝑛)‘𝑗)) = ([,) ∘ (𝐺𝑚)))
282281fveq1d 6665 . . . . . . . . . . . . . . . . 17 ((𝑚 ∈ ℕ ∧ (𝐹𝑚) = ⟨𝑛, 𝑗⟩) → (([,) ∘ ((𝐼𝑛)‘𝑗))‘𝑘) = (([,) ∘ (𝐺𝑚))‘𝑘))
283282ixpeq2dv 8465 . . . . . . . . . . . . . . . 16 ((𝑚 ∈ ℕ ∧ (𝐹𝑚) = ⟨𝑛, 𝑗⟩) → X𝑘𝑋 (([,) ∘ ((𝐼𝑛)‘𝑗))‘𝑘) = X𝑘𝑋 (([,) ∘ (𝐺𝑚))‘𝑘))
284 eqimss 4020 . . . . . . . . . . . . . . . 16 (X𝑘𝑋 (([,) ∘ ((𝐼𝑛)‘𝑗))‘𝑘) = X𝑘𝑋 (([,) ∘ (𝐺𝑚))‘𝑘) → X𝑘𝑋 (([,) ∘ ((𝐼𝑛)‘𝑗))‘𝑘) ⊆ X𝑘𝑋 (([,) ∘ (𝐺𝑚))‘𝑘))
285283, 284syl 17 . . . . . . . . . . . . . . 15 ((𝑚 ∈ ℕ ∧ (𝐹𝑚) = ⟨𝑛, 𝑗⟩) → X𝑘𝑋 (([,) ∘ ((𝐼𝑛)‘𝑗))‘𝑘) ⊆ X𝑘𝑋 (([,) ∘ (𝐺𝑚))‘𝑘))
2862853adant1 1122 . . . . . . . . . . . . . 14 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑗 ∈ ℕ) ∧ 𝑚 ∈ ℕ ∧ (𝐹𝑚) = ⟨𝑛, 𝑗⟩) → X𝑘𝑋 (([,) ∘ ((𝐼𝑛)‘𝑗))‘𝑘) ⊆ X𝑘𝑋 (([,) ∘ (𝐺𝑚))‘𝑘))
287 rspe 3301 . . . . . . . . . . . . . 14 ((𝑚 ∈ {𝑖 ∈ ℕ ∣ (1st ‘(𝐹𝑖)) = 𝑛} ∧ X𝑘𝑋 (([,) ∘ ((𝐼𝑛)‘𝑗))‘𝑘) ⊆ X𝑘𝑋 (([,) ∘ (𝐺𝑚))‘𝑘)) → ∃𝑚 ∈ {𝑖 ∈ ℕ ∣ (1st ‘(𝐹𝑖)) = 𝑛}X𝑘𝑋 (([,) ∘ ((𝐼𝑛)‘𝑗))‘𝑘) ⊆ X𝑘𝑋 (([,) ∘ (𝐺𝑚))‘𝑘))
288272, 286, 287syl2anc 584 . . . . . . . . . . . . 13 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑗 ∈ ℕ) ∧ 𝑚 ∈ ℕ ∧ (𝐹𝑚) = ⟨𝑛, 𝑗⟩) → ∃𝑚 ∈ {𝑖 ∈ ℕ ∣ (1st ‘(𝐹𝑖)) = 𝑛}X𝑘𝑋 (([,) ∘ ((𝐼𝑛)‘𝑗))‘𝑘) ⊆ X𝑘𝑋 (([,) ∘ (𝐺𝑚))‘𝑘))
2892883exp 1111 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → (𝑚 ∈ ℕ → ((𝐹𝑚) = ⟨𝑛, 𝑗⟩ → ∃𝑚 ∈ {𝑖 ∈ ℕ ∣ (1st ‘(𝐹𝑖)) = 𝑛}X𝑘𝑋 (([,) ∘ ((𝐼𝑛)‘𝑗))‘𝑘) ⊆ X𝑘𝑋 (([,) ∘ (𝐺𝑚))‘𝑘))))
290258, 259, 289rexlimd 3314 . . . . . . . . . . 11 (((𝜑𝑛 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → (∃𝑚 ∈ ℕ (𝐹𝑚) = ⟨𝑛, 𝑗⟩ → ∃𝑚 ∈ {𝑖 ∈ ℕ ∣ (1st ‘(𝐹𝑖)) = 𝑛}X𝑘𝑋 (([,) ∘ ((𝐼𝑛)‘𝑗))‘𝑘) ⊆ X𝑘𝑋 (([,) ∘ (𝐺𝑚))‘𝑘)))
291257, 290mpd 15 . . . . . . . . . 10 (((𝜑𝑛 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → ∃𝑚 ∈ {𝑖 ∈ ℕ ∣ (1st ‘(𝐹𝑖)) = 𝑛}X𝑘𝑋 (([,) ∘ ((𝐼𝑛)‘𝑗))‘𝑘) ⊆ X𝑘𝑋 (([,) ∘ (𝐺𝑚))‘𝑘))
292291ralrimiva 3179 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → ∀𝑗 ∈ ℕ ∃𝑚 ∈ {𝑖 ∈ ℕ ∣ (1st ‘(𝐹𝑖)) = 𝑛}X𝑘𝑋 (([,) ∘ ((𝐼𝑛)‘𝑗))‘𝑘) ⊆ X𝑘𝑋 (([,) ∘ (𝐺𝑚))‘𝑘))
293 iunss2 4964 . . . . . . . . 9 (∀𝑗 ∈ ℕ ∃𝑚 ∈ {𝑖 ∈ ℕ ∣ (1st ‘(𝐹𝑖)) = 𝑛}X𝑘𝑋 (([,) ∘ ((𝐼𝑛)‘𝑗))‘𝑘) ⊆ X𝑘𝑋 (([,) ∘ (𝐺𝑚))‘𝑘) → 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ ((𝐼𝑛)‘𝑗))‘𝑘) ⊆ 𝑚 ∈ {𝑖 ∈ ℕ ∣ (1st ‘(𝐹𝑖)) = 𝑛}X𝑘𝑋 (([,) ∘ (𝐺𝑚))‘𝑘))
294292, 293syl 17 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ ((𝐼𝑛)‘𝑗))‘𝑘) ⊆ 𝑚 ∈ {𝑖 ∈ ℕ ∣ (1st ‘(𝐹𝑖)) = 𝑛}X𝑘𝑋 (([,) ∘ (𝐺𝑚))‘𝑘))
295250, 294sstrd 3974 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → (𝐴𝑛) ⊆ 𝑚 ∈ {𝑖 ∈ ℕ ∣ (1st ‘(𝐹𝑖)) = 𝑛}X𝑘𝑋 (([,) ∘ (𝐺𝑚))‘𝑘))
296 ssrab2 4053 . . . . . . . . 9 {𝑖 ∈ ℕ ∣ (1st ‘(𝐹𝑖)) = 𝑛} ⊆ ℕ
297 iunss1 4924 . . . . . . . . 9 ({𝑖 ∈ ℕ ∣ (1st ‘(𝐹𝑖)) = 𝑛} ⊆ ℕ → 𝑚 ∈ {𝑖 ∈ ℕ ∣ (1st ‘(𝐹𝑖)) = 𝑛}X𝑘𝑋 (([,) ∘ (𝐺𝑚))‘𝑘) ⊆ 𝑚 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝐺𝑚))‘𝑘))
298296, 297ax-mp 5 . . . . . . . 8 𝑚 ∈ {𝑖 ∈ ℕ ∣ (1st ‘(𝐹𝑖)) = 𝑛}X𝑘𝑋 (([,) ∘ (𝐺𝑚))‘𝑘) ⊆ 𝑚 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝐺𝑚))‘𝑘)
299298a1i 11 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → 𝑚 ∈ {𝑖 ∈ ℕ ∣ (1st ‘(𝐹𝑖)) = 𝑛}X𝑘𝑋 (([,) ∘ (𝐺𝑚))‘𝑘) ⊆ 𝑚 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝐺𝑚))‘𝑘))
300295, 299sstrd 3974 . . . . . 6 ((𝜑𝑛 ∈ ℕ) → (𝐴𝑛) ⊆ 𝑚 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝐺𝑚))‘𝑘))
301300ralrimiva 3179 . . . . 5 (𝜑 → ∀𝑛 ∈ ℕ (𝐴𝑛) ⊆ 𝑚 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝐺𝑚))‘𝑘))
302 iunss 4960 . . . . 5 ( 𝑛 ∈ ℕ (𝐴𝑛) ⊆ 𝑚 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝐺𝑚))‘𝑘) ↔ ∀𝑛 ∈ ℕ (𝐴𝑛) ⊆ 𝑚 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝐺𝑚))‘𝑘))
303301, 302sylibr 235 . . . 4 (𝜑 𝑛 ∈ ℕ (𝐴𝑛) ⊆ 𝑚 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝐺𝑚))‘𝑘))
3041, 126, 19, 234, 303ovnlecvr 42717 . . 3 (𝜑 → ((voln*‘𝑋)‘ 𝑛 ∈ ℕ (𝐴𝑛)) ≤ (Σ^‘(𝑚 ∈ ℕ ↦ (𝐿‘(𝐺𝑚)))))
305112fveq2d 6667 . . . . . . 7 ((𝜑𝑚 ∈ ℕ) → (𝐿‘(𝐺𝑚)) = (𝐿‘((𝐼‘(1st ‘(𝐹𝑚)))‘(2nd ‘(𝐹𝑚)))))
306305mpteq2dva 5152 . . . . . 6 (𝜑 → (𝑚 ∈ ℕ ↦ (𝐿‘(𝐺𝑚))) = (𝑚 ∈ ℕ ↦ (𝐿‘((𝐼‘(1st ‘(𝐹𝑚)))‘(2nd ‘(𝐹𝑚))))))
307306fveq2d 6667 . . . . 5 (𝜑 → (Σ^‘(𝑚 ∈ ℕ ↦ (𝐿‘(𝐺𝑚)))) = (Σ^‘(𝑚 ∈ ℕ ↦ (𝐿‘((𝐼‘(1st ‘(𝐹𝑚)))‘(2nd ‘(𝐹𝑚)))))))
308 nfv 1906 . . . . . 6 𝑝𝜑
309 2fveq3 6668 . . . . . . . 8 (𝑝 = (𝐹𝑚) → (𝐼‘(1st𝑝)) = (𝐼‘(1st ‘(𝐹𝑚))))
310 fveq2 6663 . . . . . . . 8 (𝑝 = (𝐹𝑚) → (2nd𝑝) = (2nd ‘(𝐹𝑚)))
311309, 310fveq12d 6670 . . . . . . 7 (𝑝 = (𝐹𝑚) → ((𝐼‘(1st𝑝))‘(2nd𝑝)) = ((𝐼‘(1st ‘(𝐹𝑚)))‘(2nd ‘(𝐹𝑚))))
312311fveq2d 6667 . . . . . 6 (𝑝 = (𝐹𝑚) → (𝐿‘((𝐼‘(1st𝑝))‘(2nd𝑝))) = (𝐿‘((𝐼‘(1st ‘(𝐹𝑚)))‘(2nd ‘(𝐹𝑚)))))
313 eqidd 2819 . . . . . 6 ((𝜑𝑚 ∈ ℕ) → (𝐹𝑚) = (𝐹𝑚))
314 nfv 1906 . . . . . . . 8 𝑘(𝜑𝑝 ∈ (ℕ × ℕ))
3151adantr 481 . . . . . . . 8 ((𝜑𝑝 ∈ (ℕ × ℕ)) → 𝑋 ∈ Fin)
316 simpl 483 . . . . . . . . 9 ((𝜑𝑝 ∈ (ℕ × ℕ)) → 𝜑)
317 xp1st 7710 . . . . . . . . . 10 (𝑝 ∈ (ℕ × ℕ) → (1st𝑝) ∈ ℕ)
318317adantl 482 . . . . . . . . 9 ((𝜑𝑝 ∈ (ℕ × ℕ)) → (1st𝑝) ∈ ℕ)
319 xp2nd 7711 . . . . . . . . . 10 (𝑝 ∈ (ℕ × ℕ) → (2nd𝑝) ∈ ℕ)
320319adantl 482 . . . . . . . . 9 ((𝜑𝑝 ∈ (ℕ × ℕ)) → (2nd𝑝) ∈ ℕ)
321 fvex 6676 . . . . . . . . . 10 (2nd𝑝) ∈ V
322 eleq1 2897 . . . . . . . . . . . 12 (𝑗 = (2nd𝑝) → (𝑗 ∈ ℕ ↔ (2nd𝑝) ∈ ℕ))
3233223anbi3d 1433 . . . . . . . . . . 11 (𝑗 = (2nd𝑝) → ((𝜑 ∧ (1st𝑝) ∈ ℕ ∧ 𝑗 ∈ ℕ) ↔ (𝜑 ∧ (1st𝑝) ∈ ℕ ∧ (2nd𝑝) ∈ ℕ)))
324 fveq2 6663 . . . . . . . . . . . 12 (𝑗 = (2nd𝑝) → ((𝐼‘(1st𝑝))‘𝑗) = ((𝐼‘(1st𝑝))‘(2nd𝑝)))
325324feq1d 6492 . . . . . . . . . . 11 (𝑗 = (2nd𝑝) → (((𝐼‘(1st𝑝))‘𝑗):𝑋⟶(ℝ × ℝ) ↔ ((𝐼‘(1st𝑝))‘(2nd𝑝)):𝑋⟶(ℝ × ℝ)))
326323, 325imbi12d 346 . . . . . . . . . 10 (𝑗 = (2nd𝑝) → (((𝜑 ∧ (1st𝑝) ∈ ℕ ∧ 𝑗 ∈ ℕ) → ((𝐼‘(1st𝑝))‘𝑗):𝑋⟶(ℝ × ℝ)) ↔ ((𝜑 ∧ (1st𝑝) ∈ ℕ ∧ (2nd𝑝) ∈ ℕ) → ((𝐼‘(1st𝑝))‘(2nd𝑝)):𝑋⟶(ℝ × ℝ))))
327 fvex 6676 . . . . . . . . . . 11 (1st𝑝) ∈ V
328 eleq1 2897 . . . . . . . . . . . . 13 (𝑛 = (1st𝑝) → (𝑛 ∈ ℕ ↔ (1st𝑝) ∈ ℕ))
3293283anbi2d 1432 . . . . . . . . . . . 12 (𝑛 = (1st𝑝) → ((𝜑𝑛 ∈ ℕ ∧ 𝑗 ∈ ℕ) ↔ (𝜑 ∧ (1st𝑝) ∈ ℕ ∧ 𝑗 ∈ ℕ)))
330 fveq2 6663 . . . . . . . . . . . . . 14 (𝑛 = (1st𝑝) → (𝐼𝑛) = (𝐼‘(1st𝑝)))
331330fveq1d 6665 . . . . . . . . . . . . 13 (𝑛 = (1st𝑝) → ((𝐼𝑛)‘𝑗) = ((𝐼‘(1st𝑝))‘𝑗))
332331feq1d 6492 . . . . . . . . . . . 12 (𝑛 = (1st𝑝) → (((𝐼𝑛)‘𝑗):𝑋⟶(ℝ × ℝ) ↔ ((𝐼‘(1st𝑝))‘𝑗):𝑋⟶(ℝ × ℝ)))
333329, 332imbi12d 346 . . . . . . . . . . 11 (𝑛 = (1st𝑝) → (((𝜑𝑛 ∈ ℕ ∧ 𝑗 ∈ ℕ) → ((𝐼𝑛)‘𝑗):𝑋⟶(ℝ × ℝ)) ↔ ((𝜑 ∧ (1st𝑝) ∈ ℕ ∧ 𝑗 ∈ ℕ) → ((𝐼‘(1st𝑝))‘𝑗):𝑋⟶(ℝ × ℝ))))
334327, 333, 102vtocl 3557 . . . . . . . . . 10 ((𝜑 ∧ (1st𝑝) ∈ ℕ ∧ 𝑗 ∈ ℕ) → ((𝐼‘(1st𝑝))‘𝑗):𝑋⟶(ℝ × ℝ))
335321, 326, 334vtocl 3557 . . . . . . . . 9 ((𝜑 ∧ (1st𝑝) ∈ ℕ ∧ (2nd𝑝) ∈ ℕ) → ((𝐼‘(1st𝑝))‘(2nd𝑝)):𝑋⟶(ℝ × ℝ))
336316, 318, 320, 335syl3anc 1363 . . . . . . . 8 ((𝜑𝑝 ∈ (ℕ × ℕ)) → ((𝐼‘(1st𝑝))‘(2nd𝑝)):𝑋⟶(ℝ × ℝ))
337314, 315, 19, 336hoiprodcl2 42714 . . . . . . 7 ((𝜑𝑝 ∈ (ℕ × ℕ)) → (𝐿‘((𝐼‘(1st𝑝))‘(2nd𝑝))) ∈ (0[,)+∞))
33815, 337sseldi 3962 . . . . . 6 ((𝜑𝑝 ∈ (ℕ × ℕ)) → (𝐿‘((𝐼‘(1st𝑝))‘(2nd𝑝))) ∈ (0[,]+∞))
339308, 12, 312, 14, 20, 313, 338sge0f1o 42541 . . . . 5 (𝜑 → (Σ^‘(𝑝 ∈ (ℕ × ℕ) ↦ (𝐿‘((𝐼‘(1st𝑝))‘(2nd𝑝))))) = (Σ^‘(𝑚 ∈ ℕ ↦ (𝐿‘((𝐼‘(1st ‘(𝐹𝑚)))‘(2nd ‘(𝐹𝑚)))))))
340307, 339eqtr4d 2856 . . . 4 (𝜑 → (Σ^‘(𝑚 ∈ ℕ ↦ (𝐿‘(𝐺𝑚)))) = (Σ^‘(𝑝 ∈ (ℕ × ℕ) ↦ (𝐿‘((𝐼‘(1st𝑝))‘(2nd𝑝))))))
341 nfv 1906 . . . . . . 7 𝑗𝜑
342275, 276op1std 7688 . . . . . . . . . 10 (𝑝 = ⟨𝑛, 𝑗⟩ → (1st𝑝) = 𝑛)
343342fveq2d 6667 . . . . . . . . 9 (𝑝 = ⟨𝑛, 𝑗⟩ → (𝐼‘(1st𝑝)) = (𝐼𝑛))
344275, 276op2ndd 7689 . . . . . . . . 9 (𝑝 = ⟨𝑛, 𝑗⟩ → (2nd𝑝) = 𝑗)
345343, 344fveq12d 6670 . . . . . . . 8 (𝑝 = ⟨𝑛, 𝑗⟩ → ((𝐼‘(1st𝑝))‘(2nd𝑝)) = ((𝐼𝑛)‘𝑗))
346345fveq2d 6667 . . . . . . 7 (𝑝 = ⟨𝑛, 𝑗⟩ → (𝐿‘((𝐼‘(1st𝑝))‘(2nd𝑝))) = (𝐿‘((𝐼𝑛)‘𝑗)))
347 nfv 1906 . . . . . . . . . 10 𝑘((𝜑𝑛 ∈ ℕ) ∧ 𝑗 ∈ ℕ)
348123adantr 481 . . . . . . . . . 10 (((𝜑𝑛 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → 𝑋 ∈ Fin)
34993, 101syl 17 . . . . . . . . . 10 (((𝜑𝑛 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → ((𝐼𝑛)‘𝑗):𝑋⟶(ℝ × ℝ))
350347, 348, 19, 349hoiprodcl2 42714 . . . . . . . . 9 (((𝜑𝑛 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → (𝐿‘((𝐼𝑛)‘𝑗)) ∈ (0[,)+∞))
35115, 350sseldi 3962 . . . . . . . 8 (((𝜑𝑛 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → (𝐿‘((𝐼𝑛)‘𝑗)) ∈ (0[,]+∞))
3523513impa 1102 . . . . . . 7 ((𝜑𝑛 ∈ ℕ ∧ 𝑗 ∈ ℕ) → (𝐿‘((𝐼𝑛)‘𝑗)) ∈ (0[,]+∞))
353341, 346, 14, 14, 352sge0xp 42588 . . . . . 6 (𝜑 → (Σ^‘(𝑛 ∈ ℕ ↦ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘((𝐼𝑛)‘𝑗)))))) = (Σ^‘(𝑝 ∈ (ℕ × ℕ) ↦ (𝐿‘((𝐼‘(1st𝑝))‘(2nd𝑝))))))
354353eqcomd 2824 . . . . 5 (𝜑 → (Σ^‘(𝑝 ∈ (ℕ × ℕ) ↦ (𝐿‘((𝐼‘(1st𝑝))‘(2nd𝑝))))) = (Σ^‘(𝑛 ∈ ℕ ↦ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘((𝐼𝑛)‘𝑗)))))))
35513a1i 11 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → ℕ ∈ V)
356 eqid 2818 . . . . . . . 8 (𝑗 ∈ ℕ ↦ (𝐿‘((𝐼𝑛)‘𝑗))) = (𝑗 ∈ ℕ ↦ (𝐿‘((𝐼𝑛)‘𝑗)))
357351, 356fmptd 6870 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → (𝑗 ∈ ℕ ↦ (𝐿‘((𝐼𝑛)‘𝑗))):ℕ⟶(0[,]+∞))
358355, 357sge0cl 42540 . . . . . 6 ((𝜑𝑛 ∈ ℕ) → (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘((𝐼𝑛)‘𝑗)))) ∈ (0[,]+∞))
359 fveq1 6662 . . . . . . . . . . . . 13 (𝑖 = (𝐼𝑛) → (𝑖𝑗) = ((𝐼𝑛)‘𝑗))
360359fveq2d 6667 . . . . . . . . . . . 12 (𝑖 = (𝐼𝑛) → (𝐿‘(𝑖𝑗)) = (𝐿‘((𝐼𝑛)‘𝑗)))
361360mpteq2dv 5153 . . . . . . . . . . 11 (𝑖 = (𝐼𝑛) → (𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗))) = (𝑗 ∈ ℕ ↦ (𝐿‘((𝐼𝑛)‘𝑗))))
362361fveq2d 6667 . . . . . . . . . 10 (𝑖 = (𝐼𝑛) → (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) = (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘((𝐼𝑛)‘𝑗)))))
363362breq1d 5067 . . . . . . . . 9 (𝑖 = (𝐼𝑛) → ((Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛))) ↔ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘((𝐼𝑛)‘𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛)))))
364363elrab 3677 . . . . . . . 8 ((𝐼𝑛) ∈ {𝑖 ∈ (𝐶‘(𝐴𝑛)) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛)))} ↔ ((𝐼𝑛) ∈ (𝐶‘(𝐴𝑛)) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘((𝐼𝑛)‘𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛)))))
365236, 364sylib 219 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → ((𝐼𝑛) ∈ (𝐶‘(𝐴𝑛)) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘((𝐼𝑛)‘𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛)))))
366365simprd 496 . . . . . 6 ((𝜑𝑛 ∈ ℕ) → (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘((𝐼𝑛)‘𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛))))
367118, 14, 358, 173, 366sge0lempt 42569 . . . . 5 (𝜑 → (Σ^‘(𝑛 ∈ ℕ ↦ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘((𝐼𝑛)‘𝑗)))))) ≤ (Σ^‘(𝑛 ∈ ℕ ↦ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛))))))
368354, 367eqbrtrd 5079 . . . 4 (𝜑 → (Σ^‘(𝑝 ∈ (ℕ × ℕ) ↦ (𝐿‘((𝐼‘(1st𝑝))‘(2nd𝑝))))) ≤ (Σ^‘(𝑛 ∈ ℕ ↦ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛))))))
369340, 368eqbrtrd 5079 . . 3 (𝜑 → (Σ^‘(𝑚 ∈ ℕ ↦ (𝐿‘(𝐺𝑚)))) ≤ (Σ^‘(𝑛 ∈ ℕ ↦ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛))))))
37011, 117, 174, 304, 369xrletrd 12543 . 2 (𝜑 → ((voln*‘𝑋)‘ 𝑛 ∈ ℕ (𝐴𝑛)) ≤ (Σ^‘(𝑛 ∈ ℕ ↦ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛))))))
371118, 14, 160, 168sge0xadd 42594 . . 3 (𝜑 → (Σ^‘(𝑛 ∈ ℕ ↦ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛))))) = ((Σ^‘(𝑛 ∈ ℕ ↦ ((voln*‘𝑋)‘(𝐴𝑛)))) +𝑒^‘(𝑛 ∈ ℕ ↦ (𝐸 / (2↑𝑛))))))
372119a1i 11 . . . . . 6 (𝜑 → 0 ∈ ℝ*)
373121a1i 11 . . . . . 6 (𝜑 → +∞ ∈ ℝ*)
374145rexrd 10679 . . . . . 6 (𝜑𝐸 ∈ ℝ*)
37570rpge0d 12423 . . . . . 6 (𝜑 → 0 ≤ 𝐸)
376145ltpnfd 12504 . . . . . 6 (𝜑𝐸 < +∞)
377372, 373, 374, 375, 376elicod 12775 . . . . 5 (𝜑𝐸 ∈ (0[,)+∞))
378377sge0ad2en 42590 . . . 4 (𝜑 → (Σ^‘(𝑛 ∈ ℕ ↦ (𝐸 / (2↑𝑛)))) = 𝐸)
379378oveq2d 7161 . . 3 (𝜑 → ((Σ^‘(𝑛 ∈ ℕ ↦ ((voln*‘𝑋)‘(𝐴𝑛)))) +𝑒^‘(𝑛 ∈ ℕ ↦ (𝐸 / (2↑𝑛))))) = ((Σ^‘(𝑛 ∈ ℕ ↦ ((voln*‘𝑋)‘(𝐴𝑛)))) +𝑒 𝐸))
380371, 379eqtrd 2853 . 2 (𝜑 → (Σ^‘(𝑛 ∈ ℕ ↦ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛))))) = ((Σ^‘(𝑛 ∈ ℕ ↦ ((voln*‘𝑋)‘(𝐴𝑛)))) +𝑒 𝐸))
381370, 380breqtrd 5083 1 (𝜑 → ((voln*‘𝑋)‘ 𝑛 ∈ ℕ (𝐴𝑛)) ≤ ((Σ^‘(𝑛 ∈ ℕ ↦ ((voln*‘𝑋)‘(𝐴𝑛)))) +𝑒 𝐸))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  w3a 1079   = wceq 1528  wcel 2105  wne 3013  wral 3135  wrex 3136  {crab 3139  Vcvv 3492  wss 3933  c0 4288  ifcif 4463  𝒫 cpw 4535  cop 4563   ciun 4910   class class class wbr 5057  cmpt 5137   × cxp 5546  ccom 5552   Fn wfn 6343  wf 6344  ontowfo 6346  1-1-ontowf1o 6347  cfv 6348  (class class class)co 7145  1st c1st 7676  2nd c2nd 7677  m cmap 8395  Xcixp 8449  Fincfn 8497  infcinf 8893  cr 10524  0cc0 10525  +∞cpnf 10660  *cxr 10662   < clt 10663  cle 10664   / cdiv 11285  cn 11626  2c2 11680  +crp 12377   +𝑒 cxad 12493  [,)cico 12728  [,]cicc 12729  cexp 13417  cprod 15247  volcvol 23991  Σ^csumge0 42521  voln*covoln 42695
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-rep 5181  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7450  ax-inf2 9092  ax-ac2 9873  ax-cnex 10581  ax-resscn 10582  ax-1cn 10583  ax-icn 10584  ax-addcl 10585  ax-addrcl 10586  ax-mulcl 10587  ax-mulrcl 10588  ax-mulcom 10589  ax-addass 10590  ax-mulass 10591  ax-distr 10592  ax-i2m1 10593  ax-1ne0 10594  ax-1rid 10595  ax-rnegex 10596  ax-rrecex 10597  ax-cnre 10598  ax-pre-lttri 10599  ax-pre-lttrn 10600  ax-pre-ltadd 10601  ax-pre-mulgt0 10602  ax-pre-sup 10603  ax-addf 10604  ax-mulf 10605
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3or 1080  df-3an 1081  df-tru 1531  df-fal 1541  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ne 3014  df-nel 3121  df-ral 3140  df-rex 3141  df-reu 3142  df-rmo 3143  df-rab 3144  df-v 3494  df-sbc 3770  df-csb 3881  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-pss 3951  df-nul 4289  df-if 4464  df-pw 4537  df-sn 4558  df-pr 4560  df-tp 4562  df-op 4564  df-uni 4831  df-int 4868  df-iun 4912  df-disj 5023  df-br 5058  df-opab 5120  df-mpt 5138  df-tr 5164  df-id 5453  df-eprel 5458  df-po 5467  df-so 5468  df-fr 5507  df-se 5508  df-we 5509  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-pred 6141  df-ord 6187  df-on 6188  df-lim 6189  df-suc 6190  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-isom 6357  df-riota 7103  df-ov 7148  df-oprab 7149  df-mpo 7150  df-of 7398  df-om 7570  df-1st 7678  df-2nd 7679  df-tpos 7881  df-wrecs 7936  df-recs 7997  df-rdg 8035  df-1o 8091  df-2o 8092  df-oadd 8095  df-er 8278  df-map 8397  df-pm 8398  df-ixp 8450  df-en 8498  df-dom 8499  df-sdom 8500  df-fin 8501  df-fi 8863  df-sup 8894  df-inf 8895  df-oi 8962  df-dju 9318  df-card 9356  df-acn 9359  df-ac 9530  df-pnf 10665  df-mnf 10666  df-xr 10667  df-ltxr 10668  df-le 10669  df-sub 10860  df-neg 10861  df-div 11286  df-nn 11627  df-2 11688  df-3 11689  df-4 11690  df-5 11691  df-6 11692  df-7 11693  df-8 11694  df-9 11695  df-n0 11886  df-z 11970  df-dec 12087  df-uz 12232  df-q 12337  df-rp 12378  df-xneg 12495  df-xadd 12496  df-xmul 12497  df-ioo 12730  df-ico 12732  df-icc 12733  df-fz 12881  df-fzo 13022  df-fl 13150  df-seq 13358  df-exp 13418  df-hash 13679  df-cj 14446  df-re 14447  df-im 14448  df-sqrt 14582  df-abs 14583  df-clim 14833  df-rlim 14834  df-sum 15031  df-prod 15248  df-struct 16473  df-ndx 16474  df-slot 16475  df-base 16477  df-sets 16478  df-ress 16479  df-plusg 16566  df-mulr 16567  df-starv 16568  df-tset 16572  df-ple 16573  df-ds 16575  df-unif 16576  df-rest 16684  df-0g 16703  df-topgen 16705  df-mgm 17840  df-sgrp 17889  df-mnd 17900  df-grp 18044  df-minusg 18045  df-subg 18214  df-cmn 18837  df-abl 18838  df-mgp 19169  df-ur 19181  df-ring 19228  df-cring 19229  df-oppr 19302  df-dvdsr 19320  df-unit 19321  df-invr 19351  df-dvr 19362  df-drng 19433  df-psmet 20465  df-xmet 20466  df-met 20467  df-bl 20468  df-mopn 20469  df-cnfld 20474  df-top 21430  df-topon 21447  df-bases 21482  df-cmp 21923  df-ovol 23992  df-vol 23993  df-sumge0 42522  df-ovoln 42696
This theorem is referenced by:  ovnsubaddlem2  42730
  Copyright terms: Public domain W3C validator