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 𝑍 = (𝑎 ∈ 𝒫 (ℝ ↑m 𝑋) ↦ {𝑧 ∈ ℝ* ∣ ∃𝑖 ∈ (((ℝ × ℝ) ↑m 𝑋) ↑m ℕ)(𝑎 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑖𝑗))‘𝑘) ∧ 𝑧 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘𝑋 (vol‘(([,) ∘ (𝑖𝑗))‘𝑘)))))})
ovnsubaddlem1.c 𝐶 = (𝑎 ∈ 𝒫 (ℝ ↑m 𝑋) ↦ { ∈ (((ℝ × ℝ) ↑m 𝑋) ↑m ℕ) ∣ 𝑎 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘)})
ovnsubaddlem1.l 𝐿 = (𝑖 ∈ ((ℝ × ℝ) ↑m 𝑋) ↦ ∏𝑘𝑋 (vol‘(([,) ∘ 𝑖)‘𝑘)))
ovnsubaddlem1.d 𝐷 = (𝑎 ∈ 𝒫 (ℝ ↑m 𝑋) ↦ (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶𝑎) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((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 (𝜑𝐴:ℕ⟶𝒫 (ℝ ↑m 𝑋))
32adantr 484 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → 𝐴:ℕ⟶𝒫 (ℝ ↑m 𝑋))
4 simpr 488 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → 𝑛 ∈ ℕ)
53, 4ffvelrnd 6834 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → (𝐴𝑛) ∈ 𝒫 (ℝ ↑m 𝑋))
6 elpwi 4506 . . . . . . 7 ((𝐴𝑛) ∈ 𝒫 (ℝ ↑m 𝑋) → (𝐴𝑛) ⊆ (ℝ ↑m 𝑋))
75, 6syl 17 . . . . . 6 ((𝜑𝑛 ∈ ℕ) → (𝐴𝑛) ⊆ (ℝ ↑m 𝑋))
87ralrimiva 3149 . . . . 5 (𝜑 → ∀𝑛 ∈ ℕ (𝐴𝑛) ⊆ (ℝ ↑m 𝑋))
9 iunss 4933 . . . . 5 ( 𝑛 ∈ ℕ (𝐴𝑛) ⊆ (ℝ ↑m 𝑋) ↔ ∀𝑛 ∈ ℕ (𝐴𝑛) ⊆ (ℝ ↑m 𝑋))
108, 9sylibr 237 . . . 4 (𝜑 𝑛 ∈ ℕ (𝐴𝑛) ⊆ (ℝ ↑m 𝑋))
111, 10ovnxrcl 43269 . . 3 (𝜑 → ((voln*‘𝑋)‘ 𝑛 ∈ ℕ (𝐴𝑛)) ∈ ℝ*)
12 nfv 1915 . . . 4 𝑚𝜑
13 nnex 11638 . . . . 5 ℕ ∈ V
1413a1i 11 . . . 4 (𝜑 → ℕ ∈ V)
15 icossicc 12821 . . . . 5 (0[,)+∞) ⊆ (0[,]+∞)
16 nfv 1915 . . . . . 6 𝑘(𝜑𝑚 ∈ ℕ)
17 simpl 486 . . . . . . 7 ((𝜑𝑚 ∈ ℕ) → 𝜑)
1817, 1syl 17 . . . . . 6 ((𝜑𝑚 ∈ ℕ) → 𝑋 ∈ Fin)
19 ovnsubaddlem1.l . . . . . 6 𝐿 = (𝑖 ∈ ((ℝ × ℝ) ↑m 𝑋) ↦ ∏𝑘𝑋 (vol‘(([,) ∘ 𝑖)‘𝑘)))
20 ovnsubaddlem1.f . . . . . . . . . . . 12 (𝜑𝐹:ℕ–1-1-onto→(ℕ × ℕ))
21 f1of 6594 . . . . . . . . . . . 12 (𝐹:ℕ–1-1-onto→(ℕ × ℕ) → 𝐹:ℕ⟶(ℕ × ℕ))
2220, 21syl 17 . . . . . . . . . . 11 (𝜑𝐹:ℕ⟶(ℕ × ℕ))
2322adantr 484 . . . . . . . . . 10 ((𝜑𝑚 ∈ ℕ) → 𝐹:ℕ⟶(ℕ × ℕ))
24 simpr 488 . . . . . . . . . 10 ((𝜑𝑚 ∈ ℕ) → 𝑚 ∈ ℕ)
2523, 24ffvelrnd 6834 . . . . . . . . 9 ((𝜑𝑚 ∈ ℕ) → (𝐹𝑚) ∈ (ℕ × ℕ))
26 xp1st 7710 . . . . . . . . 9 ((𝐹𝑚) ∈ (ℕ × ℕ) → (1st ‘(𝐹𝑚)) ∈ ℕ)
2725, 26syl 17 . . . . . . . 8 ((𝜑𝑚 ∈ ℕ) → (1st ‘(𝐹𝑚)) ∈ ℕ)
28 xp2nd 7711 . . . . . . . . 9 ((𝐹𝑚) ∈ (ℕ × ℕ) → (2nd ‘(𝐹𝑚)) ∈ ℕ)
2925, 28syl 17 . . . . . . . 8 ((𝜑𝑚 ∈ ℕ) → (2nd ‘(𝐹𝑚)) ∈ ℕ)
30 fvex 6663 . . . . . . . . 9 (2nd ‘(𝐹𝑚)) ∈ V
31 eleq1 2877 . . . . . . . . . . 11 (𝑗 = (2nd ‘(𝐹𝑚)) → (𝑗 ∈ ℕ ↔ (2nd ‘(𝐹𝑚)) ∈ ℕ))
32313anbi3d 1439 . . . . . . . . . 10 (𝑗 = (2nd ‘(𝐹𝑚)) → ((𝜑 ∧ (1st ‘(𝐹𝑚)) ∈ ℕ ∧ 𝑗 ∈ ℕ) ↔ (𝜑 ∧ (1st ‘(𝐹𝑚)) ∈ ℕ ∧ (2nd ‘(𝐹𝑚)) ∈ ℕ)))
33 fveq2 6650 . . . . . . . . . . 11 (𝑗 = (2nd ‘(𝐹𝑚)) → ((𝐼‘(1st ‘(𝐹𝑚)))‘𝑗) = ((𝐼‘(1st ‘(𝐹𝑚)))‘(2nd ‘(𝐹𝑚))))
3433feq1d 6475 . . . . . . . . . 10 (𝑗 = (2nd ‘(𝐹𝑚)) → (((𝐼‘(1st ‘(𝐹𝑚)))‘𝑗):𝑋⟶(ℝ × ℝ) ↔ ((𝐼‘(1st ‘(𝐹𝑚)))‘(2nd ‘(𝐹𝑚))):𝑋⟶(ℝ × ℝ)))
3532, 34imbi12d 348 . . . . . . . . 9 (𝑗 = (2nd ‘(𝐹𝑚)) → (((𝜑 ∧ (1st ‘(𝐹𝑚)) ∈ ℕ ∧ 𝑗 ∈ ℕ) → ((𝐼‘(1st ‘(𝐹𝑚)))‘𝑗):𝑋⟶(ℝ × ℝ)) ↔ ((𝜑 ∧ (1st ‘(𝐹𝑚)) ∈ ℕ ∧ (2nd ‘(𝐹𝑚)) ∈ ℕ) → ((𝐼‘(1st ‘(𝐹𝑚)))‘(2nd ‘(𝐹𝑚))):𝑋⟶(ℝ × ℝ))))
36 fvex 6663 . . . . . . . . . 10 (1st ‘(𝐹𝑚)) ∈ V
37 eleq1 2877 . . . . . . . . . . . 12 (𝑛 = (1st ‘(𝐹𝑚)) → (𝑛 ∈ ℕ ↔ (1st ‘(𝐹𝑚)) ∈ ℕ))
38373anbi2d 1438 . . . . . . . . . . 11 (𝑛 = (1st ‘(𝐹𝑚)) → ((𝜑𝑛 ∈ ℕ ∧ 𝑗 ∈ ℕ) ↔ (𝜑 ∧ (1st ‘(𝐹𝑚)) ∈ ℕ ∧ 𝑗 ∈ ℕ)))
39 fveq2 6650 . . . . . . . . . . . . 13 (𝑛 = (1st ‘(𝐹𝑚)) → (𝐼𝑛) = (𝐼‘(1st ‘(𝐹𝑚))))
4039fveq1d 6652 . . . . . . . . . . . 12 (𝑛 = (1st ‘(𝐹𝑚)) → ((𝐼𝑛)‘𝑗) = ((𝐼‘(1st ‘(𝐹𝑚)))‘𝑗))
4140feq1d 6475 . . . . . . . . . . 11 (𝑛 = (1st ‘(𝐹𝑚)) → (((𝐼𝑛)‘𝑗):𝑋⟶(ℝ × ℝ) ↔ ((𝐼‘(1st ‘(𝐹𝑚)))‘𝑗):𝑋⟶(ℝ × ℝ)))
4238, 41imbi12d 348 . . . . . . . . . 10 (𝑛 = (1st ‘(𝐹𝑚)) → (((𝜑𝑛 ∈ ℕ ∧ 𝑗 ∈ ℕ) → ((𝐼𝑛)‘𝑗):𝑋⟶(ℝ × ℝ)) ↔ ((𝜑 ∧ (1st ‘(𝐹𝑚)) ∈ ℕ ∧ 𝑗 ∈ ℕ) → ((𝐼‘(1st ‘(𝐹𝑚)))‘𝑗):𝑋⟶(ℝ × ℝ))))
43 ovnsubaddlem1.c . . . . . . . . . . . . . . . . . . 19 𝐶 = (𝑎 ∈ 𝒫 (ℝ ↑m 𝑋) ↦ { ∈ (((ℝ × ℝ) ↑m 𝑋) ↑m ℕ) ∣ 𝑎 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘)})
44 sseq1 3940 . . . . . . . . . . . . . . . . . . . 20 (𝑎 = (𝐴𝑛) → (𝑎 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘) ↔ (𝐴𝑛) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘)))
4544rabbidv 3427 . . . . . . . . . . . . . . . . . . 19 (𝑎 = (𝐴𝑛) → { ∈ (((ℝ × ℝ) ↑m 𝑋) ↑m ℕ) ∣ 𝑎 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘)} = { ∈ (((ℝ × ℝ) ↑m 𝑋) ↑m ℕ) ∣ (𝐴𝑛) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘)})
46 ovex 7173 . . . . . . . . . . . . . . . . . . . . 21 (((ℝ × ℝ) ↑m 𝑋) ↑m ℕ) ∈ V
4746rabex 5200 . . . . . . . . . . . . . . . . . . . 20 { ∈ (((ℝ × ℝ) ↑m 𝑋) ↑m ℕ) ∣ (𝐴𝑛) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘)} ∈ V
4847a1i 11 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑛 ∈ ℕ) → { ∈ (((ℝ × ℝ) ↑m 𝑋) ↑m ℕ) ∣ (𝐴𝑛) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘)} ∈ V)
4943, 45, 5, 48fvmptd3 6773 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑛 ∈ ℕ) → (𝐶‘(𝐴𝑛)) = { ∈ (((ℝ × ℝ) ↑m 𝑋) ↑m ℕ) ∣ (𝐴𝑛) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘)})
50 ssrab2 4007 . . . . . . . . . . . . . . . . . . 19 { ∈ (((ℝ × ℝ) ↑m 𝑋) ↑m ℕ) ∣ (𝐴𝑛) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘)} ⊆ (((ℝ × ℝ) ↑m 𝑋) ↑m ℕ)
5150a1i 11 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑛 ∈ ℕ) → { ∈ (((ℝ × ℝ) ↑m 𝑋) ↑m ℕ) ∣ (𝐴𝑛) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘)} ⊆ (((ℝ × ℝ) ↑m 𝑋) ↑m ℕ))
5249, 51eqsstrd 3953 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛 ∈ ℕ) → (𝐶‘(𝐴𝑛)) ⊆ (((ℝ × ℝ) ↑m 𝑋) ↑m ℕ))
53 ovnsubaddlem1.d . . . . . . . . . . . . . . . . . . . . 21 𝐷 = (𝑎 ∈ 𝒫 (ℝ ↑m 𝑋) ↦ (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶𝑎) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘𝑎) +𝑒 𝑒)}))
54 fveq2 6650 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑎 = (𝐴𝑛) → (𝐶𝑎) = (𝐶‘(𝐴𝑛)))
5554eleq2d 2875 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑎 = (𝐴𝑛) → (𝑖 ∈ (𝐶𝑎) ↔ 𝑖 ∈ (𝐶‘(𝐴𝑛))))
56 fveq2 6650 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑎 = (𝐴𝑛) → ((voln*‘𝑋)‘𝑎) = ((voln*‘𝑋)‘(𝐴𝑛)))
5756oveq1d 7155 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑎 = (𝐴𝑛) → (((voln*‘𝑋)‘𝑎) +𝑒 𝑒) = (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 𝑒))
5857breq2d 5043 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑎 = (𝐴𝑛) → ((Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘𝑎) +𝑒 𝑒) ↔ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 𝑒)))
5955, 58anbi12d 633 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑎 = (𝐴𝑛) → ((𝑖 ∈ (𝐶𝑎) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘𝑎) +𝑒 𝑒)) ↔ (𝑖 ∈ (𝐶‘(𝐴𝑛)) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 𝑒))))
6059rabbidva2 3423 . . . . . . . . . . . . . . . . . . . . . 22 (𝑎 = (𝐴𝑛) → {𝑖 ∈ (𝐶𝑎) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘𝑎) +𝑒 𝑒)} = {𝑖 ∈ (𝐶‘(𝐴𝑛)) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 𝑒)})
6160mpteq2dv 5127 . . . . . . . . . . . . . . . . . . . . 21 (𝑎 = (𝐴𝑛) → (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶𝑎) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘𝑎) +𝑒 𝑒)}) = (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶‘(𝐴𝑛)) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 𝑒)}))
62 rpex 42039 . . . . . . . . . . . . . . . . . . . . . . 23 + ∈ V
6362mptex 6968 . . . . . . . . . . . . . . . . . . . . . 22 (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶‘(𝐴𝑛)) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 𝑒)}) ∈ V
6463a1i 11 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑛 ∈ ℕ) → (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶‘(𝐴𝑛)) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 𝑒)}) ∈ V)
6553, 61, 5, 64fvmptd3 6773 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑛 ∈ ℕ) → (𝐷‘(𝐴𝑛)) = (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶‘(𝐴𝑛)) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 𝑒)}))
66 oveq2 7148 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑒 = (𝐸 / (2↑𝑛)) → (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 𝑒) = (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛))))
6766breq2d 5043 . . . . . . . . . . . . . . . . . . . . . 22 (𝑒 = (𝐸 / (2↑𝑛)) → ((Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 𝑒) ↔ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛)))))
6867rabbidv 3427 . . . . . . . . . . . . . . . . . . . . 21 (𝑒 = (𝐸 / (2↑𝑛)) → {𝑖 ∈ (𝐶‘(𝐴𝑛)) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 𝑒)} = {𝑖 ∈ (𝐶‘(𝐴𝑛)) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛)))})
6968adantl 485 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑛 ∈ ℕ) ∧ 𝑒 = (𝐸 / (2↑𝑛))) → {𝑖 ∈ (𝐶‘(𝐴𝑛)) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 𝑒)} = {𝑖 ∈ (𝐶‘(𝐴𝑛)) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛)))})
70 ovnsubaddlem1.e . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝐸 ∈ ℝ+)
7170adantr 484 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑛 ∈ ℕ) → 𝐸 ∈ ℝ+)
72 2nn 11705 . . . . . . . . . . . . . . . . . . . . . . . . 25 2 ∈ ℕ
7372a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 ∈ ℕ → 2 ∈ ℕ)
74 nnnn0 11899 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 ∈ ℕ → 𝑛 ∈ ℕ0)
7573, 74nnexpcld 13609 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 ∈ ℕ → (2↑𝑛) ∈ ℕ)
7675nnrpd 12424 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 ∈ ℕ → (2↑𝑛) ∈ ℝ+)
7776adantl 485 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑛 ∈ ℕ) → (2↑𝑛) ∈ ℝ+)
7871, 77rpdivcld 12443 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑛 ∈ ℕ) → (𝐸 / (2↑𝑛)) ∈ ℝ+)
79 fvex 6663 . . . . . . . . . . . . . . . . . . . . . 22 (𝐶‘(𝐴𝑛)) ∈ V
8079rabex 5200 . . . . . . . . . . . . . . . . . . . . 21 {𝑖 ∈ (𝐶‘(𝐴𝑛)) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛)))} ∈ V
8180a1i 11 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑛 ∈ ℕ) → {𝑖 ∈ (𝐶‘(𝐴𝑛)) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛)))} ∈ V)
8265, 69, 78, 81fvmptd 6757 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑛 ∈ ℕ) → ((𝐷‘(𝐴𝑛))‘(𝐸 / (2↑𝑛))) = {𝑖 ∈ (𝐶‘(𝐴𝑛)) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛)))})
83 ssrab2 4007 . . . . . . . . . . . . . . . . . . . 20 {𝑖 ∈ (𝐶‘(𝐴𝑛)) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛)))} ⊆ (𝐶‘(𝐴𝑛))
8483a1i 11 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑛 ∈ ℕ) → {𝑖 ∈ (𝐶‘(𝐴𝑛)) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛)))} ⊆ (𝐶‘(𝐴𝑛)))
8582, 84eqsstrd 3953 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑛 ∈ ℕ) → ((𝐷‘(𝐴𝑛))‘(𝐸 / (2↑𝑛))) ⊆ (𝐶‘(𝐴𝑛)))
86 ovnsubaddlem1.i . . . . . . . . . . . . . . . . . 18 ((𝜑𝑛 ∈ ℕ) → (𝐼𝑛) ∈ ((𝐷‘(𝐴𝑛))‘(𝐸 / (2↑𝑛))))
8785, 86sseldd 3916 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛 ∈ ℕ) → (𝐼𝑛) ∈ (𝐶‘(𝐴𝑛)))
8852, 87sseldd 3916 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ ℕ) → (𝐼𝑛) ∈ (((ℝ × ℝ) ↑m 𝑋) ↑m ℕ))
89 elmapfn 8419 . . . . . . . . . . . . . . . 16 ((𝐼𝑛) ∈ (((ℝ × ℝ) ↑m 𝑋) ↑m ℕ) → (𝐼𝑛) Fn ℕ)
9088, 89syl 17 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ) → (𝐼𝑛) Fn ℕ)
91 elmapi 8418 . . . . . . . . . . . . . . . . . 18 ((𝐼𝑛) ∈ (((ℝ × ℝ) ↑m 𝑋) ↑m ℕ) → (𝐼𝑛):ℕ⟶((ℝ × ℝ) ↑m 𝑋))
9288, 91syl 17 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛 ∈ ℕ) → (𝐼𝑛):ℕ⟶((ℝ × ℝ) ↑m 𝑋))
9392ffvelrnda 6833 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → ((𝐼𝑛)‘𝑗) ∈ ((ℝ × ℝ) ↑m 𝑋))
9493ralrimiva 3149 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ) → ∀𝑗 ∈ ℕ ((𝐼𝑛)‘𝑗) ∈ ((ℝ × ℝ) ↑m 𝑋))
9590, 94jca 515 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ ℕ) → ((𝐼𝑛) Fn ℕ ∧ ∀𝑗 ∈ ℕ ((𝐼𝑛)‘𝑗) ∈ ((ℝ × ℝ) ↑m 𝑋)))
96953adant3 1129 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ ℕ ∧ 𝑗 ∈ ℕ) → ((𝐼𝑛) Fn ℕ ∧ ∀𝑗 ∈ ℕ ((𝐼𝑛)‘𝑗) ∈ ((ℝ × ℝ) ↑m 𝑋)))
97 ffnfv 6864 . . . . . . . . . . . . 13 ((𝐼𝑛):ℕ⟶((ℝ × ℝ) ↑m 𝑋) ↔ ((𝐼𝑛) Fn ℕ ∧ ∀𝑗 ∈ ℕ ((𝐼𝑛)‘𝑗) ∈ ((ℝ × ℝ) ↑m 𝑋)))
9896, 97sylibr 237 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ ∧ 𝑗 ∈ ℕ) → (𝐼𝑛):ℕ⟶((ℝ × ℝ) ↑m 𝑋))
99 simp3 1135 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ ℕ)
10098, 99ffvelrnd 6834 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ ∧ 𝑗 ∈ ℕ) → ((𝐼𝑛)‘𝑗) ∈ ((ℝ × ℝ) ↑m 𝑋))
101 elmapi 8418 . . . . . . . . . . 11 (((𝐼𝑛)‘𝑗) ∈ ((ℝ × ℝ) ↑m 𝑋) → ((𝐼𝑛)‘𝑗):𝑋⟶(ℝ × ℝ))
102100, 101syl 17 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ ∧ 𝑗 ∈ ℕ) → ((𝐼𝑛)‘𝑗):𝑋⟶(ℝ × ℝ))
10336, 42, 102vtocl 3507 . . . . . . . . 9 ((𝜑 ∧ (1st ‘(𝐹𝑚)) ∈ ℕ ∧ 𝑗 ∈ ℕ) → ((𝐼‘(1st ‘(𝐹𝑚)))‘𝑗):𝑋⟶(ℝ × ℝ))
10430, 35, 103vtocl 3507 . . . . . . . 8 ((𝜑 ∧ (1st ‘(𝐹𝑚)) ∈ ℕ ∧ (2nd ‘(𝐹𝑚)) ∈ ℕ) → ((𝐼‘(1st ‘(𝐹𝑚)))‘(2nd ‘(𝐹𝑚))):𝑋⟶(ℝ × ℝ))
10517, 27, 29, 104syl3anc 1368 . . . . . . 7 ((𝜑𝑚 ∈ ℕ) → ((𝐼‘(1st ‘(𝐹𝑚)))‘(2nd ‘(𝐹𝑚))):𝑋⟶(ℝ × ℝ))
106 id 22 . . . . . . . . . 10 (𝑚 ∈ ℕ → 𝑚 ∈ ℕ)
107 fvex 6663 . . . . . . . . . . 11 ((𝐼‘(1st ‘(𝐹𝑚)))‘(2nd ‘(𝐹𝑚))) ∈ V
108107a1i 11 . . . . . . . . . 10 (𝑚 ∈ ℕ → ((𝐼‘(1st ‘(𝐹𝑚)))‘(2nd ‘(𝐹𝑚))) ∈ V)
109 ovnsubaddlem1.g . . . . . . . . . . 11 𝐺 = (𝑚 ∈ ℕ ↦ ((𝐼‘(1st ‘(𝐹𝑚)))‘(2nd ‘(𝐹𝑚))))
110109fvmpt2 6761 . . . . . . . . . 10 ((𝑚 ∈ ℕ ∧ ((𝐼‘(1st ‘(𝐹𝑚)))‘(2nd ‘(𝐹𝑚))) ∈ V) → (𝐺𝑚) = ((𝐼‘(1st ‘(𝐹𝑚)))‘(2nd ‘(𝐹𝑚))))
111106, 108, 110syl2anc 587 . . . . . . . . 9 (𝑚 ∈ ℕ → (𝐺𝑚) = ((𝐼‘(1st ‘(𝐹𝑚)))‘(2nd ‘(𝐹𝑚))))
112111adantl 485 . . . . . . . 8 ((𝜑𝑚 ∈ ℕ) → (𝐺𝑚) = ((𝐼‘(1st ‘(𝐹𝑚)))‘(2nd ‘(𝐹𝑚))))
113112feq1d 6475 . . . . . . 7 ((𝜑𝑚 ∈ ℕ) → ((𝐺𝑚):𝑋⟶(ℝ × ℝ) ↔ ((𝐼‘(1st ‘(𝐹𝑚)))‘(2nd ‘(𝐹𝑚))):𝑋⟶(ℝ × ℝ)))
114105, 113mpbird 260 . . . . . 6 ((𝜑𝑚 ∈ ℕ) → (𝐺𝑚):𝑋⟶(ℝ × ℝ))
11516, 18, 19, 114hoiprodcl2 43255 . . . . 5 ((𝜑𝑚 ∈ ℕ) → (𝐿‘(𝐺𝑚)) ∈ (0[,)+∞))
11615, 115sseldi 3913 . . . 4 ((𝜑𝑚 ∈ ℕ) → (𝐿‘(𝐺𝑚)) ∈ (0[,]+∞))
11712, 14, 116sge0xrclmpt 43128 . . 3 (𝜑 → (Σ^‘(𝑚 ∈ ℕ ↦ (𝐿‘(𝐺𝑚)))) ∈ ℝ*)
118 nfv 1915 . . . 4 𝑛𝜑
119 0xr 10684 . . . . . 6 0 ∈ ℝ*
120119a1i 11 . . . . 5 ((𝜑𝑛 ∈ ℕ) → 0 ∈ ℝ*)
121 pnfxr 10691 . . . . . 6 +∞ ∈ ℝ*
122121a1i 11 . . . . 5 ((𝜑𝑛 ∈ ℕ) → +∞ ∈ ℝ*)
1231adantr 484 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → 𝑋 ∈ Fin)
124 ovnsubaddlem1.z . . . . . . . . 9 𝑍 = (𝑎 ∈ 𝒫 (ℝ ↑m 𝑋) ↦ {𝑧 ∈ ℝ* ∣ ∃𝑖 ∈ (((ℝ × ℝ) ↑m 𝑋) ↑m ℕ)(𝑎 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑖𝑗))‘𝑘) ∧ 𝑧 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘𝑋 (vol‘(([,) ∘ (𝑖𝑗))‘𝑘)))))})
125123, 7, 124ovnval2b 43252 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → ((voln*‘𝑋)‘(𝐴𝑛)) = if(𝑋 = ∅, 0, inf((𝑍‘(𝐴𝑛)), ℝ*, < )))
126 ovnsubaddlem1.n0 . . . . . . . . . . 11 (𝜑𝑋 ≠ ∅)
127126neneqd 2992 . . . . . . . . . 10 (𝜑 → ¬ 𝑋 = ∅)
128127iffalsed 4436 . . . . . . . . 9 (𝜑 → if(𝑋 = ∅, 0, inf((𝑍‘(𝐴𝑛)), ℝ*, < )) = inf((𝑍‘(𝐴𝑛)), ℝ*, < ))
129128adantr 484 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → if(𝑋 = ∅, 0, inf((𝑍‘(𝐴𝑛)), ℝ*, < )) = inf((𝑍‘(𝐴𝑛)), ℝ*, < ))
130125, 129eqtrd 2833 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → ((voln*‘𝑋)‘(𝐴𝑛)) = inf((𝑍‘(𝐴𝑛)), ℝ*, < ))
131 sseq1 3940 . . . . . . . . . . . . 13 (𝑎 = (𝐴𝑛) → (𝑎 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑖𝑗))‘𝑘) ↔ (𝐴𝑛) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑖𝑗))‘𝑘)))
132131anbi1d 632 . . . . . . . . . . . 12 (𝑎 = (𝐴𝑛) → ((𝑎 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑖𝑗))‘𝑘) ∧ 𝑧 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘𝑋 (vol‘(([,) ∘ (𝑖𝑗))‘𝑘))))) ↔ ((𝐴𝑛) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑖𝑗))‘𝑘) ∧ 𝑧 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘𝑋 (vol‘(([,) ∘ (𝑖𝑗))‘𝑘)))))))
133132rexbidv 3256 . . . . . . . . . . 11 (𝑎 = (𝐴𝑛) → (∃𝑖 ∈ (((ℝ × ℝ) ↑m 𝑋) ↑m ℕ)(𝑎 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑖𝑗))‘𝑘) ∧ 𝑧 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘𝑋 (vol‘(([,) ∘ (𝑖𝑗))‘𝑘))))) ↔ ∃𝑖 ∈ (((ℝ × ℝ) ↑m 𝑋) ↑m ℕ)((𝐴𝑛) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑖𝑗))‘𝑘) ∧ 𝑧 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘𝑋 (vol‘(([,) ∘ (𝑖𝑗))‘𝑘)))))))
134133rabbidv 3427 . . . . . . . . . 10 (𝑎 = (𝐴𝑛) → {𝑧 ∈ ℝ* ∣ ∃𝑖 ∈ (((ℝ × ℝ) ↑m 𝑋) ↑m ℕ)(𝑎 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑖𝑗))‘𝑘) ∧ 𝑧 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘𝑋 (vol‘(([,) ∘ (𝑖𝑗))‘𝑘)))))} = {𝑧 ∈ ℝ* ∣ ∃𝑖 ∈ (((ℝ × ℝ) ↑m 𝑋) ↑m ℕ)((𝐴𝑛) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑖𝑗))‘𝑘) ∧ 𝑧 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘𝑋 (vol‘(([,) ∘ (𝑖𝑗))‘𝑘)))))})
135 xrex 12381 . . . . . . . . . . . 12 * ∈ V
136135rabex 5200 . . . . . . . . . . 11 {𝑧 ∈ ℝ* ∣ ∃𝑖 ∈ (((ℝ × ℝ) ↑m 𝑋) ↑m ℕ)((𝐴𝑛) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑖𝑗))‘𝑘) ∧ 𝑧 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘𝑋 (vol‘(([,) ∘ (𝑖𝑗))‘𝑘)))))} ∈ V
137136a1i 11 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → {𝑧 ∈ ℝ* ∣ ∃𝑖 ∈ (((ℝ × ℝ) ↑m 𝑋) ↑m ℕ)((𝐴𝑛) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑖𝑗))‘𝑘) ∧ 𝑧 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘𝑋 (vol‘(([,) ∘ (𝑖𝑗))‘𝑘)))))} ∈ V)
138124, 134, 5, 137fvmptd3 6773 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → (𝑍‘(𝐴𝑛)) = {𝑧 ∈ ℝ* ∣ ∃𝑖 ∈ (((ℝ × ℝ) ↑m 𝑋) ↑m ℕ)((𝐴𝑛) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑖𝑗))‘𝑘) ∧ 𝑧 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘𝑋 (vol‘(([,) ∘ (𝑖𝑗))‘𝑘)))))})
139 ssrab2 4007 . . . . . . . . . 10 {𝑧 ∈ ℝ* ∣ ∃𝑖 ∈ (((ℝ × ℝ) ↑m 𝑋) ↑m ℕ)((𝐴𝑛) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑖𝑗))‘𝑘) ∧ 𝑧 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘𝑋 (vol‘(([,) ∘ (𝑖𝑗))‘𝑘)))))} ⊆ ℝ*
140139a1i 11 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → {𝑧 ∈ ℝ* ∣ ∃𝑖 ∈ (((ℝ × ℝ) ↑m 𝑋) ↑m ℕ)((𝐴𝑛) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑖𝑗))‘𝑘) ∧ 𝑧 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘𝑋 (vol‘(([,) ∘ (𝑖𝑗))‘𝑘)))))} ⊆ ℝ*)
141138, 140eqsstrd 3953 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → (𝑍‘(𝐴𝑛)) ⊆ ℝ*)
142 infxrcl 12721 . . . . . . . 8 ((𝑍‘(𝐴𝑛)) ⊆ ℝ* → inf((𝑍‘(𝐴𝑛)), ℝ*, < ) ∈ ℝ*)
143141, 142syl 17 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → inf((𝑍‘(𝐴𝑛)), ℝ*, < ) ∈ ℝ*)
144130, 143eqeltrd 2890 . . . . . 6 ((𝜑𝑛 ∈ ℕ) → ((voln*‘𝑋)‘(𝐴𝑛)) ∈ ℝ*)
14570rpred 12426 . . . . . . . . 9 (𝜑𝐸 ∈ ℝ)
146145adantr 484 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → 𝐸 ∈ ℝ)
147 2re 11706 . . . . . . . . . . 11 2 ∈ ℝ
148147a1i 11 . . . . . . . . . 10 (𝑛 ∈ ℕ → 2 ∈ ℝ)
149148, 74reexpcld 13530 . . . . . . . . 9 (𝑛 ∈ ℕ → (2↑𝑛) ∈ ℝ)
150149adantl 485 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → (2↑𝑛) ∈ ℝ)
151148recnd 10665 . . . . . . . . . 10 (𝑛 ∈ ℕ → 2 ∈ ℂ)
152 2ne0 11736 . . . . . . . . . . 11 2 ≠ 0
153152a1i 11 . . . . . . . . . 10 (𝑛 ∈ ℕ → 2 ≠ 0)
154 nnz 11999 . . . . . . . . . 10 (𝑛 ∈ ℕ → 𝑛 ∈ ℤ)
155151, 153, 154expne0d 13519 . . . . . . . . 9 (𝑛 ∈ ℕ → (2↑𝑛) ≠ 0)
156155adantl 485 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → (2↑𝑛) ≠ 0)
157146, 150, 156redivcld 11464 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → (𝐸 / (2↑𝑛)) ∈ ℝ)
158157rexrd 10687 . . . . . 6 ((𝜑𝑛 ∈ ℕ) → (𝐸 / (2↑𝑛)) ∈ ℝ*)
159144, 158xaddcld 12689 . . . . 5 ((𝜑𝑛 ∈ ℕ) → (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛))) ∈ ℝ*)
160123, 7ovncl 43267 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → ((voln*‘𝑋)‘(𝐴𝑛)) ∈ (0[,]+∞))
161 xrge0ge0 42040 . . . . . . 7 (((voln*‘𝑋)‘(𝐴𝑛)) ∈ (0[,]+∞) → 0 ≤ ((voln*‘𝑋)‘(𝐴𝑛)))
162160, 161syl 17 . . . . . 6 ((𝜑𝑛 ∈ ℕ) → 0 ≤ ((voln*‘𝑋)‘(𝐴𝑛)))
163 0red 10640 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → 0 ∈ ℝ)
16478rpgt0d 12429 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → 0 < (𝐸 / (2↑𝑛)))
165163, 157, 164ltled 10784 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → 0 ≤ (𝐸 / (2↑𝑛)))
166157ltpnfd 12511 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → (𝐸 / (2↑𝑛)) < +∞)
167158, 122, 166xrltled 12538 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → (𝐸 / (2↑𝑛)) ≤ +∞)
168120, 122, 158, 165, 167eliccxrd 42225 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → (𝐸 / (2↑𝑛)) ∈ (0[,]+∞))
169144, 168xadd0ge 42013 . . . . . 6 ((𝜑𝑛 ∈ ℕ) → ((voln*‘𝑋)‘(𝐴𝑛)) ≤ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛))))
170120, 144, 159, 162, 169xrletrd 12550 . . . . 5 ((𝜑𝑛 ∈ ℕ) → 0 ≤ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛))))
171 pnfge 12520 . . . . . 6 ((((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛))) ∈ ℝ* → (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛))) ≤ +∞)
172159, 171syl 17 . . . . 5 ((𝜑𝑛 ∈ ℕ) → (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛))) ≤ +∞)
173120, 122, 159, 170, 172eliccxrd 42225 . . . 4 ((𝜑𝑛 ∈ ℕ) → (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛))) ∈ (0[,]+∞))
174118, 14, 173sge0xrclmpt 43128 . . 3 (𝜑 → (Σ^‘(𝑛 ∈ ℕ ↦ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛))))) ∈ ℝ*)
175 sseq1 3940 . . . . . . . . . . . . 13 (𝑎 = (𝐴‘(1st ‘(𝐹𝑚))) → (𝑎 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘) ↔ (𝐴‘(1st ‘(𝐹𝑚))) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘)))
176175rabbidv 3427 . . . . . . . . . . . 12 (𝑎 = (𝐴‘(1st ‘(𝐹𝑚))) → { ∈ (((ℝ × ℝ) ↑m 𝑋) ↑m ℕ) ∣ 𝑎 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘)} = { ∈ (((ℝ × ℝ) ↑m 𝑋) ↑m ℕ) ∣ (𝐴‘(1st ‘(𝐹𝑚))) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘)})
1772adantr 484 . . . . . . . . . . . . 13 ((𝜑𝑚 ∈ ℕ) → 𝐴:ℕ⟶𝒫 (ℝ ↑m 𝑋))
178177, 27ffvelrnd 6834 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ ℕ) → (𝐴‘(1st ‘(𝐹𝑚))) ∈ 𝒫 (ℝ ↑m 𝑋))
17946rabex 5200 . . . . . . . . . . . . 13 { ∈ (((ℝ × ℝ) ↑m 𝑋) ↑m ℕ) ∣ (𝐴‘(1st ‘(𝐹𝑚))) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘)} ∈ V
180179a1i 11 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ ℕ) → { ∈ (((ℝ × ℝ) ↑m 𝑋) ↑m ℕ) ∣ (𝐴‘(1st ‘(𝐹𝑚))) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘)} ∈ V)
18143, 176, 178, 180fvmptd3 6773 . . . . . . . . . . 11 ((𝜑𝑚 ∈ ℕ) → (𝐶‘(𝐴‘(1st ‘(𝐹𝑚)))) = { ∈ (((ℝ × ℝ) ↑m 𝑋) ↑m ℕ) ∣ (𝐴‘(1st ‘(𝐹𝑚))) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘)})
182 ssrab2 4007 . . . . . . . . . . . 12 { ∈ (((ℝ × ℝ) ↑m 𝑋) ↑m ℕ) ∣ (𝐴‘(1st ‘(𝐹𝑚))) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘)} ⊆ (((ℝ × ℝ) ↑m 𝑋) ↑m ℕ)
183182a1i 11 . . . . . . . . . . 11 ((𝜑𝑚 ∈ ℕ) → { ∈ (((ℝ × ℝ) ↑m 𝑋) ↑m ℕ) ∣ (𝐴‘(1st ‘(𝐹𝑚))) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘)} ⊆ (((ℝ × ℝ) ↑m 𝑋) ↑m ℕ))
184181, 183eqsstrd 3953 . . . . . . . . . 10 ((𝜑𝑚 ∈ ℕ) → (𝐶‘(𝐴‘(1st ‘(𝐹𝑚)))) ⊆ (((ℝ × ℝ) ↑m 𝑋) ↑m ℕ))
185 fveq2 6650 . . . . . . . . . . . . . . . . . 18 (𝑎 = (𝐴‘(1st ‘(𝐹𝑚))) → (𝐶𝑎) = (𝐶‘(𝐴‘(1st ‘(𝐹𝑚)))))
186185eleq2d 2875 . . . . . . . . . . . . . . . . 17 (𝑎 = (𝐴‘(1st ‘(𝐹𝑚))) → (𝑖 ∈ (𝐶𝑎) ↔ 𝑖 ∈ (𝐶‘(𝐴‘(1st ‘(𝐹𝑚))))))
187 fveq2 6650 . . . . . . . . . . . . . . . . . . 19 (𝑎 = (𝐴‘(1st ‘(𝐹𝑚))) → ((voln*‘𝑋)‘𝑎) = ((voln*‘𝑋)‘(𝐴‘(1st ‘(𝐹𝑚)))))
188187oveq1d 7155 . . . . . . . . . . . . . . . . . 18 (𝑎 = (𝐴‘(1st ‘(𝐹𝑚))) → (((voln*‘𝑋)‘𝑎) +𝑒 𝑒) = (((voln*‘𝑋)‘(𝐴‘(1st ‘(𝐹𝑚)))) +𝑒 𝑒))
189188breq2d 5043 . . . . . . . . . . . . . . . . 17 (𝑎 = (𝐴‘(1st ‘(𝐹𝑚))) → ((Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘𝑎) +𝑒 𝑒) ↔ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴‘(1st ‘(𝐹𝑚)))) +𝑒 𝑒)))
190186, 189anbi12d 633 . . . . . . . . . . . . . . . 16 (𝑎 = (𝐴‘(1st ‘(𝐹𝑚))) → ((𝑖 ∈ (𝐶𝑎) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘𝑎) +𝑒 𝑒)) ↔ (𝑖 ∈ (𝐶‘(𝐴‘(1st ‘(𝐹𝑚)))) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴‘(1st ‘(𝐹𝑚)))) +𝑒 𝑒))))
191190rabbidva2 3423 . . . . . . . . . . . . . . 15 (𝑎 = (𝐴‘(1st ‘(𝐹𝑚))) → {𝑖 ∈ (𝐶𝑎) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘𝑎) +𝑒 𝑒)} = {𝑖 ∈ (𝐶‘(𝐴‘(1st ‘(𝐹𝑚)))) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴‘(1st ‘(𝐹𝑚)))) +𝑒 𝑒)})
192191mpteq2dv 5127 . . . . . . . . . . . . . 14 (𝑎 = (𝐴‘(1st ‘(𝐹𝑚))) → (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶𝑎) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘𝑎) +𝑒 𝑒)}) = (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶‘(𝐴‘(1st ‘(𝐹𝑚)))) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴‘(1st ‘(𝐹𝑚)))) +𝑒 𝑒)}))
19362mptex 6968 . . . . . . . . . . . . . . 15 (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶‘(𝐴‘(1st ‘(𝐹𝑚)))) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴‘(1st ‘(𝐹𝑚)))) +𝑒 𝑒)}) ∈ V
194193a1i 11 . . . . . . . . . . . . . 14 ((𝜑𝑚 ∈ ℕ) → (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶‘(𝐴‘(1st ‘(𝐹𝑚)))) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴‘(1st ‘(𝐹𝑚)))) +𝑒 𝑒)}) ∈ V)
19553, 192, 178, 194fvmptd3 6773 . . . . . . . . . . . . 13 ((𝜑𝑚 ∈ ℕ) → (𝐷‘(𝐴‘(1st ‘(𝐹𝑚)))) = (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶‘(𝐴‘(1st ‘(𝐹𝑚)))) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴‘(1st ‘(𝐹𝑚)))) +𝑒 𝑒)}))
196 oveq2 7148 . . . . . . . . . . . . . . . 16 (𝑒 = (𝐸 / (2↑(1st ‘(𝐹𝑚)))) → (((voln*‘𝑋)‘(𝐴‘(1st ‘(𝐹𝑚)))) +𝑒 𝑒) = (((voln*‘𝑋)‘(𝐴‘(1st ‘(𝐹𝑚)))) +𝑒 (𝐸 / (2↑(1st ‘(𝐹𝑚))))))
197196breq2d 5043 . . . . . . . . . . . . . . 15 (𝑒 = (𝐸 / (2↑(1st ‘(𝐹𝑚)))) → ((Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴‘(1st ‘(𝐹𝑚)))) +𝑒 𝑒) ↔ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴‘(1st ‘(𝐹𝑚)))) +𝑒 (𝐸 / (2↑(1st ‘(𝐹𝑚)))))))
198197rabbidv 3427 . . . . . . . . . . . . . 14 (𝑒 = (𝐸 / (2↑(1st ‘(𝐹𝑚)))) → {𝑖 ∈ (𝐶‘(𝐴‘(1st ‘(𝐹𝑚)))) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴‘(1st ‘(𝐹𝑚)))) +𝑒 𝑒)} = {𝑖 ∈ (𝐶‘(𝐴‘(1st ‘(𝐹𝑚)))) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴‘(1st ‘(𝐹𝑚)))) +𝑒 (𝐸 / (2↑(1st ‘(𝐹𝑚)))))})
199198adantl 485 . . . . . . . . . . . . 13 (((𝜑𝑚 ∈ ℕ) ∧ 𝑒 = (𝐸 / (2↑(1st ‘(𝐹𝑚))))) → {𝑖 ∈ (𝐶‘(𝐴‘(1st ‘(𝐹𝑚)))) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴‘(1st ‘(𝐹𝑚)))) +𝑒 𝑒)} = {𝑖 ∈ (𝐶‘(𝐴‘(1st ‘(𝐹𝑚)))) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴‘(1st ‘(𝐹𝑚)))) +𝑒 (𝐸 / (2↑(1st ‘(𝐹𝑚)))))})
20017, 70syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑚 ∈ ℕ) → 𝐸 ∈ ℝ+)
201 2rp 12389 . . . . . . . . . . . . . . . 16 2 ∈ ℝ+
202201a1i 11 . . . . . . . . . . . . . . 15 ((𝜑𝑚 ∈ ℕ) → 2 ∈ ℝ+)
20327nnzd 12081 . . . . . . . . . . . . . . 15 ((𝜑𝑚 ∈ ℕ) → (1st ‘(𝐹𝑚)) ∈ ℤ)
204202, 203rpexpcld 13611 . . . . . . . . . . . . . 14 ((𝜑𝑚 ∈ ℕ) → (2↑(1st ‘(𝐹𝑚))) ∈ ℝ+)
205200, 204rpdivcld 12443 . . . . . . . . . . . . 13 ((𝜑𝑚 ∈ ℕ) → (𝐸 / (2↑(1st ‘(𝐹𝑚)))) ∈ ℝ+)
206 fvex 6663 . . . . . . . . . . . . . . 15 (𝐶‘(𝐴‘(1st ‘(𝐹𝑚)))) ∈ V
207206rabex 5200 . . . . . . . . . . . . . 14 {𝑖 ∈ (𝐶‘(𝐴‘(1st ‘(𝐹𝑚)))) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴‘(1st ‘(𝐹𝑚)))) +𝑒 (𝐸 / (2↑(1st ‘(𝐹𝑚)))))} ∈ V
208207a1i 11 . . . . . . . . . . . . 13 ((𝜑𝑚 ∈ ℕ) → {𝑖 ∈ (𝐶‘(𝐴‘(1st ‘(𝐹𝑚)))) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴‘(1st ‘(𝐹𝑚)))) +𝑒 (𝐸 / (2↑(1st ‘(𝐹𝑚)))))} ∈ V)
209195, 199, 205, 208fvmptd 6757 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ ℕ) → ((𝐷‘(𝐴‘(1st ‘(𝐹𝑚))))‘(𝐸 / (2↑(1st ‘(𝐹𝑚))))) = {𝑖 ∈ (𝐶‘(𝐴‘(1st ‘(𝐹𝑚)))) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴‘(1st ‘(𝐹𝑚)))) +𝑒 (𝐸 / (2↑(1st ‘(𝐹𝑚)))))})
210 ssrab2 4007 . . . . . . . . . . . . 13 {𝑖 ∈ (𝐶‘(𝐴‘(1st ‘(𝐹𝑚)))) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴‘(1st ‘(𝐹𝑚)))) +𝑒 (𝐸 / (2↑(1st ‘(𝐹𝑚)))))} ⊆ (𝐶‘(𝐴‘(1st ‘(𝐹𝑚))))
211210a1i 11 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ ℕ) → {𝑖 ∈ (𝐶‘(𝐴‘(1st ‘(𝐹𝑚)))) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴‘(1st ‘(𝐹𝑚)))) +𝑒 (𝐸 / (2↑(1st ‘(𝐹𝑚)))))} ⊆ (𝐶‘(𝐴‘(1st ‘(𝐹𝑚)))))
212209, 211eqsstrd 3953 . . . . . . . . . . 11 ((𝜑𝑚 ∈ ℕ) → ((𝐷‘(𝐴‘(1st ‘(𝐹𝑚))))‘(𝐸 / (2↑(1st ‘(𝐹𝑚))))) ⊆ (𝐶‘(𝐴‘(1st ‘(𝐹𝑚)))))
21337anbi2d 631 . . . . . . . . . . . . . 14 (𝑛 = (1st ‘(𝐹𝑚)) → ((𝜑𝑛 ∈ ℕ) ↔ (𝜑 ∧ (1st ‘(𝐹𝑚)) ∈ ℕ)))
214 2fveq3 6655 . . . . . . . . . . . . . . . 16 (𝑛 = (1st ‘(𝐹𝑚)) → (𝐷‘(𝐴𝑛)) = (𝐷‘(𝐴‘(1st ‘(𝐹𝑚)))))
215 oveq2 7148 . . . . . . . . . . . . . . . . 17 (𝑛 = (1st ‘(𝐹𝑚)) → (2↑𝑛) = (2↑(1st ‘(𝐹𝑚))))
216215oveq2d 7156 . . . . . . . . . . . . . . . 16 (𝑛 = (1st ‘(𝐹𝑚)) → (𝐸 / (2↑𝑛)) = (𝐸 / (2↑(1st ‘(𝐹𝑚)))))
217214, 216fveq12d 6657 . . . . . . . . . . . . . . 15 (𝑛 = (1st ‘(𝐹𝑚)) → ((𝐷‘(𝐴𝑛))‘(𝐸 / (2↑𝑛))) = ((𝐷‘(𝐴‘(1st ‘(𝐹𝑚))))‘(𝐸 / (2↑(1st ‘(𝐹𝑚))))))
21839, 217eleq12d 2884 . . . . . . . . . . . . . 14 (𝑛 = (1st ‘(𝐹𝑚)) → ((𝐼𝑛) ∈ ((𝐷‘(𝐴𝑛))‘(𝐸 / (2↑𝑛))) ↔ (𝐼‘(1st ‘(𝐹𝑚))) ∈ ((𝐷‘(𝐴‘(1st ‘(𝐹𝑚))))‘(𝐸 / (2↑(1st ‘(𝐹𝑚)))))))
219213, 218imbi12d 348 . . . . . . . . . . . . 13 (𝑛 = (1st ‘(𝐹𝑚)) → (((𝜑𝑛 ∈ ℕ) → (𝐼𝑛) ∈ ((𝐷‘(𝐴𝑛))‘(𝐸 / (2↑𝑛)))) ↔ ((𝜑 ∧ (1st ‘(𝐹𝑚)) ∈ ℕ) → (𝐼‘(1st ‘(𝐹𝑚))) ∈ ((𝐷‘(𝐴‘(1st ‘(𝐹𝑚))))‘(𝐸 / (2↑(1st ‘(𝐹𝑚))))))))
22036, 219, 86vtocl 3507 . . . . . . . . . . . 12 ((𝜑 ∧ (1st ‘(𝐹𝑚)) ∈ ℕ) → (𝐼‘(1st ‘(𝐹𝑚))) ∈ ((𝐷‘(𝐴‘(1st ‘(𝐹𝑚))))‘(𝐸 / (2↑(1st ‘(𝐹𝑚))))))
22117, 27, 220syl2anc 587 . . . . . . . . . . 11 ((𝜑𝑚 ∈ ℕ) → (𝐼‘(1st ‘(𝐹𝑚))) ∈ ((𝐷‘(𝐴‘(1st ‘(𝐹𝑚))))‘(𝐸 / (2↑(1st ‘(𝐹𝑚))))))
222212, 221sseldd 3916 . . . . . . . . . 10 ((𝜑𝑚 ∈ ℕ) → (𝐼‘(1st ‘(𝐹𝑚))) ∈ (𝐶‘(𝐴‘(1st ‘(𝐹𝑚)))))
223184, 222sseldd 3916 . . . . . . . . 9 ((𝜑𝑚 ∈ ℕ) → (𝐼‘(1st ‘(𝐹𝑚))) ∈ (((ℝ × ℝ) ↑m 𝑋) ↑m ℕ))
224 elmapfn 8419 . . . . . . . . 9 ((𝐼‘(1st ‘(𝐹𝑚))) ∈ (((ℝ × ℝ) ↑m 𝑋) ↑m ℕ) → (𝐼‘(1st ‘(𝐹𝑚))) Fn ℕ)
225223, 224syl 17 . . . . . . . 8 ((𝜑𝑚 ∈ ℕ) → (𝐼‘(1st ‘(𝐹𝑚))) Fn ℕ)
226 elmapi 8418 . . . . . . . . . . 11 ((𝐼‘(1st ‘(𝐹𝑚))) ∈ (((ℝ × ℝ) ↑m 𝑋) ↑m ℕ) → (𝐼‘(1st ‘(𝐹𝑚))):ℕ⟶((ℝ × ℝ) ↑m 𝑋))
227223, 226syl 17 . . . . . . . . . 10 ((𝜑𝑚 ∈ ℕ) → (𝐼‘(1st ‘(𝐹𝑚))):ℕ⟶((ℝ × ℝ) ↑m 𝑋))
228227ffvelrnda 6833 . . . . . . . . 9 (((𝜑𝑚 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → ((𝐼‘(1st ‘(𝐹𝑚)))‘𝑗) ∈ ((ℝ × ℝ) ↑m 𝑋))
229228ralrimiva 3149 . . . . . . . 8 ((𝜑𝑚 ∈ ℕ) → ∀𝑗 ∈ ℕ ((𝐼‘(1st ‘(𝐹𝑚)))‘𝑗) ∈ ((ℝ × ℝ) ↑m 𝑋))
230225, 229jca 515 . . . . . . 7 ((𝜑𝑚 ∈ ℕ) → ((𝐼‘(1st ‘(𝐹𝑚))) Fn ℕ ∧ ∀𝑗 ∈ ℕ ((𝐼‘(1st ‘(𝐹𝑚)))‘𝑗) ∈ ((ℝ × ℝ) ↑m 𝑋)))
231 ffnfv 6864 . . . . . . 7 ((𝐼‘(1st ‘(𝐹𝑚))):ℕ⟶((ℝ × ℝ) ↑m 𝑋) ↔ ((𝐼‘(1st ‘(𝐹𝑚))) Fn ℕ ∧ ∀𝑗 ∈ ℕ ((𝐼‘(1st ‘(𝐹𝑚)))‘𝑗) ∈ ((ℝ × ℝ) ↑m 𝑋)))
232230, 231sylibr 237 . . . . . 6 ((𝜑𝑚 ∈ ℕ) → (𝐼‘(1st ‘(𝐹𝑚))):ℕ⟶((ℝ × ℝ) ↑m 𝑋))
233232, 29ffvelrnd 6834 . . . . 5 ((𝜑𝑚 ∈ ℕ) → ((𝐼‘(1st ‘(𝐹𝑚)))‘(2nd ‘(𝐹𝑚))) ∈ ((ℝ × ℝ) ↑m 𝑋))
234233, 109fmptd 6860 . . . 4 (𝜑𝐺:ℕ⟶((ℝ × ℝ) ↑m 𝑋))
235 simpl 486 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → 𝜑)
23686, 82eleqtrd 2892 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → (𝐼𝑛) ∈ {𝑖 ∈ (𝐶‘(𝐴𝑛)) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛)))})
23783, 236sseldi 3913 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → (𝐼𝑛) ∈ (𝐶‘(𝐴𝑛)))
238 simp3 1135 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ ∧ (𝐼𝑛) ∈ (𝐶‘(𝐴𝑛))) → (𝐼𝑛) ∈ (𝐶‘(𝐴𝑛)))
239493adant3 1129 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ ∧ (𝐼𝑛) ∈ (𝐶‘(𝐴𝑛))) → (𝐶‘(𝐴𝑛)) = { ∈ (((ℝ × ℝ) ↑m 𝑋) ↑m ℕ) ∣ (𝐴𝑛) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘)})
240238, 239eleqtrd 2892 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ ∧ (𝐼𝑛) ∈ (𝐶‘(𝐴𝑛))) → (𝐼𝑛) ∈ { ∈ (((ℝ × ℝ) ↑m 𝑋) ↑m ℕ) ∣ (𝐴𝑛) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘)})
241 fveq1 6649 . . . . . . . . . . . . . . . . 17 ( = (𝐼𝑛) → (𝑗) = ((𝐼𝑛)‘𝑗))
242241coeq2d 5698 . . . . . . . . . . . . . . . 16 ( = (𝐼𝑛) → ([,) ∘ (𝑗)) = ([,) ∘ ((𝐼𝑛)‘𝑗)))
243242fveq1d 6652 . . . . . . . . . . . . . . 15 ( = (𝐼𝑛) → (([,) ∘ (𝑗))‘𝑘) = (([,) ∘ ((𝐼𝑛)‘𝑗))‘𝑘))
244243ixpeq2dv 8467 . . . . . . . . . . . . . 14 ( = (𝐼𝑛) → X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘) = X𝑘𝑋 (([,) ∘ ((𝐼𝑛)‘𝑗))‘𝑘))
245244iuneq2d 4911 . . . . . . . . . . . . 13 ( = (𝐼𝑛) → 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘) = 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ ((𝐼𝑛)‘𝑗))‘𝑘))
246245sseq2d 3947 . . . . . . . . . . . 12 ( = (𝐼𝑛) → ((𝐴𝑛) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘) ↔ (𝐴𝑛) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ ((𝐼𝑛)‘𝑗))‘𝑘)))
247246elrab 3628 . . . . . . . . . . 11 ((𝐼𝑛) ∈ { ∈ (((ℝ × ℝ) ↑m 𝑋) ↑m ℕ) ∣ (𝐴𝑛) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑗))‘𝑘)} ↔ ((𝐼𝑛) ∈ (((ℝ × ℝ) ↑m 𝑋) ↑m ℕ) ∧ (𝐴𝑛) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ ((𝐼𝑛)‘𝑗))‘𝑘)))
248240, 247sylib 221 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ ∧ (𝐼𝑛) ∈ (𝐶‘(𝐴𝑛))) → ((𝐼𝑛) ∈ (((ℝ × ℝ) ↑m 𝑋) ↑m ℕ) ∧ (𝐴𝑛) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ ((𝐼𝑛)‘𝑗))‘𝑘)))
249248simprd 499 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ ∧ (𝐼𝑛) ∈ (𝐶‘(𝐴𝑛))) → (𝐴𝑛) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ ((𝐼𝑛)‘𝑗))‘𝑘))
250235, 4, 237, 249syl3anc 1368 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → (𝐴𝑛) ⊆ 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ ((𝐼𝑛)‘𝑗))‘𝑘))
251 f1ofo 6601 . . . . . . . . . . . . . 14 (𝐹:ℕ–1-1-onto→(ℕ × ℕ) → 𝐹:ℕ–onto→(ℕ × ℕ))
25220, 251syl 17 . . . . . . . . . . . . 13 (𝜑𝐹:ℕ–onto→(ℕ × ℕ))
253252ad2antrr 725 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → 𝐹:ℕ–onto→(ℕ × ℕ))
254 opelxpi 5557 . . . . . . . . . . . . 13 ((𝑛 ∈ ℕ ∧ 𝑗 ∈ ℕ) → ⟨𝑛, 𝑗⟩ ∈ (ℕ × ℕ))
2554, 254sylan 583 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → ⟨𝑛, 𝑗⟩ ∈ (ℕ × ℕ))
256 foelrni 6707 . . . . . . . . . . . 12 ((𝐹:ℕ–onto→(ℕ × ℕ) ∧ ⟨𝑛, 𝑗⟩ ∈ (ℕ × ℕ)) → ∃𝑚 ∈ ℕ (𝐹𝑚) = ⟨𝑛, 𝑗⟩)
257253, 255, 256syl2anc 587 . . . . . . . . . . 11 (((𝜑𝑛 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → ∃𝑚 ∈ ℕ (𝐹𝑚) = ⟨𝑛, 𝑗⟩)
258 nfv 1915 . . . . . . . . . . . 12 𝑚((𝜑𝑛 ∈ ℕ) ∧ 𝑗 ∈ ℕ)
259 nfre1 3265 . . . . . . . . . . . 12 𝑚𝑚 ∈ {𝑖 ∈ ℕ ∣ (1st ‘(𝐹𝑖)) = 𝑛}X𝑘𝑋 (([,) ∘ ((𝐼𝑛)‘𝑗))‘𝑘) ⊆ X𝑘𝑋 (([,) ∘ (𝐺𝑚))‘𝑘)
260 simpl 486 . . . . . . . . . . . . . . . . 17 ((𝑚 ∈ ℕ ∧ (𝐹𝑚) = ⟨𝑛, 𝑗⟩) → 𝑚 ∈ ℕ)
261 fveq2 6650 . . . . . . . . . . . . . . . . . . 19 ((𝐹𝑚) = ⟨𝑛, 𝑗⟩ → (1st ‘(𝐹𝑚)) = (1st ‘⟨𝑛, 𝑗⟩))
262 op1stg 7690 . . . . . . . . . . . . . . . . . . . . 21 ((𝑛 ∈ V ∧ 𝑗 ∈ V) → (1st ‘⟨𝑛, 𝑗⟩) = 𝑛)
263262el2v 3448 . . . . . . . . . . . . . . . . . . . 20 (1st ‘⟨𝑛, 𝑗⟩) = 𝑛
264263a1i 11 . . . . . . . . . . . . . . . . . . 19 ((𝐹𝑚) = ⟨𝑛, 𝑗⟩ → (1st ‘⟨𝑛, 𝑗⟩) = 𝑛)
265261, 264eqtrd 2833 . . . . . . . . . . . . . . . . . 18 ((𝐹𝑚) = ⟨𝑛, 𝑗⟩ → (1st ‘(𝐹𝑚)) = 𝑛)
266265adantl 485 . . . . . . . . . . . . . . . . 17 ((𝑚 ∈ ℕ ∧ (𝐹𝑚) = ⟨𝑛, 𝑗⟩) → (1st ‘(𝐹𝑚)) = 𝑛)
267260, 266jca 515 . . . . . . . . . . . . . . . 16 ((𝑚 ∈ ℕ ∧ (𝐹𝑚) = ⟨𝑛, 𝑗⟩) → (𝑚 ∈ ℕ ∧ (1st ‘(𝐹𝑚)) = 𝑛))
268 2fveq3 6655 . . . . . . . . . . . . . . . . . 18 (𝑖 = 𝑚 → (1st ‘(𝐹𝑖)) = (1st ‘(𝐹𝑚)))
269268eqeq1d 2800 . . . . . . . . . . . . . . . . 17 (𝑖 = 𝑚 → ((1st ‘(𝐹𝑖)) = 𝑛 ↔ (1st ‘(𝐹𝑚)) = 𝑛))
270269elrab 3628 . . . . . . . . . . . . . . . 16 (𝑚 ∈ {𝑖 ∈ ℕ ∣ (1st ‘(𝐹𝑖)) = 𝑛} ↔ (𝑚 ∈ ℕ ∧ (1st ‘(𝐹𝑚)) = 𝑛))
271267, 270sylibr 237 . . . . . . . . . . . . . . 15 ((𝑚 ∈ ℕ ∧ (𝐹𝑚) = ⟨𝑛, 𝑗⟩) → 𝑚 ∈ {𝑖 ∈ ℕ ∣ (1st ‘(𝐹𝑖)) = 𝑛})
2722713adant1 1127 . . . . . . . . . . . . . 14 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑗 ∈ ℕ) ∧ 𝑚 ∈ ℕ ∧ (𝐹𝑚) = ⟨𝑛, 𝑗⟩) → 𝑚 ∈ {𝑖 ∈ ℕ ∣ (1st ‘(𝐹𝑖)) = 𝑛})
273260, 111syl 17 . . . . . . . . . . . . . . . . . . . 20 ((𝑚 ∈ ℕ ∧ (𝐹𝑚) = ⟨𝑛, 𝑗⟩) → (𝐺𝑚) = ((𝐼‘(1st ‘(𝐹𝑚)))‘(2nd ‘(𝐹𝑚))))
274265fveq2d 6654 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐹𝑚) = ⟨𝑛, 𝑗⟩ → (𝐼‘(1st ‘(𝐹𝑚))) = (𝐼𝑛))
275 vex 3444 . . . . . . . . . . . . . . . . . . . . . . 23 𝑛 ∈ V
276 vex 3444 . . . . . . . . . . . . . . . . . . . . . . 23 𝑗 ∈ V
277275, 276op2ndd 7689 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐹𝑚) = ⟨𝑛, 𝑗⟩ → (2nd ‘(𝐹𝑚)) = 𝑗)
278274, 277fveq12d 6657 . . . . . . . . . . . . . . . . . . . . 21 ((𝐹𝑚) = ⟨𝑛, 𝑗⟩ → ((𝐼‘(1st ‘(𝐹𝑚)))‘(2nd ‘(𝐹𝑚))) = ((𝐼𝑛)‘𝑗))
279278adantl 485 . . . . . . . . . . . . . . . . . . . 20 ((𝑚 ∈ ℕ ∧ (𝐹𝑚) = ⟨𝑛, 𝑗⟩) → ((𝐼‘(1st ‘(𝐹𝑚)))‘(2nd ‘(𝐹𝑚))) = ((𝐼𝑛)‘𝑗))
280273, 279eqtr2d 2834 . . . . . . . . . . . . . . . . . . 19 ((𝑚 ∈ ℕ ∧ (𝐹𝑚) = ⟨𝑛, 𝑗⟩) → ((𝐼𝑛)‘𝑗) = (𝐺𝑚))
281280coeq2d 5698 . . . . . . . . . . . . . . . . . 18 ((𝑚 ∈ ℕ ∧ (𝐹𝑚) = ⟨𝑛, 𝑗⟩) → ([,) ∘ ((𝐼𝑛)‘𝑗)) = ([,) ∘ (𝐺𝑚)))
282281fveq1d 6652 . . . . . . . . . . . . . . . . 17 ((𝑚 ∈ ℕ ∧ (𝐹𝑚) = ⟨𝑛, 𝑗⟩) → (([,) ∘ ((𝐼𝑛)‘𝑗))‘𝑘) = (([,) ∘ (𝐺𝑚))‘𝑘))
283282ixpeq2dv 8467 . . . . . . . . . . . . . . . 16 ((𝑚 ∈ ℕ ∧ (𝐹𝑚) = ⟨𝑛, 𝑗⟩) → X𝑘𝑋 (([,) ∘ ((𝐼𝑛)‘𝑗))‘𝑘) = X𝑘𝑋 (([,) ∘ (𝐺𝑚))‘𝑘))
284 eqimss 3971 . . . . . . . . . . . . . . . 16 (X𝑘𝑋 (([,) ∘ ((𝐼𝑛)‘𝑗))‘𝑘) = X𝑘𝑋 (([,) ∘ (𝐺𝑚))‘𝑘) → X𝑘𝑋 (([,) ∘ ((𝐼𝑛)‘𝑗))‘𝑘) ⊆ X𝑘𝑋 (([,) ∘ (𝐺𝑚))‘𝑘))
285283, 284syl 17 . . . . . . . . . . . . . . 15 ((𝑚 ∈ ℕ ∧ (𝐹𝑚) = ⟨𝑛, 𝑗⟩) → X𝑘𝑋 (([,) ∘ ((𝐼𝑛)‘𝑗))‘𝑘) ⊆ X𝑘𝑋 (([,) ∘ (𝐺𝑚))‘𝑘))
2862853adant1 1127 . . . . . . . . . . . . . 14 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑗 ∈ ℕ) ∧ 𝑚 ∈ ℕ ∧ (𝐹𝑚) = ⟨𝑛, 𝑗⟩) → X𝑘𝑋 (([,) ∘ ((𝐼𝑛)‘𝑗))‘𝑘) ⊆ X𝑘𝑋 (([,) ∘ (𝐺𝑚))‘𝑘))
287 rspe 3263 . . . . . . . . . . . . . 14 ((𝑚 ∈ {𝑖 ∈ ℕ ∣ (1st ‘(𝐹𝑖)) = 𝑛} ∧ X𝑘𝑋 (([,) ∘ ((𝐼𝑛)‘𝑗))‘𝑘) ⊆ X𝑘𝑋 (([,) ∘ (𝐺𝑚))‘𝑘)) → ∃𝑚 ∈ {𝑖 ∈ ℕ ∣ (1st ‘(𝐹𝑖)) = 𝑛}X𝑘𝑋 (([,) ∘ ((𝐼𝑛)‘𝑗))‘𝑘) ⊆ X𝑘𝑋 (([,) ∘ (𝐺𝑚))‘𝑘))
288272, 286, 287syl2anc 587 . . . . . . . . . . . . 13 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑗 ∈ ℕ) ∧ 𝑚 ∈ ℕ ∧ (𝐹𝑚) = ⟨𝑛, 𝑗⟩) → ∃𝑚 ∈ {𝑖 ∈ ℕ ∣ (1st ‘(𝐹𝑖)) = 𝑛}X𝑘𝑋 (([,) ∘ ((𝐼𝑛)‘𝑗))‘𝑘) ⊆ X𝑘𝑋 (([,) ∘ (𝐺𝑚))‘𝑘))
2892883exp 1116 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → (𝑚 ∈ ℕ → ((𝐹𝑚) = ⟨𝑛, 𝑗⟩ → ∃𝑚 ∈ {𝑖 ∈ ℕ ∣ (1st ‘(𝐹𝑖)) = 𝑛}X𝑘𝑋 (([,) ∘ ((𝐼𝑛)‘𝑗))‘𝑘) ⊆ X𝑘𝑋 (([,) ∘ (𝐺𝑚))‘𝑘))))
290258, 259, 289rexlimd 3276 . . . . . . . . . . 11 (((𝜑𝑛 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → (∃𝑚 ∈ ℕ (𝐹𝑚) = ⟨𝑛, 𝑗⟩ → ∃𝑚 ∈ {𝑖 ∈ ℕ ∣ (1st ‘(𝐹𝑖)) = 𝑛}X𝑘𝑋 (([,) ∘ ((𝐼𝑛)‘𝑗))‘𝑘) ⊆ X𝑘𝑋 (([,) ∘ (𝐺𝑚))‘𝑘)))
291257, 290mpd 15 . . . . . . . . . 10 (((𝜑𝑛 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → ∃𝑚 ∈ {𝑖 ∈ ℕ ∣ (1st ‘(𝐹𝑖)) = 𝑛}X𝑘𝑋 (([,) ∘ ((𝐼𝑛)‘𝑗))‘𝑘) ⊆ X𝑘𝑋 (([,) ∘ (𝐺𝑚))‘𝑘))
292291ralrimiva 3149 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → ∀𝑗 ∈ ℕ ∃𝑚 ∈ {𝑖 ∈ ℕ ∣ (1st ‘(𝐹𝑖)) = 𝑛}X𝑘𝑋 (([,) ∘ ((𝐼𝑛)‘𝑗))‘𝑘) ⊆ X𝑘𝑋 (([,) ∘ (𝐺𝑚))‘𝑘))
293 iunss2 4937 . . . . . . . . 9 (∀𝑗 ∈ ℕ ∃𝑚 ∈ {𝑖 ∈ ℕ ∣ (1st ‘(𝐹𝑖)) = 𝑛}X𝑘𝑋 (([,) ∘ ((𝐼𝑛)‘𝑗))‘𝑘) ⊆ X𝑘𝑋 (([,) ∘ (𝐺𝑚))‘𝑘) → 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ ((𝐼𝑛)‘𝑗))‘𝑘) ⊆ 𝑚 ∈ {𝑖 ∈ ℕ ∣ (1st ‘(𝐹𝑖)) = 𝑛}X𝑘𝑋 (([,) ∘ (𝐺𝑚))‘𝑘))
294292, 293syl 17 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ ((𝐼𝑛)‘𝑗))‘𝑘) ⊆ 𝑚 ∈ {𝑖 ∈ ℕ ∣ (1st ‘(𝐹𝑖)) = 𝑛}X𝑘𝑋 (([,) ∘ (𝐺𝑚))‘𝑘))
295250, 294sstrd 3925 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → (𝐴𝑛) ⊆ 𝑚 ∈ {𝑖 ∈ ℕ ∣ (1st ‘(𝐹𝑖)) = 𝑛}X𝑘𝑋 (([,) ∘ (𝐺𝑚))‘𝑘))
296 ssrab2 4007 . . . . . . . . 9 {𝑖 ∈ ℕ ∣ (1st ‘(𝐹𝑖)) = 𝑛} ⊆ ℕ
297 iunss1 4896 . . . . . . . . 9 ({𝑖 ∈ ℕ ∣ (1st ‘(𝐹𝑖)) = 𝑛} ⊆ ℕ → 𝑚 ∈ {𝑖 ∈ ℕ ∣ (1st ‘(𝐹𝑖)) = 𝑛}X𝑘𝑋 (([,) ∘ (𝐺𝑚))‘𝑘) ⊆ 𝑚 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝐺𝑚))‘𝑘))
298296, 297ax-mp 5 . . . . . . . 8 𝑚 ∈ {𝑖 ∈ ℕ ∣ (1st ‘(𝐹𝑖)) = 𝑛}X𝑘𝑋 (([,) ∘ (𝐺𝑚))‘𝑘) ⊆ 𝑚 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝐺𝑚))‘𝑘)
299298a1i 11 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → 𝑚 ∈ {𝑖 ∈ ℕ ∣ (1st ‘(𝐹𝑖)) = 𝑛}X𝑘𝑋 (([,) ∘ (𝐺𝑚))‘𝑘) ⊆ 𝑚 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝐺𝑚))‘𝑘))
300295, 299sstrd 3925 . . . . . 6 ((𝜑𝑛 ∈ ℕ) → (𝐴𝑛) ⊆ 𝑚 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝐺𝑚))‘𝑘))
301300ralrimiva 3149 . . . . 5 (𝜑 → ∀𝑛 ∈ ℕ (𝐴𝑛) ⊆ 𝑚 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝐺𝑚))‘𝑘))
302 iunss 4933 . . . . 5 ( 𝑛 ∈ ℕ (𝐴𝑛) ⊆ 𝑚 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝐺𝑚))‘𝑘) ↔ ∀𝑛 ∈ ℕ (𝐴𝑛) ⊆ 𝑚 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝐺𝑚))‘𝑘))
303301, 302sylibr 237 . . . 4 (𝜑 𝑛 ∈ ℕ (𝐴𝑛) ⊆ 𝑚 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝐺𝑚))‘𝑘))
3041, 126, 19, 234, 303ovnlecvr 43258 . . 3 (𝜑 → ((voln*‘𝑋)‘ 𝑛 ∈ ℕ (𝐴𝑛)) ≤ (Σ^‘(𝑚 ∈ ℕ ↦ (𝐿‘(𝐺𝑚)))))
305112fveq2d 6654 . . . . . . 7 ((𝜑𝑚 ∈ ℕ) → (𝐿‘(𝐺𝑚)) = (𝐿‘((𝐼‘(1st ‘(𝐹𝑚)))‘(2nd ‘(𝐹𝑚)))))
306305mpteq2dva 5126 . . . . . 6 (𝜑 → (𝑚 ∈ ℕ ↦ (𝐿‘(𝐺𝑚))) = (𝑚 ∈ ℕ ↦ (𝐿‘((𝐼‘(1st ‘(𝐹𝑚)))‘(2nd ‘(𝐹𝑚))))))
307306fveq2d 6654 . . . . 5 (𝜑 → (Σ^‘(𝑚 ∈ ℕ ↦ (𝐿‘(𝐺𝑚)))) = (Σ^‘(𝑚 ∈ ℕ ↦ (𝐿‘((𝐼‘(1st ‘(𝐹𝑚)))‘(2nd ‘(𝐹𝑚)))))))
308 nfv 1915 . . . . . 6 𝑝𝜑
309 2fveq3 6655 . . . . . . . 8 (𝑝 = (𝐹𝑚) → (𝐼‘(1st𝑝)) = (𝐼‘(1st ‘(𝐹𝑚))))
310 fveq2 6650 . . . . . . . 8 (𝑝 = (𝐹𝑚) → (2nd𝑝) = (2nd ‘(𝐹𝑚)))
311309, 310fveq12d 6657 . . . . . . 7 (𝑝 = (𝐹𝑚) → ((𝐼‘(1st𝑝))‘(2nd𝑝)) = ((𝐼‘(1st ‘(𝐹𝑚)))‘(2nd ‘(𝐹𝑚))))
312311fveq2d 6654 . . . . . 6 (𝑝 = (𝐹𝑚) → (𝐿‘((𝐼‘(1st𝑝))‘(2nd𝑝))) = (𝐿‘((𝐼‘(1st ‘(𝐹𝑚)))‘(2nd ‘(𝐹𝑚)))))
313 eqidd 2799 . . . . . 6 ((𝜑𝑚 ∈ ℕ) → (𝐹𝑚) = (𝐹𝑚))
314 nfv 1915 . . . . . . . 8 𝑘(𝜑𝑝 ∈ (ℕ × ℕ))
3151adantr 484 . . . . . . . 8 ((𝜑𝑝 ∈ (ℕ × ℕ)) → 𝑋 ∈ Fin)
316 simpl 486 . . . . . . . . 9 ((𝜑𝑝 ∈ (ℕ × ℕ)) → 𝜑)
317 xp1st 7710 . . . . . . . . . 10 (𝑝 ∈ (ℕ × ℕ) → (1st𝑝) ∈ ℕ)
318317adantl 485 . . . . . . . . 9 ((𝜑𝑝 ∈ (ℕ × ℕ)) → (1st𝑝) ∈ ℕ)
319 xp2nd 7711 . . . . . . . . . 10 (𝑝 ∈ (ℕ × ℕ) → (2nd𝑝) ∈ ℕ)
320319adantl 485 . . . . . . . . 9 ((𝜑𝑝 ∈ (ℕ × ℕ)) → (2nd𝑝) ∈ ℕ)
321 fvex 6663 . . . . . . . . . 10 (2nd𝑝) ∈ V
322 eleq1 2877 . . . . . . . . . . . 12 (𝑗 = (2nd𝑝) → (𝑗 ∈ ℕ ↔ (2nd𝑝) ∈ ℕ))
3233223anbi3d 1439 . . . . . . . . . . 11 (𝑗 = (2nd𝑝) → ((𝜑 ∧ (1st𝑝) ∈ ℕ ∧ 𝑗 ∈ ℕ) ↔ (𝜑 ∧ (1st𝑝) ∈ ℕ ∧ (2nd𝑝) ∈ ℕ)))
324 fveq2 6650 . . . . . . . . . . . 12 (𝑗 = (2nd𝑝) → ((𝐼‘(1st𝑝))‘𝑗) = ((𝐼‘(1st𝑝))‘(2nd𝑝)))
325324feq1d 6475 . . . . . . . . . . 11 (𝑗 = (2nd𝑝) → (((𝐼‘(1st𝑝))‘𝑗):𝑋⟶(ℝ × ℝ) ↔ ((𝐼‘(1st𝑝))‘(2nd𝑝)):𝑋⟶(ℝ × ℝ)))
326323, 325imbi12d 348 . . . . . . . . . 10 (𝑗 = (2nd𝑝) → (((𝜑 ∧ (1st𝑝) ∈ ℕ ∧ 𝑗 ∈ ℕ) → ((𝐼‘(1st𝑝))‘𝑗):𝑋⟶(ℝ × ℝ)) ↔ ((𝜑 ∧ (1st𝑝) ∈ ℕ ∧ (2nd𝑝) ∈ ℕ) → ((𝐼‘(1st𝑝))‘(2nd𝑝)):𝑋⟶(ℝ × ℝ))))
327 fvex 6663 . . . . . . . . . . 11 (1st𝑝) ∈ V
328 eleq1 2877 . . . . . . . . . . . . 13 (𝑛 = (1st𝑝) → (𝑛 ∈ ℕ ↔ (1st𝑝) ∈ ℕ))
3293283anbi2d 1438 . . . . . . . . . . . 12 (𝑛 = (1st𝑝) → ((𝜑𝑛 ∈ ℕ ∧ 𝑗 ∈ ℕ) ↔ (𝜑 ∧ (1st𝑝) ∈ ℕ ∧ 𝑗 ∈ ℕ)))
330 fveq2 6650 . . . . . . . . . . . . . 14 (𝑛 = (1st𝑝) → (𝐼𝑛) = (𝐼‘(1st𝑝)))
331330fveq1d 6652 . . . . . . . . . . . . 13 (𝑛 = (1st𝑝) → ((𝐼𝑛)‘𝑗) = ((𝐼‘(1st𝑝))‘𝑗))
332331feq1d 6475 . . . . . . . . . . . 12 (𝑛 = (1st𝑝) → (((𝐼𝑛)‘𝑗):𝑋⟶(ℝ × ℝ) ↔ ((𝐼‘(1st𝑝))‘𝑗):𝑋⟶(ℝ × ℝ)))
333329, 332imbi12d 348 . . . . . . . . . . 11 (𝑛 = (1st𝑝) → (((𝜑𝑛 ∈ ℕ ∧ 𝑗 ∈ ℕ) → ((𝐼𝑛)‘𝑗):𝑋⟶(ℝ × ℝ)) ↔ ((𝜑 ∧ (1st𝑝) ∈ ℕ ∧ 𝑗 ∈ ℕ) → ((𝐼‘(1st𝑝))‘𝑗):𝑋⟶(ℝ × ℝ))))
334327, 333, 102vtocl 3507 . . . . . . . . . 10 ((𝜑 ∧ (1st𝑝) ∈ ℕ ∧ 𝑗 ∈ ℕ) → ((𝐼‘(1st𝑝))‘𝑗):𝑋⟶(ℝ × ℝ))
335321, 326, 334vtocl 3507 . . . . . . . . 9 ((𝜑 ∧ (1st𝑝) ∈ ℕ ∧ (2nd𝑝) ∈ ℕ) → ((𝐼‘(1st𝑝))‘(2nd𝑝)):𝑋⟶(ℝ × ℝ))
336316, 318, 320, 335syl3anc 1368 . . . . . . . 8 ((𝜑𝑝 ∈ (ℕ × ℕ)) → ((𝐼‘(1st𝑝))‘(2nd𝑝)):𝑋⟶(ℝ × ℝ))
337314, 315, 19, 336hoiprodcl2 43255 . . . . . . 7 ((𝜑𝑝 ∈ (ℕ × ℕ)) → (𝐿‘((𝐼‘(1st𝑝))‘(2nd𝑝))) ∈ (0[,)+∞))
33815, 337sseldi 3913 . . . . . 6 ((𝜑𝑝 ∈ (ℕ × ℕ)) → (𝐿‘((𝐼‘(1st𝑝))‘(2nd𝑝))) ∈ (0[,]+∞))
339308, 12, 312, 14, 20, 313, 338sge0f1o 43082 . . . . 5 (𝜑 → (Σ^‘(𝑝 ∈ (ℕ × ℕ) ↦ (𝐿‘((𝐼‘(1st𝑝))‘(2nd𝑝))))) = (Σ^‘(𝑚 ∈ ℕ ↦ (𝐿‘((𝐼‘(1st ‘(𝐹𝑚)))‘(2nd ‘(𝐹𝑚)))))))
340307, 339eqtr4d 2836 . . . 4 (𝜑 → (Σ^‘(𝑚 ∈ ℕ ↦ (𝐿‘(𝐺𝑚)))) = (Σ^‘(𝑝 ∈ (ℕ × ℕ) ↦ (𝐿‘((𝐼‘(1st𝑝))‘(2nd𝑝))))))
341 nfv 1915 . . . . . . 7 𝑗𝜑
342275, 276op1std 7688 . . . . . . . . . 10 (𝑝 = ⟨𝑛, 𝑗⟩ → (1st𝑝) = 𝑛)
343342fveq2d 6654 . . . . . . . . 9 (𝑝 = ⟨𝑛, 𝑗⟩ → (𝐼‘(1st𝑝)) = (𝐼𝑛))
344275, 276op2ndd 7689 . . . . . . . . 9 (𝑝 = ⟨𝑛, 𝑗⟩ → (2nd𝑝) = 𝑗)
345343, 344fveq12d 6657 . . . . . . . 8 (𝑝 = ⟨𝑛, 𝑗⟩ → ((𝐼‘(1st𝑝))‘(2nd𝑝)) = ((𝐼𝑛)‘𝑗))
346345fveq2d 6654 . . . . . . 7 (𝑝 = ⟨𝑛, 𝑗⟩ → (𝐿‘((𝐼‘(1st𝑝))‘(2nd𝑝))) = (𝐿‘((𝐼𝑛)‘𝑗)))
347 nfv 1915 . . . . . . . . . 10 𝑘((𝜑𝑛 ∈ ℕ) ∧ 𝑗 ∈ ℕ)
348123adantr 484 . . . . . . . . . 10 (((𝜑𝑛 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → 𝑋 ∈ Fin)
34993, 101syl 17 . . . . . . . . . 10 (((𝜑𝑛 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → ((𝐼𝑛)‘𝑗):𝑋⟶(ℝ × ℝ))
350347, 348, 19, 349hoiprodcl2 43255 . . . . . . . . 9 (((𝜑𝑛 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → (𝐿‘((𝐼𝑛)‘𝑗)) ∈ (0[,)+∞))
35115, 350sseldi 3913 . . . . . . . 8 (((𝜑𝑛 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → (𝐿‘((𝐼𝑛)‘𝑗)) ∈ (0[,]+∞))
3523513impa 1107 . . . . . . 7 ((𝜑𝑛 ∈ ℕ ∧ 𝑗 ∈ ℕ) → (𝐿‘((𝐼𝑛)‘𝑗)) ∈ (0[,]+∞))
353341, 346, 14, 14, 352sge0xp 43129 . . . . . 6 (𝜑 → (Σ^‘(𝑛 ∈ ℕ ↦ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘((𝐼𝑛)‘𝑗)))))) = (Σ^‘(𝑝 ∈ (ℕ × ℕ) ↦ (𝐿‘((𝐼‘(1st𝑝))‘(2nd𝑝))))))
354353eqcomd 2804 . . . . 5 (𝜑 → (Σ^‘(𝑝 ∈ (ℕ × ℕ) ↦ (𝐿‘((𝐼‘(1st𝑝))‘(2nd𝑝))))) = (Σ^‘(𝑛 ∈ ℕ ↦ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘((𝐼𝑛)‘𝑗)))))))
35513a1i 11 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → ℕ ∈ V)
356 eqid 2798 . . . . . . . 8 (𝑗 ∈ ℕ ↦ (𝐿‘((𝐼𝑛)‘𝑗))) = (𝑗 ∈ ℕ ↦ (𝐿‘((𝐼𝑛)‘𝑗)))
357351, 356fmptd 6860 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → (𝑗 ∈ ℕ ↦ (𝐿‘((𝐼𝑛)‘𝑗))):ℕ⟶(0[,]+∞))
358355, 357sge0cl 43081 . . . . . 6 ((𝜑𝑛 ∈ ℕ) → (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘((𝐼𝑛)‘𝑗)))) ∈ (0[,]+∞))
359 fveq1 6649 . . . . . . . . . . . . 13 (𝑖 = (𝐼𝑛) → (𝑖𝑗) = ((𝐼𝑛)‘𝑗))
360359fveq2d 6654 . . . . . . . . . . . 12 (𝑖 = (𝐼𝑛) → (𝐿‘(𝑖𝑗)) = (𝐿‘((𝐼𝑛)‘𝑗)))
361360mpteq2dv 5127 . . . . . . . . . . 11 (𝑖 = (𝐼𝑛) → (𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗))) = (𝑗 ∈ ℕ ↦ (𝐿‘((𝐼𝑛)‘𝑗))))
362361fveq2d 6654 . . . . . . . . . 10 (𝑖 = (𝐼𝑛) → (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) = (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘((𝐼𝑛)‘𝑗)))))
363362breq1d 5041 . . . . . . . . 9 (𝑖 = (𝐼𝑛) → ((Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛))) ↔ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘((𝐼𝑛)‘𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛)))))
364363elrab 3628 . . . . . . . 8 ((𝐼𝑛) ∈ {𝑖 ∈ (𝐶‘(𝐴𝑛)) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛)))} ↔ ((𝐼𝑛) ∈ (𝐶‘(𝐴𝑛)) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘((𝐼𝑛)‘𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛)))))
365236, 364sylib 221 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → ((𝐼𝑛) ∈ (𝐶‘(𝐴𝑛)) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘((𝐼𝑛)‘𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛)))))
366365simprd 499 . . . . . 6 ((𝜑𝑛 ∈ ℕ) → (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘((𝐼𝑛)‘𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛))))
367118, 14, 358, 173, 366sge0lempt 43110 . . . . 5 (𝜑 → (Σ^‘(𝑛 ∈ ℕ ↦ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘((𝐼𝑛)‘𝑗)))))) ≤ (Σ^‘(𝑛 ∈ ℕ ↦ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛))))))
368354, 367eqbrtrd 5053 . . . 4 (𝜑 → (Σ^‘(𝑝 ∈ (ℕ × ℕ) ↦ (𝐿‘((𝐼‘(1st𝑝))‘(2nd𝑝))))) ≤ (Σ^‘(𝑛 ∈ ℕ ↦ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛))))))
369340, 368eqbrtrd 5053 . . 3 (𝜑 → (Σ^‘(𝑚 ∈ ℕ ↦ (𝐿‘(𝐺𝑚)))) ≤ (Σ^‘(𝑛 ∈ ℕ ↦ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛))))))
37011, 117, 174, 304, 369xrletrd 12550 . 2 (𝜑 → ((voln*‘𝑋)‘ 𝑛 ∈ ℕ (𝐴𝑛)) ≤ (Σ^‘(𝑛 ∈ ℕ ↦ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛))))))
371118, 14, 160, 168sge0xadd 43135 . . 3 (𝜑 → (Σ^‘(𝑛 ∈ ℕ ↦ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛))))) = ((Σ^‘(𝑛 ∈ ℕ ↦ ((voln*‘𝑋)‘(𝐴𝑛)))) +𝑒^‘(𝑛 ∈ ℕ ↦ (𝐸 / (2↑𝑛))))))
372119a1i 11 . . . . . 6 (𝜑 → 0 ∈ ℝ*)
373121a1i 11 . . . . . 6 (𝜑 → +∞ ∈ ℝ*)
374145rexrd 10687 . . . . . 6 (𝜑𝐸 ∈ ℝ*)
37570rpge0d 12430 . . . . . 6 (𝜑 → 0 ≤ 𝐸)
376145ltpnfd 12511 . . . . . 6 (𝜑𝐸 < +∞)
377372, 373, 374, 375, 376elicod 12782 . . . . 5 (𝜑𝐸 ∈ (0[,)+∞))
378377sge0ad2en 43131 . . . 4 (𝜑 → (Σ^‘(𝑛 ∈ ℕ ↦ (𝐸 / (2↑𝑛)))) = 𝐸)
379378oveq2d 7156 . . 3 (𝜑 → ((Σ^‘(𝑛 ∈ ℕ ↦ ((voln*‘𝑋)‘(𝐴𝑛)))) +𝑒^‘(𝑛 ∈ ℕ ↦ (𝐸 / (2↑𝑛))))) = ((Σ^‘(𝑛 ∈ ℕ ↦ ((voln*‘𝑋)‘(𝐴𝑛)))) +𝑒 𝐸))
380371, 379eqtrd 2833 . 2 (𝜑 → (Σ^‘(𝑛 ∈ ℕ ↦ (((voln*‘𝑋)‘(𝐴𝑛)) +𝑒 (𝐸 / (2↑𝑛))))) = ((Σ^‘(𝑛 ∈ ℕ ↦ ((voln*‘𝑋)‘(𝐴𝑛)))) +𝑒 𝐸))
381370, 380breqtrd 5057 1 (𝜑 → ((voln*‘𝑋)‘ 𝑛 ∈ ℕ (𝐴𝑛)) ≤ ((Σ^‘(𝑛 ∈ ℕ ↦ ((voln*‘𝑋)‘(𝐴𝑛)))) +𝑒 𝐸))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1084   = wceq 1538   ∈ wcel 2111   ≠ wne 2987  ∀wral 3106  ∃wrex 3107  {crab 3110  Vcvv 3441   ⊆ wss 3881  ∅c0 4243  ifcif 4425  𝒫 cpw 4497  ⟨cop 4531  ∪ ciun 4882   class class class wbr 5031   ↦ cmpt 5111   × cxp 5518   ∘ ccom 5524   Fn wfn 6322  ⟶wf 6323  –onto→wfo 6325  –1-1-onto→wf1o 6326  ‘cfv 6327  (class class class)co 7140  1st c1st 7676  2nd c2nd 7677   ↑m cmap 8396  Xcixp 8451  Fincfn 8499  infcinf 8896  ℝcr 10532  0cc0 10533  +∞cpnf 10668  ℝ*cxr 10670   < clt 10671   ≤ cle 10672   / cdiv 11293  ℕcn 11632  2c2 11687  ℝ+crp 12384   +𝑒 cxad 12500  [,)cico 12735  [,]cicc 12736  ↑cexp 13432  ∏cprod 15258  volcvol 24081  Σ^csumge0 43062  voln*covoln 43236 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-rep 5155  ax-sep 5168  ax-nul 5175  ax-pow 5232  ax-pr 5296  ax-un 7448  ax-inf2 9095  ax-ac2 9881  ax-cnex 10589  ax-resscn 10590  ax-1cn 10591  ax-icn 10592  ax-addcl 10593  ax-addrcl 10594  ax-mulcl 10595  ax-mulrcl 10596  ax-mulcom 10597  ax-addass 10598  ax-mulass 10599  ax-distr 10600  ax-i2m1 10601  ax-1ne0 10602  ax-1rid 10603  ax-rnegex 10604  ax-rrecex 10605  ax-cnre 10606  ax-pre-lttri 10607  ax-pre-lttrn 10608  ax-pre-ltadd 10609  ax-pre-mulgt0 10610  ax-pre-sup 10611  ax-addf 10612  ax-mulf 10613 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-nel 3092  df-ral 3111  df-rex 3112  df-reu 3113  df-rmo 3114  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-pss 3900  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-tp 4530  df-op 4532  df-uni 4802  df-int 4840  df-iun 4884  df-disj 4997  df-br 5032  df-opab 5094  df-mpt 5112  df-tr 5138  df-id 5426  df-eprel 5431  df-po 5439  df-so 5440  df-fr 5479  df-se 5480  df-we 5481  df-xp 5526  df-rel 5527  df-cnv 5528  df-co 5529  df-dm 5530  df-rn 5531  df-res 5532  df-ima 5533  df-pred 6119  df-ord 6165  df-on 6166  df-lim 6167  df-suc 6168  df-iota 6286  df-fun 6329  df-fn 6330  df-f 6331  df-f1 6332  df-fo 6333  df-f1o 6334  df-fv 6335  df-isom 6336  df-riota 7098  df-ov 7143  df-oprab 7144  df-mpo 7145  df-of 7395  df-om 7568  df-1st 7678  df-2nd 7679  df-tpos 7882  df-wrecs 7937  df-recs 7998  df-rdg 8036  df-1o 8092  df-2o 8093  df-oadd 8096  df-er 8279  df-map 8398  df-pm 8399  df-ixp 8452  df-en 8500  df-dom 8501  df-sdom 8502  df-fin 8503  df-fi 8866  df-sup 8897  df-inf 8898  df-oi 8965  df-dju 9321  df-card 9359  df-acn 9362  df-ac 9534  df-pnf 10673  df-mnf 10674  df-xr 10675  df-ltxr 10676  df-le 10677  df-sub 10868  df-neg 10869  df-div 11294  df-nn 11633  df-2 11695  df-3 11696  df-4 11697  df-5 11698  df-6 11699  df-7 11700  df-8 11701  df-9 11702  df-n0 11893  df-z 11977  df-dec 12094  df-uz 12239  df-q 12344  df-rp 12385  df-xneg 12502  df-xadd 12503  df-xmul 12504  df-ioo 12737  df-ico 12739  df-icc 12740  df-fz 12893  df-fzo 13036  df-fl 13164  df-seq 13372  df-exp 13433  df-hash 13694  df-cj 14457  df-re 14458  df-im 14459  df-sqrt 14593  df-abs 14594  df-clim 14844  df-rlim 14845  df-sum 15042  df-prod 15259  df-struct 16484  df-ndx 16485  df-slot 16486  df-base 16488  df-sets 16489  df-ress 16490  df-plusg 16577  df-mulr 16578  df-starv 16579  df-tset 16583  df-ple 16584  df-ds 16586  df-unif 16587  df-rest 16695  df-0g 16714  df-topgen 16716  df-mgm 17851  df-sgrp 17900  df-mnd 17911  df-grp 18105  df-minusg 18106  df-subg 18276  df-cmn 18908  df-abl 18909  df-mgp 19241  df-ur 19253  df-ring 19300  df-cring 19301  df-oppr 19377  df-dvdsr 19395  df-unit 19396  df-invr 19426  df-dvr 19437  df-drng 19505  df-psmet 20091  df-xmet 20092  df-met 20093  df-bl 20094  df-mopn 20095  df-cnfld 20100  df-top 21513  df-topon 21530  df-bases 21565  df-cmp 22006  df-ovol 24082  df-vol 24083  df-sumge0 43063  df-ovoln 43237 This theorem is referenced by:  ovnsubaddlem2  43271
 Copyright terms: Public domain W3C validator