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 45221
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 482 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ 𝐴:β„•βŸΆπ’« (ℝ ↑m 𝑋))
4 simpr 486 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ 𝑛 ∈ β„•)
53, 4ffvelcdmd 7083 . . . . . . 7 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (π΄β€˜π‘›) ∈ 𝒫 (ℝ ↑m 𝑋))
6 elpwi 4608 . . . . . . 7 ((π΄β€˜π‘›) ∈ 𝒫 (ℝ ↑m 𝑋) β†’ (π΄β€˜π‘›) βŠ† (ℝ ↑m 𝑋))
75, 6syl 17 . . . . . 6 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (π΄β€˜π‘›) βŠ† (ℝ ↑m 𝑋))
87ralrimiva 3147 . . . . 5 (πœ‘ β†’ βˆ€π‘› ∈ β„• (π΄β€˜π‘›) βŠ† (ℝ ↑m 𝑋))
9 iunss 5047 . . . . 5 (βˆͺ 𝑛 ∈ β„• (π΄β€˜π‘›) βŠ† (ℝ ↑m 𝑋) ↔ βˆ€π‘› ∈ β„• (π΄β€˜π‘›) βŠ† (ℝ ↑m 𝑋))
108, 9sylibr 233 . . . 4 (πœ‘ β†’ βˆͺ 𝑛 ∈ β„• (π΄β€˜π‘›) βŠ† (ℝ ↑m 𝑋))
111, 10ovnxrcl 45220 . . 3 (πœ‘ β†’ ((voln*β€˜π‘‹)β€˜βˆͺ 𝑛 ∈ β„• (π΄β€˜π‘›)) ∈ ℝ*)
12 nfv 1918 . . . 4 β„²π‘šπœ‘
13 nnex 12214 . . . . 5 β„• ∈ V
1413a1i 11 . . . 4 (πœ‘ β†’ β„• ∈ V)
15 icossicc 13409 . . . . 5 (0[,)+∞) βŠ† (0[,]+∞)
16 nfv 1918 . . . . . 6 β„²π‘˜(πœ‘ ∧ π‘š ∈ β„•)
17 simpl 484 . . . . . . 7 ((πœ‘ ∧ π‘š ∈ β„•) β†’ πœ‘)
1817, 1syl 17 . . . . . 6 ((πœ‘ ∧ π‘š ∈ β„•) β†’ 𝑋 ∈ Fin)
19 ovnsubaddlem1.l . . . . . 6 𝐿 = (𝑖 ∈ ((ℝ Γ— ℝ) ↑m 𝑋) ↦ βˆπ‘˜ ∈ 𝑋 (volβ€˜(([,) ∘ 𝑖)β€˜π‘˜)))
20 ovnsubaddlem1.f . . . . . . . . . . . 12 (πœ‘ β†’ 𝐹:ℕ–1-1-ontoβ†’(β„• Γ— β„•))
21 f1of 6830 . . . . . . . . . . . 12 (𝐹:ℕ–1-1-ontoβ†’(β„• Γ— β„•) β†’ 𝐹:β„•βŸΆ(β„• Γ— β„•))
2220, 21syl 17 . . . . . . . . . . 11 (πœ‘ β†’ 𝐹:β„•βŸΆ(β„• Γ— β„•))
2322adantr 482 . . . . . . . . . 10 ((πœ‘ ∧ π‘š ∈ β„•) β†’ 𝐹:β„•βŸΆ(β„• Γ— β„•))
24 simpr 486 . . . . . . . . . 10 ((πœ‘ ∧ π‘š ∈ β„•) β†’ π‘š ∈ β„•)
2523, 24ffvelcdmd 7083 . . . . . . . . 9 ((πœ‘ ∧ π‘š ∈ β„•) β†’ (πΉβ€˜π‘š) ∈ (β„• Γ— β„•))
26 xp1st 8002 . . . . . . . . 9 ((πΉβ€˜π‘š) ∈ (β„• Γ— β„•) β†’ (1st β€˜(πΉβ€˜π‘š)) ∈ β„•)
2725, 26syl 17 . . . . . . . 8 ((πœ‘ ∧ π‘š ∈ β„•) β†’ (1st β€˜(πΉβ€˜π‘š)) ∈ β„•)
28 xp2nd 8003 . . . . . . . . 9 ((πΉβ€˜π‘š) ∈ (β„• Γ— β„•) β†’ (2nd β€˜(πΉβ€˜π‘š)) ∈ β„•)
2925, 28syl 17 . . . . . . . 8 ((πœ‘ ∧ π‘š ∈ β„•) β†’ (2nd β€˜(πΉβ€˜π‘š)) ∈ β„•)
30 fvex 6901 . . . . . . . . 9 (2nd β€˜(πΉβ€˜π‘š)) ∈ V
31 eleq1 2822 . . . . . . . . . . 11 (𝑗 = (2nd β€˜(πΉβ€˜π‘š)) β†’ (𝑗 ∈ β„• ↔ (2nd β€˜(πΉβ€˜π‘š)) ∈ β„•))
32313anbi3d 1443 . . . . . . . . . 10 (𝑗 = (2nd β€˜(πΉβ€˜π‘š)) β†’ ((πœ‘ ∧ (1st β€˜(πΉβ€˜π‘š)) ∈ β„• ∧ 𝑗 ∈ β„•) ↔ (πœ‘ ∧ (1st β€˜(πΉβ€˜π‘š)) ∈ β„• ∧ (2nd β€˜(πΉβ€˜π‘š)) ∈ β„•)))
33 fveq2 6888 . . . . . . . . . . 11 (𝑗 = (2nd β€˜(πΉβ€˜π‘š)) β†’ ((πΌβ€˜(1st β€˜(πΉβ€˜π‘š)))β€˜π‘—) = ((πΌβ€˜(1st β€˜(πΉβ€˜π‘š)))β€˜(2nd β€˜(πΉβ€˜π‘š))))
3433feq1d 6699 . . . . . . . . . 10 (𝑗 = (2nd β€˜(πΉβ€˜π‘š)) β†’ (((πΌβ€˜(1st β€˜(πΉβ€˜π‘š)))β€˜π‘—):π‘‹βŸΆ(ℝ Γ— ℝ) ↔ ((πΌβ€˜(1st β€˜(πΉβ€˜π‘š)))β€˜(2nd β€˜(πΉβ€˜π‘š))):π‘‹βŸΆ(ℝ Γ— ℝ)))
3532, 34imbi12d 345 . . . . . . . . 9 (𝑗 = (2nd β€˜(πΉβ€˜π‘š)) β†’ (((πœ‘ ∧ (1st β€˜(πΉβ€˜π‘š)) ∈ β„• ∧ 𝑗 ∈ β„•) β†’ ((πΌβ€˜(1st β€˜(πΉβ€˜π‘š)))β€˜π‘—):π‘‹βŸΆ(ℝ Γ— ℝ)) ↔ ((πœ‘ ∧ (1st β€˜(πΉβ€˜π‘š)) ∈ β„• ∧ (2nd β€˜(πΉβ€˜π‘š)) ∈ β„•) β†’ ((πΌβ€˜(1st β€˜(πΉβ€˜π‘š)))β€˜(2nd β€˜(πΉβ€˜π‘š))):π‘‹βŸΆ(ℝ Γ— ℝ))))
36 fvex 6901 . . . . . . . . . 10 (1st β€˜(πΉβ€˜π‘š)) ∈ V
37 eleq1 2822 . . . . . . . . . . . 12 (𝑛 = (1st β€˜(πΉβ€˜π‘š)) β†’ (𝑛 ∈ β„• ↔ (1st β€˜(πΉβ€˜π‘š)) ∈ β„•))
38373anbi2d 1442 . . . . . . . . . . 11 (𝑛 = (1st β€˜(πΉβ€˜π‘š)) β†’ ((πœ‘ ∧ 𝑛 ∈ β„• ∧ 𝑗 ∈ β„•) ↔ (πœ‘ ∧ (1st β€˜(πΉβ€˜π‘š)) ∈ β„• ∧ 𝑗 ∈ β„•)))
39 fveq2 6888 . . . . . . . . . . . . 13 (𝑛 = (1st β€˜(πΉβ€˜π‘š)) β†’ (πΌβ€˜π‘›) = (πΌβ€˜(1st β€˜(πΉβ€˜π‘š))))
4039fveq1d 6890 . . . . . . . . . . . 12 (𝑛 = (1st β€˜(πΉβ€˜π‘š)) β†’ ((πΌβ€˜π‘›)β€˜π‘—) = ((πΌβ€˜(1st β€˜(πΉβ€˜π‘š)))β€˜π‘—))
4140feq1d 6699 . . . . . . . . . . 11 (𝑛 = (1st β€˜(πΉβ€˜π‘š)) β†’ (((πΌβ€˜π‘›)β€˜π‘—):π‘‹βŸΆ(ℝ Γ— ℝ) ↔ ((πΌβ€˜(1st β€˜(πΉβ€˜π‘š)))β€˜π‘—):π‘‹βŸΆ(ℝ Γ— ℝ)))
4238, 41imbi12d 345 . . . . . . . . . 10 (𝑛 = (1st β€˜(πΉβ€˜π‘š)) β†’ (((πœ‘ ∧ 𝑛 ∈ β„• ∧ 𝑗 ∈ β„•) β†’ ((πΌβ€˜π‘›)β€˜π‘—):π‘‹βŸΆ(ℝ Γ— ℝ)) ↔ ((πœ‘ ∧ (1st β€˜(πΉβ€˜π‘š)) ∈ β„• ∧ 𝑗 ∈ β„•) β†’ ((πΌβ€˜(1st β€˜(πΉβ€˜π‘š)))β€˜π‘—):π‘‹βŸΆ(ℝ Γ— ℝ))))
43 ovnsubaddlem1.c . . . . . . . . . . . . . . . . . . 19 𝐢 = (π‘Ž ∈ 𝒫 (ℝ ↑m 𝑋) ↦ {β„Ž ∈ (((ℝ Γ— ℝ) ↑m 𝑋) ↑m β„•) ∣ π‘Ž βŠ† βˆͺ 𝑗 ∈ β„• Xπ‘˜ ∈ 𝑋 (([,) ∘ (β„Žβ€˜π‘—))β€˜π‘˜)})
44 sseq1 4006 . . . . . . . . . . . . . . . . . . . 20 (π‘Ž = (π΄β€˜π‘›) β†’ (π‘Ž βŠ† βˆͺ 𝑗 ∈ β„• Xπ‘˜ ∈ 𝑋 (([,) ∘ (β„Žβ€˜π‘—))β€˜π‘˜) ↔ (π΄β€˜π‘›) βŠ† βˆͺ 𝑗 ∈ β„• Xπ‘˜ ∈ 𝑋 (([,) ∘ (β„Žβ€˜π‘—))β€˜π‘˜)))
4544rabbidv 3441 . . . . . . . . . . . . . . . . . . 19 (π‘Ž = (π΄β€˜π‘›) β†’ {β„Ž ∈ (((ℝ Γ— ℝ) ↑m 𝑋) ↑m β„•) ∣ π‘Ž βŠ† βˆͺ 𝑗 ∈ β„• Xπ‘˜ ∈ 𝑋 (([,) ∘ (β„Žβ€˜π‘—))β€˜π‘˜)} = {β„Ž ∈ (((ℝ Γ— ℝ) ↑m 𝑋) ↑m β„•) ∣ (π΄β€˜π‘›) βŠ† βˆͺ 𝑗 ∈ β„• Xπ‘˜ ∈ 𝑋 (([,) ∘ (β„Žβ€˜π‘—))β€˜π‘˜)})
46 ovex 7437 . . . . . . . . . . . . . . . . . . . . 21 (((ℝ Γ— ℝ) ↑m 𝑋) ↑m β„•) ∈ V
4746rabex 5331 . . . . . . . . . . . . . . . . . . . 20 {β„Ž ∈ (((ℝ Γ— ℝ) ↑m 𝑋) ↑m β„•) ∣ (π΄β€˜π‘›) βŠ† βˆͺ 𝑗 ∈ β„• Xπ‘˜ ∈ 𝑋 (([,) ∘ (β„Žβ€˜π‘—))β€˜π‘˜)} ∈ V
4847a1i 11 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ {β„Ž ∈ (((ℝ Γ— ℝ) ↑m 𝑋) ↑m β„•) ∣ (π΄β€˜π‘›) βŠ† βˆͺ 𝑗 ∈ β„• Xπ‘˜ ∈ 𝑋 (([,) ∘ (β„Žβ€˜π‘—))β€˜π‘˜)} ∈ V)
4943, 45, 5, 48fvmptd3 7017 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (πΆβ€˜(π΄β€˜π‘›)) = {β„Ž ∈ (((ℝ Γ— ℝ) ↑m 𝑋) ↑m β„•) ∣ (π΄β€˜π‘›) βŠ† βˆͺ 𝑗 ∈ β„• Xπ‘˜ ∈ 𝑋 (([,) ∘ (β„Žβ€˜π‘—))β€˜π‘˜)})
50 ssrab2 4076 . . . . . . . . . . . . . . . . . . 19 {β„Ž ∈ (((ℝ Γ— ℝ) ↑m 𝑋) ↑m β„•) ∣ (π΄β€˜π‘›) βŠ† βˆͺ 𝑗 ∈ β„• Xπ‘˜ ∈ 𝑋 (([,) ∘ (β„Žβ€˜π‘—))β€˜π‘˜)} βŠ† (((ℝ Γ— ℝ) ↑m 𝑋) ↑m β„•)
5150a1i 11 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ {β„Ž ∈ (((ℝ Γ— ℝ) ↑m 𝑋) ↑m β„•) ∣ (π΄β€˜π‘›) βŠ† βˆͺ 𝑗 ∈ β„• Xπ‘˜ ∈ 𝑋 (([,) ∘ (β„Žβ€˜π‘—))β€˜π‘˜)} βŠ† (((ℝ Γ— ℝ) ↑m 𝑋) ↑m β„•))
5249, 51eqsstrd 4019 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (πΆβ€˜(π΄β€˜π‘›)) βŠ† (((ℝ Γ— ℝ) ↑m 𝑋) ↑m β„•))
53 ovnsubaddlem1.d . . . . . . . . . . . . . . . . . . . . 21 𝐷 = (π‘Ž ∈ 𝒫 (ℝ ↑m 𝑋) ↦ (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (πΆβ€˜π‘Ž) ∣ (Ξ£^β€˜(𝑗 ∈ β„• ↦ (πΏβ€˜(π‘–β€˜π‘—)))) ≀ (((voln*β€˜π‘‹)β€˜π‘Ž) +𝑒 𝑒)}))
54 fveq2 6888 . . . . . . . . . . . . . . . . . . . . . . . . 25 (π‘Ž = (π΄β€˜π‘›) β†’ (πΆβ€˜π‘Ž) = (πΆβ€˜(π΄β€˜π‘›)))
5554eleq2d 2820 . . . . . . . . . . . . . . . . . . . . . . . 24 (π‘Ž = (π΄β€˜π‘›) β†’ (𝑖 ∈ (πΆβ€˜π‘Ž) ↔ 𝑖 ∈ (πΆβ€˜(π΄β€˜π‘›))))
56 fveq2 6888 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (π‘Ž = (π΄β€˜π‘›) β†’ ((voln*β€˜π‘‹)β€˜π‘Ž) = ((voln*β€˜π‘‹)β€˜(π΄β€˜π‘›)))
5756oveq1d 7419 . . . . . . . . . . . . . . . . . . . . . . . . 25 (π‘Ž = (π΄β€˜π‘›) β†’ (((voln*β€˜π‘‹)β€˜π‘Ž) +𝑒 𝑒) = (((voln*β€˜π‘‹)β€˜(π΄β€˜π‘›)) +𝑒 𝑒))
5857breq2d 5159 . . . . . . . . . . . . . . . . . . . . . . . 24 (π‘Ž = (π΄β€˜π‘›) β†’ ((Ξ£^β€˜(𝑗 ∈ β„• ↦ (πΏβ€˜(π‘–β€˜π‘—)))) ≀ (((voln*β€˜π‘‹)β€˜π‘Ž) +𝑒 𝑒) ↔ (Ξ£^β€˜(𝑗 ∈ β„• ↦ (πΏβ€˜(π‘–β€˜π‘—)))) ≀ (((voln*β€˜π‘‹)β€˜(π΄β€˜π‘›)) +𝑒 𝑒)))
5955, 58anbi12d 632 . . . . . . . . . . . . . . . . . . . . . . 23 (π‘Ž = (π΄β€˜π‘›) β†’ ((𝑖 ∈ (πΆβ€˜π‘Ž) ∧ (Ξ£^β€˜(𝑗 ∈ β„• ↦ (πΏβ€˜(π‘–β€˜π‘—)))) ≀ (((voln*β€˜π‘‹)β€˜π‘Ž) +𝑒 𝑒)) ↔ (𝑖 ∈ (πΆβ€˜(π΄β€˜π‘›)) ∧ (Ξ£^β€˜(𝑗 ∈ β„• ↦ (πΏβ€˜(π‘–β€˜π‘—)))) ≀ (((voln*β€˜π‘‹)β€˜(π΄β€˜π‘›)) +𝑒 𝑒))))
6059rabbidva2 3435 . . . . . . . . . . . . . . . . . . . . . 22 (π‘Ž = (π΄β€˜π‘›) β†’ {𝑖 ∈ (πΆβ€˜π‘Ž) ∣ (Ξ£^β€˜(𝑗 ∈ β„• ↦ (πΏβ€˜(π‘–β€˜π‘—)))) ≀ (((voln*β€˜π‘‹)β€˜π‘Ž) +𝑒 𝑒)} = {𝑖 ∈ (πΆβ€˜(π΄β€˜π‘›)) ∣ (Ξ£^β€˜(𝑗 ∈ β„• ↦ (πΏβ€˜(π‘–β€˜π‘—)))) ≀ (((voln*β€˜π‘‹)β€˜(π΄β€˜π‘›)) +𝑒 𝑒)})
6160mpteq2dv 5249 . . . . . . . . . . . . . . . . . . . . 21 (π‘Ž = (π΄β€˜π‘›) β†’ (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (πΆβ€˜π‘Ž) ∣ (Ξ£^β€˜(𝑗 ∈ β„• ↦ (πΏβ€˜(π‘–β€˜π‘—)))) ≀ (((voln*β€˜π‘‹)β€˜π‘Ž) +𝑒 𝑒)}) = (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (πΆβ€˜(π΄β€˜π‘›)) ∣ (Ξ£^β€˜(𝑗 ∈ β„• ↦ (πΏβ€˜(π‘–β€˜π‘—)))) ≀ (((voln*β€˜π‘‹)β€˜(π΄β€˜π‘›)) +𝑒 𝑒)}))
62 rpex 43991 . . . . . . . . . . . . . . . . . . . . . . 23 ℝ+ ∈ V
6362mptex 7220 . . . . . . . . . . . . . . . . . . . . . 22 (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (πΆβ€˜(π΄β€˜π‘›)) ∣ (Ξ£^β€˜(𝑗 ∈ β„• ↦ (πΏβ€˜(π‘–β€˜π‘—)))) ≀ (((voln*β€˜π‘‹)β€˜(π΄β€˜π‘›)) +𝑒 𝑒)}) ∈ V
6463a1i 11 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (πΆβ€˜(π΄β€˜π‘›)) ∣ (Ξ£^β€˜(𝑗 ∈ β„• ↦ (πΏβ€˜(π‘–β€˜π‘—)))) ≀ (((voln*β€˜π‘‹)β€˜(π΄β€˜π‘›)) +𝑒 𝑒)}) ∈ V)
6553, 61, 5, 64fvmptd3 7017 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (π·β€˜(π΄β€˜π‘›)) = (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (πΆβ€˜(π΄β€˜π‘›)) ∣ (Ξ£^β€˜(𝑗 ∈ β„• ↦ (πΏβ€˜(π‘–β€˜π‘—)))) ≀ (((voln*β€˜π‘‹)β€˜(π΄β€˜π‘›)) +𝑒 𝑒)}))
66 oveq2 7412 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑒 = (𝐸 / (2↑𝑛)) β†’ (((voln*β€˜π‘‹)β€˜(π΄β€˜π‘›)) +𝑒 𝑒) = (((voln*β€˜π‘‹)β€˜(π΄β€˜π‘›)) +𝑒 (𝐸 / (2↑𝑛))))
6766breq2d 5159 . . . . . . . . . . . . . . . . . . . . . 22 (𝑒 = (𝐸 / (2↑𝑛)) β†’ ((Ξ£^β€˜(𝑗 ∈ β„• ↦ (πΏβ€˜(π‘–β€˜π‘—)))) ≀ (((voln*β€˜π‘‹)β€˜(π΄β€˜π‘›)) +𝑒 𝑒) ↔ (Ξ£^β€˜(𝑗 ∈ β„• ↦ (πΏβ€˜(π‘–β€˜π‘—)))) ≀ (((voln*β€˜π‘‹)β€˜(π΄β€˜π‘›)) +𝑒 (𝐸 / (2↑𝑛)))))
6867rabbidv 3441 . . . . . . . . . . . . . . . . . . . . 21 (𝑒 = (𝐸 / (2↑𝑛)) β†’ {𝑖 ∈ (πΆβ€˜(π΄β€˜π‘›)) ∣ (Ξ£^β€˜(𝑗 ∈ β„• ↦ (πΏβ€˜(π‘–β€˜π‘—)))) ≀ (((voln*β€˜π‘‹)β€˜(π΄β€˜π‘›)) +𝑒 𝑒)} = {𝑖 ∈ (πΆβ€˜(π΄β€˜π‘›)) ∣ (Ξ£^β€˜(𝑗 ∈ β„• ↦ (πΏβ€˜(π‘–β€˜π‘—)))) ≀ (((voln*β€˜π‘‹)β€˜(π΄β€˜π‘›)) +𝑒 (𝐸 / (2↑𝑛)))})
6968adantl 483 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑒 = (𝐸 / (2↑𝑛))) β†’ {𝑖 ∈ (πΆβ€˜(π΄β€˜π‘›)) ∣ (Ξ£^β€˜(𝑗 ∈ β„• ↦ (πΏβ€˜(π‘–β€˜π‘—)))) ≀ (((voln*β€˜π‘‹)β€˜(π΄β€˜π‘›)) +𝑒 𝑒)} = {𝑖 ∈ (πΆβ€˜(π΄β€˜π‘›)) ∣ (Ξ£^β€˜(𝑗 ∈ β„• ↦ (πΏβ€˜(π‘–β€˜π‘—)))) ≀ (((voln*β€˜π‘‹)β€˜(π΄β€˜π‘›)) +𝑒 (𝐸 / (2↑𝑛)))})
70 ovnsubaddlem1.e . . . . . . . . . . . . . . . . . . . . . 22 (πœ‘ β†’ 𝐸 ∈ ℝ+)
7170adantr 482 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ 𝐸 ∈ ℝ+)
72 2nn 12281 . . . . . . . . . . . . . . . . . . . . . . . . 25 2 ∈ β„•
7372a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 ∈ β„• β†’ 2 ∈ β„•)
74 nnnn0 12475 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 ∈ β„• β†’ 𝑛 ∈ β„•0)
7573, 74nnexpcld 14204 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 ∈ β„• β†’ (2↑𝑛) ∈ β„•)
7675nnrpd 13010 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 ∈ β„• β†’ (2↑𝑛) ∈ ℝ+)
7776adantl 483 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (2↑𝑛) ∈ ℝ+)
7871, 77rpdivcld 13029 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (𝐸 / (2↑𝑛)) ∈ ℝ+)
79 fvex 6901 . . . . . . . . . . . . . . . . . . . . . 22 (πΆβ€˜(π΄β€˜π‘›)) ∈ V
8079rabex 5331 . . . . . . . . . . . . . . . . . . . . 21 {𝑖 ∈ (πΆβ€˜(π΄β€˜π‘›)) ∣ (Ξ£^β€˜(𝑗 ∈ β„• ↦ (πΏβ€˜(π‘–β€˜π‘—)))) ≀ (((voln*β€˜π‘‹)β€˜(π΄β€˜π‘›)) +𝑒 (𝐸 / (2↑𝑛)))} ∈ V
8180a1i 11 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ {𝑖 ∈ (πΆβ€˜(π΄β€˜π‘›)) ∣ (Ξ£^β€˜(𝑗 ∈ β„• ↦ (πΏβ€˜(π‘–β€˜π‘—)))) ≀ (((voln*β€˜π‘‹)β€˜(π΄β€˜π‘›)) +𝑒 (𝐸 / (2↑𝑛)))} ∈ V)
8265, 69, 78, 81fvmptd 7001 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ ((π·β€˜(π΄β€˜π‘›))β€˜(𝐸 / (2↑𝑛))) = {𝑖 ∈ (πΆβ€˜(π΄β€˜π‘›)) ∣ (Ξ£^β€˜(𝑗 ∈ β„• ↦ (πΏβ€˜(π‘–β€˜π‘—)))) ≀ (((voln*β€˜π‘‹)β€˜(π΄β€˜π‘›)) +𝑒 (𝐸 / (2↑𝑛)))})
83 ssrab2 4076 . . . . . . . . . . . . . . . . . . . 20 {𝑖 ∈ (πΆβ€˜(π΄β€˜π‘›)) ∣ (Ξ£^β€˜(𝑗 ∈ β„• ↦ (πΏβ€˜(π‘–β€˜π‘—)))) ≀ (((voln*β€˜π‘‹)β€˜(π΄β€˜π‘›)) +𝑒 (𝐸 / (2↑𝑛)))} βŠ† (πΆβ€˜(π΄β€˜π‘›))
8483a1i 11 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ {𝑖 ∈ (πΆβ€˜(π΄β€˜π‘›)) ∣ (Ξ£^β€˜(𝑗 ∈ β„• ↦ (πΏβ€˜(π‘–β€˜π‘—)))) ≀ (((voln*β€˜π‘‹)β€˜(π΄β€˜π‘›)) +𝑒 (𝐸 / (2↑𝑛)))} βŠ† (πΆβ€˜(π΄β€˜π‘›)))
8582, 84eqsstrd 4019 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ ((π·β€˜(π΄β€˜π‘›))β€˜(𝐸 / (2↑𝑛))) βŠ† (πΆβ€˜(π΄β€˜π‘›)))
86 ovnsubaddlem1.i . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (πΌβ€˜π‘›) ∈ ((π·β€˜(π΄β€˜π‘›))β€˜(𝐸 / (2↑𝑛))))
8785, 86sseldd 3982 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (πΌβ€˜π‘›) ∈ (πΆβ€˜(π΄β€˜π‘›)))
8852, 87sseldd 3982 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (πΌβ€˜π‘›) ∈ (((ℝ Γ— ℝ) ↑m 𝑋) ↑m β„•))
89 elmapfn 8855 . . . . . . . . . . . . . . . 16 ((πΌβ€˜π‘›) ∈ (((ℝ Γ— ℝ) ↑m 𝑋) ↑m β„•) β†’ (πΌβ€˜π‘›) Fn β„•)
9088, 89syl 17 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (πΌβ€˜π‘›) Fn β„•)
91 elmapi 8839 . . . . . . . . . . . . . . . . . 18 ((πΌβ€˜π‘›) ∈ (((ℝ Γ— ℝ) ↑m 𝑋) ↑m β„•) β†’ (πΌβ€˜π‘›):β„•βŸΆ((ℝ Γ— ℝ) ↑m 𝑋))
9288, 91syl 17 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (πΌβ€˜π‘›):β„•βŸΆ((ℝ Γ— ℝ) ↑m 𝑋))
9392ffvelcdmda 7082 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑗 ∈ β„•) β†’ ((πΌβ€˜π‘›)β€˜π‘—) ∈ ((ℝ Γ— ℝ) ↑m 𝑋))
9493ralrimiva 3147 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ βˆ€π‘— ∈ β„• ((πΌβ€˜π‘›)β€˜π‘—) ∈ ((ℝ Γ— ℝ) ↑m 𝑋))
9590, 94jca 513 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ ((πΌβ€˜π‘›) Fn β„• ∧ βˆ€π‘— ∈ β„• ((πΌβ€˜π‘›)β€˜π‘—) ∈ ((ℝ Γ— ℝ) ↑m 𝑋)))
96953adant3 1133 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑛 ∈ β„• ∧ 𝑗 ∈ β„•) β†’ ((πΌβ€˜π‘›) Fn β„• ∧ βˆ€π‘— ∈ β„• ((πΌβ€˜π‘›)β€˜π‘—) ∈ ((ℝ Γ— ℝ) ↑m 𝑋)))
97 ffnfv 7113 . . . . . . . . . . . . 13 ((πΌβ€˜π‘›):β„•βŸΆ((ℝ Γ— ℝ) ↑m 𝑋) ↔ ((πΌβ€˜π‘›) Fn β„• ∧ βˆ€π‘— ∈ β„• ((πΌβ€˜π‘›)β€˜π‘—) ∈ ((ℝ Γ— ℝ) ↑m 𝑋)))
9896, 97sylibr 233 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑛 ∈ β„• ∧ 𝑗 ∈ β„•) β†’ (πΌβ€˜π‘›):β„•βŸΆ((ℝ Γ— ℝ) ↑m 𝑋))
99 simp3 1139 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑛 ∈ β„• ∧ 𝑗 ∈ β„•) β†’ 𝑗 ∈ β„•)
10098, 99ffvelcdmd 7083 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑛 ∈ β„• ∧ 𝑗 ∈ β„•) β†’ ((πΌβ€˜π‘›)β€˜π‘—) ∈ ((ℝ Γ— ℝ) ↑m 𝑋))
101 elmapi 8839 . . . . . . . . . . 11 (((πΌβ€˜π‘›)β€˜π‘—) ∈ ((ℝ Γ— ℝ) ↑m 𝑋) β†’ ((πΌβ€˜π‘›)β€˜π‘—):π‘‹βŸΆ(ℝ Γ— ℝ))
102100, 101syl 17 . . . . . . . . . 10 ((πœ‘ ∧ 𝑛 ∈ β„• ∧ 𝑗 ∈ β„•) β†’ ((πΌβ€˜π‘›)β€˜π‘—):π‘‹βŸΆ(ℝ Γ— ℝ))
10336, 42, 102vtocl 3549 . . . . . . . . 9 ((πœ‘ ∧ (1st β€˜(πΉβ€˜π‘š)) ∈ β„• ∧ 𝑗 ∈ β„•) β†’ ((πΌβ€˜(1st β€˜(πΉβ€˜π‘š)))β€˜π‘—):π‘‹βŸΆ(ℝ Γ— ℝ))
10430, 35, 103vtocl 3549 . . . . . . . 8 ((πœ‘ ∧ (1st β€˜(πΉβ€˜π‘š)) ∈ β„• ∧ (2nd β€˜(πΉβ€˜π‘š)) ∈ β„•) β†’ ((πΌβ€˜(1st β€˜(πΉβ€˜π‘š)))β€˜(2nd β€˜(πΉβ€˜π‘š))):π‘‹βŸΆ(ℝ Γ— ℝ))
10517, 27, 29, 104syl3anc 1372 . . . . . . 7 ((πœ‘ ∧ π‘š ∈ β„•) β†’ ((πΌβ€˜(1st β€˜(πΉβ€˜π‘š)))β€˜(2nd β€˜(πΉβ€˜π‘š))):π‘‹βŸΆ(ℝ Γ— ℝ))
106 id 22 . . . . . . . . . 10 (π‘š ∈ β„• β†’ π‘š ∈ β„•)
107 fvex 6901 . . . . . . . . . . 11 ((πΌβ€˜(1st β€˜(πΉβ€˜π‘š)))β€˜(2nd β€˜(πΉβ€˜π‘š))) ∈ V
108107a1i 11 . . . . . . . . . 10 (π‘š ∈ β„• β†’ ((πΌβ€˜(1st β€˜(πΉβ€˜π‘š)))β€˜(2nd β€˜(πΉβ€˜π‘š))) ∈ V)
109 ovnsubaddlem1.g . . . . . . . . . . 11 𝐺 = (π‘š ∈ β„• ↦ ((πΌβ€˜(1st β€˜(πΉβ€˜π‘š)))β€˜(2nd β€˜(πΉβ€˜π‘š))))
110109fvmpt2 7005 . . . . . . . . . 10 ((π‘š ∈ β„• ∧ ((πΌβ€˜(1st β€˜(πΉβ€˜π‘š)))β€˜(2nd β€˜(πΉβ€˜π‘š))) ∈ V) β†’ (πΊβ€˜π‘š) = ((πΌβ€˜(1st β€˜(πΉβ€˜π‘š)))β€˜(2nd β€˜(πΉβ€˜π‘š))))
111106, 108, 110syl2anc 585 . . . . . . . . 9 (π‘š ∈ β„• β†’ (πΊβ€˜π‘š) = ((πΌβ€˜(1st β€˜(πΉβ€˜π‘š)))β€˜(2nd β€˜(πΉβ€˜π‘š))))
112111adantl 483 . . . . . . . 8 ((πœ‘ ∧ π‘š ∈ β„•) β†’ (πΊβ€˜π‘š) = ((πΌβ€˜(1st β€˜(πΉβ€˜π‘š)))β€˜(2nd β€˜(πΉβ€˜π‘š))))
113112feq1d 6699 . . . . . . 7 ((πœ‘ ∧ π‘š ∈ β„•) β†’ ((πΊβ€˜π‘š):π‘‹βŸΆ(ℝ Γ— ℝ) ↔ ((πΌβ€˜(1st β€˜(πΉβ€˜π‘š)))β€˜(2nd β€˜(πΉβ€˜π‘š))):π‘‹βŸΆ(ℝ Γ— ℝ)))
114105, 113mpbird 257 . . . . . 6 ((πœ‘ ∧ π‘š ∈ β„•) β†’ (πΊβ€˜π‘š):π‘‹βŸΆ(ℝ Γ— ℝ))
11516, 18, 19, 114hoiprodcl2 45206 . . . . 5 ((πœ‘ ∧ π‘š ∈ β„•) β†’ (πΏβ€˜(πΊβ€˜π‘š)) ∈ (0[,)+∞))
11615, 115sselid 3979 . . . 4 ((πœ‘ ∧ π‘š ∈ β„•) β†’ (πΏβ€˜(πΊβ€˜π‘š)) ∈ (0[,]+∞))
11712, 14, 116sge0xrclmpt 45079 . . 3 (πœ‘ β†’ (Ξ£^β€˜(π‘š ∈ β„• ↦ (πΏβ€˜(πΊβ€˜π‘š)))) ∈ ℝ*)
118 nfv 1918 . . . 4 β„²π‘›πœ‘
119 0xr 11257 . . . . . 6 0 ∈ ℝ*
120119a1i 11 . . . . 5 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ 0 ∈ ℝ*)
121 pnfxr 11264 . . . . . 6 +∞ ∈ ℝ*
122121a1i 11 . . . . 5 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ +∞ ∈ ℝ*)
1231adantr 482 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ 𝑋 ∈ Fin)
124 ovnsubaddlem1.z . . . . . . . . 9 𝑍 = (π‘Ž ∈ 𝒫 (ℝ ↑m 𝑋) ↦ {𝑧 ∈ ℝ* ∣ βˆƒπ‘– ∈ (((ℝ Γ— ℝ) ↑m 𝑋) ↑m β„•)(π‘Ž βŠ† βˆͺ 𝑗 ∈ β„• Xπ‘˜ ∈ 𝑋 (([,) ∘ (π‘–β€˜π‘—))β€˜π‘˜) ∧ 𝑧 = (Ξ£^β€˜(𝑗 ∈ β„• ↦ βˆπ‘˜ ∈ 𝑋 (volβ€˜(([,) ∘ (π‘–β€˜π‘—))β€˜π‘˜)))))})
125123, 7, 124ovnval2b 45203 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ ((voln*β€˜π‘‹)β€˜(π΄β€˜π‘›)) = if(𝑋 = βˆ…, 0, inf((π‘β€˜(π΄β€˜π‘›)), ℝ*, < )))
126 ovnsubaddlem1.n0 . . . . . . . . . . 11 (πœ‘ β†’ 𝑋 β‰  βˆ…)
127126neneqd 2946 . . . . . . . . . 10 (πœ‘ β†’ Β¬ 𝑋 = βˆ…)
128127iffalsed 4538 . . . . . . . . 9 (πœ‘ β†’ if(𝑋 = βˆ…, 0, inf((π‘β€˜(π΄β€˜π‘›)), ℝ*, < )) = inf((π‘β€˜(π΄β€˜π‘›)), ℝ*, < ))
129128adantr 482 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ if(𝑋 = βˆ…, 0, inf((π‘β€˜(π΄β€˜π‘›)), ℝ*, < )) = inf((π‘β€˜(π΄β€˜π‘›)), ℝ*, < ))
130125, 129eqtrd 2773 . . . . . . 7 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ ((voln*β€˜π‘‹)β€˜(π΄β€˜π‘›)) = inf((π‘β€˜(π΄β€˜π‘›)), ℝ*, < ))
131 sseq1 4006 . . . . . . . . . . . . 13 (π‘Ž = (π΄β€˜π‘›) β†’ (π‘Ž βŠ† βˆͺ 𝑗 ∈ β„• Xπ‘˜ ∈ 𝑋 (([,) ∘ (π‘–β€˜π‘—))β€˜π‘˜) ↔ (π΄β€˜π‘›) βŠ† βˆͺ 𝑗 ∈ β„• Xπ‘˜ ∈ 𝑋 (([,) ∘ (π‘–β€˜π‘—))β€˜π‘˜)))
132131anbi1d 631 . . . . . . . . . . . 12 (π‘Ž = (π΄β€˜π‘›) β†’ ((π‘Ž βŠ† βˆͺ 𝑗 ∈ β„• Xπ‘˜ ∈ 𝑋 (([,) ∘ (π‘–β€˜π‘—))β€˜π‘˜) ∧ 𝑧 = (Ξ£^β€˜(𝑗 ∈ β„• ↦ βˆπ‘˜ ∈ 𝑋 (volβ€˜(([,) ∘ (π‘–β€˜π‘—))β€˜π‘˜))))) ↔ ((π΄β€˜π‘›) βŠ† βˆͺ 𝑗 ∈ β„• Xπ‘˜ ∈ 𝑋 (([,) ∘ (π‘–β€˜π‘—))β€˜π‘˜) ∧ 𝑧 = (Ξ£^β€˜(𝑗 ∈ β„• ↦ βˆπ‘˜ ∈ 𝑋 (volβ€˜(([,) ∘ (π‘–β€˜π‘—))β€˜π‘˜)))))))
133132rexbidv 3179 . . . . . . . . . . 11 (π‘Ž = (π΄β€˜π‘›) β†’ (βˆƒπ‘– ∈ (((ℝ Γ— ℝ) ↑m 𝑋) ↑m β„•)(π‘Ž βŠ† βˆͺ 𝑗 ∈ β„• Xπ‘˜ ∈ 𝑋 (([,) ∘ (π‘–β€˜π‘—))β€˜π‘˜) ∧ 𝑧 = (Ξ£^β€˜(𝑗 ∈ β„• ↦ βˆπ‘˜ ∈ 𝑋 (volβ€˜(([,) ∘ (π‘–β€˜π‘—))β€˜π‘˜))))) ↔ βˆƒπ‘– ∈ (((ℝ Γ— ℝ) ↑m 𝑋) ↑m β„•)((π΄β€˜π‘›) βŠ† βˆͺ 𝑗 ∈ β„• Xπ‘˜ ∈ 𝑋 (([,) ∘ (π‘–β€˜π‘—))β€˜π‘˜) ∧ 𝑧 = (Ξ£^β€˜(𝑗 ∈ β„• ↦ βˆπ‘˜ ∈ 𝑋 (volβ€˜(([,) ∘ (π‘–β€˜π‘—))β€˜π‘˜)))))))
134133rabbidv 3441 . . . . . . . . . 10 (π‘Ž = (π΄β€˜π‘›) β†’ {𝑧 ∈ ℝ* ∣ βˆƒπ‘– ∈ (((ℝ Γ— ℝ) ↑m 𝑋) ↑m β„•)(π‘Ž βŠ† βˆͺ 𝑗 ∈ β„• Xπ‘˜ ∈ 𝑋 (([,) ∘ (π‘–β€˜π‘—))β€˜π‘˜) ∧ 𝑧 = (Ξ£^β€˜(𝑗 ∈ β„• ↦ βˆπ‘˜ ∈ 𝑋 (volβ€˜(([,) ∘ (π‘–β€˜π‘—))β€˜π‘˜)))))} = {𝑧 ∈ ℝ* ∣ βˆƒπ‘– ∈ (((ℝ Γ— ℝ) ↑m 𝑋) ↑m β„•)((π΄β€˜π‘›) βŠ† βˆͺ 𝑗 ∈ β„• Xπ‘˜ ∈ 𝑋 (([,) ∘ (π‘–β€˜π‘—))β€˜π‘˜) ∧ 𝑧 = (Ξ£^β€˜(𝑗 ∈ β„• ↦ βˆπ‘˜ ∈ 𝑋 (volβ€˜(([,) ∘ (π‘–β€˜π‘—))β€˜π‘˜)))))})
135 xrex 12967 . . . . . . . . . . . 12 ℝ* ∈ V
136135rabex 5331 . . . . . . . . . . 11 {𝑧 ∈ ℝ* ∣ βˆƒπ‘– ∈ (((ℝ Γ— ℝ) ↑m 𝑋) ↑m β„•)((π΄β€˜π‘›) βŠ† βˆͺ 𝑗 ∈ β„• Xπ‘˜ ∈ 𝑋 (([,) ∘ (π‘–β€˜π‘—))β€˜π‘˜) ∧ 𝑧 = (Ξ£^β€˜(𝑗 ∈ β„• ↦ βˆπ‘˜ ∈ 𝑋 (volβ€˜(([,) ∘ (π‘–β€˜π‘—))β€˜π‘˜)))))} ∈ V
137136a1i 11 . . . . . . . . . 10 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ {𝑧 ∈ ℝ* ∣ βˆƒπ‘– ∈ (((ℝ Γ— ℝ) ↑m 𝑋) ↑m β„•)((π΄β€˜π‘›) βŠ† βˆͺ 𝑗 ∈ β„• Xπ‘˜ ∈ 𝑋 (([,) ∘ (π‘–β€˜π‘—))β€˜π‘˜) ∧ 𝑧 = (Ξ£^β€˜(𝑗 ∈ β„• ↦ βˆπ‘˜ ∈ 𝑋 (volβ€˜(([,) ∘ (π‘–β€˜π‘—))β€˜π‘˜)))))} ∈ V)
138124, 134, 5, 137fvmptd3 7017 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (π‘β€˜(π΄β€˜π‘›)) = {𝑧 ∈ ℝ* ∣ βˆƒπ‘– ∈ (((ℝ Γ— ℝ) ↑m 𝑋) ↑m β„•)((π΄β€˜π‘›) βŠ† βˆͺ 𝑗 ∈ β„• Xπ‘˜ ∈ 𝑋 (([,) ∘ (π‘–β€˜π‘—))β€˜π‘˜) ∧ 𝑧 = (Ξ£^β€˜(𝑗 ∈ β„• ↦ βˆπ‘˜ ∈ 𝑋 (volβ€˜(([,) ∘ (π‘–β€˜π‘—))β€˜π‘˜)))))})
139 ssrab2 4076 . . . . . . . . . 10 {𝑧 ∈ ℝ* ∣ βˆƒπ‘– ∈ (((ℝ Γ— ℝ) ↑m 𝑋) ↑m β„•)((π΄β€˜π‘›) βŠ† βˆͺ 𝑗 ∈ β„• Xπ‘˜ ∈ 𝑋 (([,) ∘ (π‘–β€˜π‘—))β€˜π‘˜) ∧ 𝑧 = (Ξ£^β€˜(𝑗 ∈ β„• ↦ βˆπ‘˜ ∈ 𝑋 (volβ€˜(([,) ∘ (π‘–β€˜π‘—))β€˜π‘˜)))))} βŠ† ℝ*
140139a1i 11 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ {𝑧 ∈ ℝ* ∣ βˆƒπ‘– ∈ (((ℝ Γ— ℝ) ↑m 𝑋) ↑m β„•)((π΄β€˜π‘›) βŠ† βˆͺ 𝑗 ∈ β„• Xπ‘˜ ∈ 𝑋 (([,) ∘ (π‘–β€˜π‘—))β€˜π‘˜) ∧ 𝑧 = (Ξ£^β€˜(𝑗 ∈ β„• ↦ βˆπ‘˜ ∈ 𝑋 (volβ€˜(([,) ∘ (π‘–β€˜π‘—))β€˜π‘˜)))))} βŠ† ℝ*)
141138, 140eqsstrd 4019 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (π‘β€˜(π΄β€˜π‘›)) βŠ† ℝ*)
142 infxrcl 13308 . . . . . . . 8 ((π‘β€˜(π΄β€˜π‘›)) βŠ† ℝ* β†’ inf((π‘β€˜(π΄β€˜π‘›)), ℝ*, < ) ∈ ℝ*)
143141, 142syl 17 . . . . . . 7 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ inf((π‘β€˜(π΄β€˜π‘›)), ℝ*, < ) ∈ ℝ*)
144130, 143eqeltrd 2834 . . . . . 6 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ ((voln*β€˜π‘‹)β€˜(π΄β€˜π‘›)) ∈ ℝ*)
14570rpred 13012 . . . . . . . . 9 (πœ‘ β†’ 𝐸 ∈ ℝ)
146145adantr 482 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ 𝐸 ∈ ℝ)
147 2re 12282 . . . . . . . . . . 11 2 ∈ ℝ
148147a1i 11 . . . . . . . . . 10 (𝑛 ∈ β„• β†’ 2 ∈ ℝ)
149148, 74reexpcld 14124 . . . . . . . . 9 (𝑛 ∈ β„• β†’ (2↑𝑛) ∈ ℝ)
150149adantl 483 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (2↑𝑛) ∈ ℝ)
151148recnd 11238 . . . . . . . . . 10 (𝑛 ∈ β„• β†’ 2 ∈ β„‚)
152 2ne0 12312 . . . . . . . . . . 11 2 β‰  0
153152a1i 11 . . . . . . . . . 10 (𝑛 ∈ β„• β†’ 2 β‰  0)
154 nnz 12575 . . . . . . . . . 10 (𝑛 ∈ β„• β†’ 𝑛 ∈ β„€)
155151, 153, 154expne0d 14113 . . . . . . . . 9 (𝑛 ∈ β„• β†’ (2↑𝑛) β‰  0)
156155adantl 483 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (2↑𝑛) β‰  0)
157146, 150, 156redivcld 12038 . . . . . . 7 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (𝐸 / (2↑𝑛)) ∈ ℝ)
158157rexrd 11260 . . . . . 6 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (𝐸 / (2↑𝑛)) ∈ ℝ*)
159144, 158xaddcld 13276 . . . . 5 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (((voln*β€˜π‘‹)β€˜(π΄β€˜π‘›)) +𝑒 (𝐸 / (2↑𝑛))) ∈ ℝ*)
160123, 7ovncl 45218 . . . . . . 7 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ ((voln*β€˜π‘‹)β€˜(π΄β€˜π‘›)) ∈ (0[,]+∞))
161 xrge0ge0 43992 . . . . . . 7 (((voln*β€˜π‘‹)β€˜(π΄β€˜π‘›)) ∈ (0[,]+∞) β†’ 0 ≀ ((voln*β€˜π‘‹)β€˜(π΄β€˜π‘›)))
162160, 161syl 17 . . . . . 6 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ 0 ≀ ((voln*β€˜π‘‹)β€˜(π΄β€˜π‘›)))
163 0red 11213 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ 0 ∈ ℝ)
16478rpgt0d 13015 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ 0 < (𝐸 / (2↑𝑛)))
165163, 157, 164ltled 11358 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ 0 ≀ (𝐸 / (2↑𝑛)))
166157ltpnfd 13097 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (𝐸 / (2↑𝑛)) < +∞)
167158, 122, 166xrltled 13125 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (𝐸 / (2↑𝑛)) ≀ +∞)
168120, 122, 158, 165, 167eliccxrd 44175 . . . . . . 7 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (𝐸 / (2↑𝑛)) ∈ (0[,]+∞))
169144, 168xadd0ge 43965 . . . . . 6 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ ((voln*β€˜π‘‹)β€˜(π΄β€˜π‘›)) ≀ (((voln*β€˜π‘‹)β€˜(π΄β€˜π‘›)) +𝑒 (𝐸 / (2↑𝑛))))
170120, 144, 159, 162, 169xrletrd 13137 . . . . 5 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ 0 ≀ (((voln*β€˜π‘‹)β€˜(π΄β€˜π‘›)) +𝑒 (𝐸 / (2↑𝑛))))
171 pnfge 13106 . . . . . 6 ((((voln*β€˜π‘‹)β€˜(π΄β€˜π‘›)) +𝑒 (𝐸 / (2↑𝑛))) ∈ ℝ* β†’ (((voln*β€˜π‘‹)β€˜(π΄β€˜π‘›)) +𝑒 (𝐸 / (2↑𝑛))) ≀ +∞)
172159, 171syl 17 . . . . 5 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (((voln*β€˜π‘‹)β€˜(π΄β€˜π‘›)) +𝑒 (𝐸 / (2↑𝑛))) ≀ +∞)
173120, 122, 159, 170, 172eliccxrd 44175 . . . 4 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (((voln*β€˜π‘‹)β€˜(π΄β€˜π‘›)) +𝑒 (𝐸 / (2↑𝑛))) ∈ (0[,]+∞))
174118, 14, 173sge0xrclmpt 45079 . . 3 (πœ‘ β†’ (Ξ£^β€˜(𝑛 ∈ β„• ↦ (((voln*β€˜π‘‹)β€˜(π΄β€˜π‘›)) +𝑒 (𝐸 / (2↑𝑛))))) ∈ ℝ*)
175 sseq1 4006 . . . . . . . . . . . . 13 (π‘Ž = (π΄β€˜(1st β€˜(πΉβ€˜π‘š))) β†’ (π‘Ž βŠ† βˆͺ 𝑗 ∈ β„• Xπ‘˜ ∈ 𝑋 (([,) ∘ (β„Žβ€˜π‘—))β€˜π‘˜) ↔ (π΄β€˜(1st β€˜(πΉβ€˜π‘š))) βŠ† βˆͺ 𝑗 ∈ β„• Xπ‘˜ ∈ 𝑋 (([,) ∘ (β„Žβ€˜π‘—))β€˜π‘˜)))
176175rabbidv 3441 . . . . . . . . . . . 12 (π‘Ž = (π΄β€˜(1st β€˜(πΉβ€˜π‘š))) β†’ {β„Ž ∈ (((ℝ Γ— ℝ) ↑m 𝑋) ↑m β„•) ∣ π‘Ž βŠ† βˆͺ 𝑗 ∈ β„• Xπ‘˜ ∈ 𝑋 (([,) ∘ (β„Žβ€˜π‘—))β€˜π‘˜)} = {β„Ž ∈ (((ℝ Γ— ℝ) ↑m 𝑋) ↑m β„•) ∣ (π΄β€˜(1st β€˜(πΉβ€˜π‘š))) βŠ† βˆͺ 𝑗 ∈ β„• Xπ‘˜ ∈ 𝑋 (([,) ∘ (β„Žβ€˜π‘—))β€˜π‘˜)})
1772adantr 482 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘š ∈ β„•) β†’ 𝐴:β„•βŸΆπ’« (ℝ ↑m 𝑋))
178177, 27ffvelcdmd 7083 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘š ∈ β„•) β†’ (π΄β€˜(1st β€˜(πΉβ€˜π‘š))) ∈ 𝒫 (ℝ ↑m 𝑋))
17946rabex 5331 . . . . . . . . . . . . 13 {β„Ž ∈ (((ℝ Γ— ℝ) ↑m 𝑋) ↑m β„•) ∣ (π΄β€˜(1st β€˜(πΉβ€˜π‘š))) βŠ† βˆͺ 𝑗 ∈ β„• Xπ‘˜ ∈ 𝑋 (([,) ∘ (β„Žβ€˜π‘—))β€˜π‘˜)} ∈ V
180179a1i 11 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘š ∈ β„•) β†’ {β„Ž ∈ (((ℝ Γ— ℝ) ↑m 𝑋) ↑m β„•) ∣ (π΄β€˜(1st β€˜(πΉβ€˜π‘š))) βŠ† βˆͺ 𝑗 ∈ β„• Xπ‘˜ ∈ 𝑋 (([,) ∘ (β„Žβ€˜π‘—))β€˜π‘˜)} ∈ V)
18143, 176, 178, 180fvmptd3 7017 . . . . . . . . . . 11 ((πœ‘ ∧ π‘š ∈ β„•) β†’ (πΆβ€˜(π΄β€˜(1st β€˜(πΉβ€˜π‘š)))) = {β„Ž ∈ (((ℝ Γ— ℝ) ↑m 𝑋) ↑m β„•) ∣ (π΄β€˜(1st β€˜(πΉβ€˜π‘š))) βŠ† βˆͺ 𝑗 ∈ β„• Xπ‘˜ ∈ 𝑋 (([,) ∘ (β„Žβ€˜π‘—))β€˜π‘˜)})
182 ssrab2 4076 . . . . . . . . . . . 12 {β„Ž ∈ (((ℝ Γ— ℝ) ↑m 𝑋) ↑m β„•) ∣ (π΄β€˜(1st β€˜(πΉβ€˜π‘š))) βŠ† βˆͺ 𝑗 ∈ β„• Xπ‘˜ ∈ 𝑋 (([,) ∘ (β„Žβ€˜π‘—))β€˜π‘˜)} βŠ† (((ℝ Γ— ℝ) ↑m 𝑋) ↑m β„•)
183182a1i 11 . . . . . . . . . . 11 ((πœ‘ ∧ π‘š ∈ β„•) β†’ {β„Ž ∈ (((ℝ Γ— ℝ) ↑m 𝑋) ↑m β„•) ∣ (π΄β€˜(1st β€˜(πΉβ€˜π‘š))) βŠ† βˆͺ 𝑗 ∈ β„• Xπ‘˜ ∈ 𝑋 (([,) ∘ (β„Žβ€˜π‘—))β€˜π‘˜)} βŠ† (((ℝ Γ— ℝ) ↑m 𝑋) ↑m β„•))
184181, 183eqsstrd 4019 . . . . . . . . . 10 ((πœ‘ ∧ π‘š ∈ β„•) β†’ (πΆβ€˜(π΄β€˜(1st β€˜(πΉβ€˜π‘š)))) βŠ† (((ℝ Γ— ℝ) ↑m 𝑋) ↑m β„•))
185 fveq2 6888 . . . . . . . . . . . . . . . . . 18 (π‘Ž = (π΄β€˜(1st β€˜(πΉβ€˜π‘š))) β†’ (πΆβ€˜π‘Ž) = (πΆβ€˜(π΄β€˜(1st β€˜(πΉβ€˜π‘š)))))
186185eleq2d 2820 . . . . . . . . . . . . . . . . 17 (π‘Ž = (π΄β€˜(1st β€˜(πΉβ€˜π‘š))) β†’ (𝑖 ∈ (πΆβ€˜π‘Ž) ↔ 𝑖 ∈ (πΆβ€˜(π΄β€˜(1st β€˜(πΉβ€˜π‘š))))))
187 fveq2 6888 . . . . . . . . . . . . . . . . . . 19 (π‘Ž = (π΄β€˜(1st β€˜(πΉβ€˜π‘š))) β†’ ((voln*β€˜π‘‹)β€˜π‘Ž) = ((voln*β€˜π‘‹)β€˜(π΄β€˜(1st β€˜(πΉβ€˜π‘š)))))
188187oveq1d 7419 . . . . . . . . . . . . . . . . . 18 (π‘Ž = (π΄β€˜(1st β€˜(πΉβ€˜π‘š))) β†’ (((voln*β€˜π‘‹)β€˜π‘Ž) +𝑒 𝑒) = (((voln*β€˜π‘‹)β€˜(π΄β€˜(1st β€˜(πΉβ€˜π‘š)))) +𝑒 𝑒))
189188breq2d 5159 . . . . . . . . . . . . . . . . 17 (π‘Ž = (π΄β€˜(1st β€˜(πΉβ€˜π‘š))) β†’ ((Ξ£^β€˜(𝑗 ∈ β„• ↦ (πΏβ€˜(π‘–β€˜π‘—)))) ≀ (((voln*β€˜π‘‹)β€˜π‘Ž) +𝑒 𝑒) ↔ (Ξ£^β€˜(𝑗 ∈ β„• ↦ (πΏβ€˜(π‘–β€˜π‘—)))) ≀ (((voln*β€˜π‘‹)β€˜(π΄β€˜(1st β€˜(πΉβ€˜π‘š)))) +𝑒 𝑒)))
190186, 189anbi12d 632 . . . . . . . . . . . . . . . 16 (π‘Ž = (π΄β€˜(1st β€˜(πΉβ€˜π‘š))) β†’ ((𝑖 ∈ (πΆβ€˜π‘Ž) ∧ (Ξ£^β€˜(𝑗 ∈ β„• ↦ (πΏβ€˜(π‘–β€˜π‘—)))) ≀ (((voln*β€˜π‘‹)β€˜π‘Ž) +𝑒 𝑒)) ↔ (𝑖 ∈ (πΆβ€˜(π΄β€˜(1st β€˜(πΉβ€˜π‘š)))) ∧ (Ξ£^β€˜(𝑗 ∈ β„• ↦ (πΏβ€˜(π‘–β€˜π‘—)))) ≀ (((voln*β€˜π‘‹)β€˜(π΄β€˜(1st β€˜(πΉβ€˜π‘š)))) +𝑒 𝑒))))
191190rabbidva2 3435 . . . . . . . . . . . . . . 15 (π‘Ž = (π΄β€˜(1st β€˜(πΉβ€˜π‘š))) β†’ {𝑖 ∈ (πΆβ€˜π‘Ž) ∣ (Ξ£^β€˜(𝑗 ∈ β„• ↦ (πΏβ€˜(π‘–β€˜π‘—)))) ≀ (((voln*β€˜π‘‹)β€˜π‘Ž) +𝑒 𝑒)} = {𝑖 ∈ (πΆβ€˜(π΄β€˜(1st β€˜(πΉβ€˜π‘š)))) ∣ (Ξ£^β€˜(𝑗 ∈ β„• ↦ (πΏβ€˜(π‘–β€˜π‘—)))) ≀ (((voln*β€˜π‘‹)β€˜(π΄β€˜(1st β€˜(πΉβ€˜π‘š)))) +𝑒 𝑒)})
192191mpteq2dv 5249 . . . . . . . . . . . . . 14 (π‘Ž = (π΄β€˜(1st β€˜(πΉβ€˜π‘š))) β†’ (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (πΆβ€˜π‘Ž) ∣ (Ξ£^β€˜(𝑗 ∈ β„• ↦ (πΏβ€˜(π‘–β€˜π‘—)))) ≀ (((voln*β€˜π‘‹)β€˜π‘Ž) +𝑒 𝑒)}) = (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (πΆβ€˜(π΄β€˜(1st β€˜(πΉβ€˜π‘š)))) ∣ (Ξ£^β€˜(𝑗 ∈ β„• ↦ (πΏβ€˜(π‘–β€˜π‘—)))) ≀ (((voln*β€˜π‘‹)β€˜(π΄β€˜(1st β€˜(πΉβ€˜π‘š)))) +𝑒 𝑒)}))
19362mptex 7220 . . . . . . . . . . . . . . 15 (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (πΆβ€˜(π΄β€˜(1st β€˜(πΉβ€˜π‘š)))) ∣ (Ξ£^β€˜(𝑗 ∈ β„• ↦ (πΏβ€˜(π‘–β€˜π‘—)))) ≀ (((voln*β€˜π‘‹)β€˜(π΄β€˜(1st β€˜(πΉβ€˜π‘š)))) +𝑒 𝑒)}) ∈ V
194193a1i 11 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘š ∈ β„•) β†’ (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (πΆβ€˜(π΄β€˜(1st β€˜(πΉβ€˜π‘š)))) ∣ (Ξ£^β€˜(𝑗 ∈ β„• ↦ (πΏβ€˜(π‘–β€˜π‘—)))) ≀ (((voln*β€˜π‘‹)β€˜(π΄β€˜(1st β€˜(πΉβ€˜π‘š)))) +𝑒 𝑒)}) ∈ V)
19553, 192, 178, 194fvmptd3 7017 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘š ∈ β„•) β†’ (π·β€˜(π΄β€˜(1st β€˜(πΉβ€˜π‘š)))) = (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (πΆβ€˜(π΄β€˜(1st β€˜(πΉβ€˜π‘š)))) ∣ (Ξ£^β€˜(𝑗 ∈ β„• ↦ (πΏβ€˜(π‘–β€˜π‘—)))) ≀ (((voln*β€˜π‘‹)β€˜(π΄β€˜(1st β€˜(πΉβ€˜π‘š)))) +𝑒 𝑒)}))
196 oveq2 7412 . . . . . . . . . . . . . . . 16 (𝑒 = (𝐸 / (2↑(1st β€˜(πΉβ€˜π‘š)))) β†’ (((voln*β€˜π‘‹)β€˜(π΄β€˜(1st β€˜(πΉβ€˜π‘š)))) +𝑒 𝑒) = (((voln*β€˜π‘‹)β€˜(π΄β€˜(1st β€˜(πΉβ€˜π‘š)))) +𝑒 (𝐸 / (2↑(1st β€˜(πΉβ€˜π‘š))))))
197196breq2d 5159 . . . . . . . . . . . . . . 15 (𝑒 = (𝐸 / (2↑(1st β€˜(πΉβ€˜π‘š)))) β†’ ((Ξ£^β€˜(𝑗 ∈ β„• ↦ (πΏβ€˜(π‘–β€˜π‘—)))) ≀ (((voln*β€˜π‘‹)β€˜(π΄β€˜(1st β€˜(πΉβ€˜π‘š)))) +𝑒 𝑒) ↔ (Ξ£^β€˜(𝑗 ∈ β„• ↦ (πΏβ€˜(π‘–β€˜π‘—)))) ≀ (((voln*β€˜π‘‹)β€˜(π΄β€˜(1st β€˜(πΉβ€˜π‘š)))) +𝑒 (𝐸 / (2↑(1st β€˜(πΉβ€˜π‘š)))))))
198197rabbidv 3441 . . . . . . . . . . . . . 14 (𝑒 = (𝐸 / (2↑(1st β€˜(πΉβ€˜π‘š)))) β†’ {𝑖 ∈ (πΆβ€˜(π΄β€˜(1st β€˜(πΉβ€˜π‘š)))) ∣ (Ξ£^β€˜(𝑗 ∈ β„• ↦ (πΏβ€˜(π‘–β€˜π‘—)))) ≀ (((voln*β€˜π‘‹)β€˜(π΄β€˜(1st β€˜(πΉβ€˜π‘š)))) +𝑒 𝑒)} = {𝑖 ∈ (πΆβ€˜(π΄β€˜(1st β€˜(πΉβ€˜π‘š)))) ∣ (Ξ£^β€˜(𝑗 ∈ β„• ↦ (πΏβ€˜(π‘–β€˜π‘—)))) ≀ (((voln*β€˜π‘‹)β€˜(π΄β€˜(1st β€˜(πΉβ€˜π‘š)))) +𝑒 (𝐸 / (2↑(1st β€˜(πΉβ€˜π‘š)))))})
199198adantl 483 . . . . . . . . . . . . 13 (((πœ‘ ∧ π‘š ∈ β„•) ∧ 𝑒 = (𝐸 / (2↑(1st β€˜(πΉβ€˜π‘š))))) β†’ {𝑖 ∈ (πΆβ€˜(π΄β€˜(1st β€˜(πΉβ€˜π‘š)))) ∣ (Ξ£^β€˜(𝑗 ∈ β„• ↦ (πΏβ€˜(π‘–β€˜π‘—)))) ≀ (((voln*β€˜π‘‹)β€˜(π΄β€˜(1st β€˜(πΉβ€˜π‘š)))) +𝑒 𝑒)} = {𝑖 ∈ (πΆβ€˜(π΄β€˜(1st β€˜(πΉβ€˜π‘š)))) ∣ (Ξ£^β€˜(𝑗 ∈ β„• ↦ (πΏβ€˜(π‘–β€˜π‘—)))) ≀ (((voln*β€˜π‘‹)β€˜(π΄β€˜(1st β€˜(πΉβ€˜π‘š)))) +𝑒 (𝐸 / (2↑(1st β€˜(πΉβ€˜π‘š)))))})
20017, 70syl 17 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘š ∈ β„•) β†’ 𝐸 ∈ ℝ+)
201 2rp 12975 . . . . . . . . . . . . . . . 16 2 ∈ ℝ+
202201a1i 11 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘š ∈ β„•) β†’ 2 ∈ ℝ+)
20327nnzd 12581 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘š ∈ β„•) β†’ (1st β€˜(πΉβ€˜π‘š)) ∈ β„€)
204202, 203rpexpcld 14206 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘š ∈ β„•) β†’ (2↑(1st β€˜(πΉβ€˜π‘š))) ∈ ℝ+)
205200, 204rpdivcld 13029 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘š ∈ β„•) β†’ (𝐸 / (2↑(1st β€˜(πΉβ€˜π‘š)))) ∈ ℝ+)
206 fvex 6901 . . . . . . . . . . . . . . 15 (πΆβ€˜(π΄β€˜(1st β€˜(πΉβ€˜π‘š)))) ∈ V
207206rabex 5331 . . . . . . . . . . . . . 14 {𝑖 ∈ (πΆβ€˜(π΄β€˜(1st β€˜(πΉβ€˜π‘š)))) ∣ (Ξ£^β€˜(𝑗 ∈ β„• ↦ (πΏβ€˜(π‘–β€˜π‘—)))) ≀ (((voln*β€˜π‘‹)β€˜(π΄β€˜(1st β€˜(πΉβ€˜π‘š)))) +𝑒 (𝐸 / (2↑(1st β€˜(πΉβ€˜π‘š)))))} ∈ V
208207a1i 11 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘š ∈ β„•) β†’ {𝑖 ∈ (πΆβ€˜(π΄β€˜(1st β€˜(πΉβ€˜π‘š)))) ∣ (Ξ£^β€˜(𝑗 ∈ β„• ↦ (πΏβ€˜(π‘–β€˜π‘—)))) ≀ (((voln*β€˜π‘‹)β€˜(π΄β€˜(1st β€˜(πΉβ€˜π‘š)))) +𝑒 (𝐸 / (2↑(1st β€˜(πΉβ€˜π‘š)))))} ∈ V)
209195, 199, 205, 208fvmptd 7001 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘š ∈ β„•) β†’ ((π·β€˜(π΄β€˜(1st β€˜(πΉβ€˜π‘š))))β€˜(𝐸 / (2↑(1st β€˜(πΉβ€˜π‘š))))) = {𝑖 ∈ (πΆβ€˜(π΄β€˜(1st β€˜(πΉβ€˜π‘š)))) ∣ (Ξ£^β€˜(𝑗 ∈ β„• ↦ (πΏβ€˜(π‘–β€˜π‘—)))) ≀ (((voln*β€˜π‘‹)β€˜(π΄β€˜(1st β€˜(πΉβ€˜π‘š)))) +𝑒 (𝐸 / (2↑(1st β€˜(πΉβ€˜π‘š)))))})
210 ssrab2 4076 . . . . . . . . . . . . 13 {𝑖 ∈ (πΆβ€˜(π΄β€˜(1st β€˜(πΉβ€˜π‘š)))) ∣ (Ξ£^β€˜(𝑗 ∈ β„• ↦ (πΏβ€˜(π‘–β€˜π‘—)))) ≀ (((voln*β€˜π‘‹)β€˜(π΄β€˜(1st β€˜(πΉβ€˜π‘š)))) +𝑒 (𝐸 / (2↑(1st β€˜(πΉβ€˜π‘š)))))} βŠ† (πΆβ€˜(π΄β€˜(1st β€˜(πΉβ€˜π‘š))))
211210a1i 11 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘š ∈ β„•) β†’ {𝑖 ∈ (πΆβ€˜(π΄β€˜(1st β€˜(πΉβ€˜π‘š)))) ∣ (Ξ£^β€˜(𝑗 ∈ β„• ↦ (πΏβ€˜(π‘–β€˜π‘—)))) ≀ (((voln*β€˜π‘‹)β€˜(π΄β€˜(1st β€˜(πΉβ€˜π‘š)))) +𝑒 (𝐸 / (2↑(1st β€˜(πΉβ€˜π‘š)))))} βŠ† (πΆβ€˜(π΄β€˜(1st β€˜(πΉβ€˜π‘š)))))
212209, 211eqsstrd 4019 . . . . . . . . . . 11 ((πœ‘ ∧ π‘š ∈ β„•) β†’ ((π·β€˜(π΄β€˜(1st β€˜(πΉβ€˜π‘š))))β€˜(𝐸 / (2↑(1st β€˜(πΉβ€˜π‘š))))) βŠ† (πΆβ€˜(π΄β€˜(1st β€˜(πΉβ€˜π‘š)))))
21337anbi2d 630 . . . . . . . . . . . . . 14 (𝑛 = (1st β€˜(πΉβ€˜π‘š)) β†’ ((πœ‘ ∧ 𝑛 ∈ β„•) ↔ (πœ‘ ∧ (1st β€˜(πΉβ€˜π‘š)) ∈ β„•)))
214 2fveq3 6893 . . . . . . . . . . . . . . . 16 (𝑛 = (1st β€˜(πΉβ€˜π‘š)) β†’ (π·β€˜(π΄β€˜π‘›)) = (π·β€˜(π΄β€˜(1st β€˜(πΉβ€˜π‘š)))))
215 oveq2 7412 . . . . . . . . . . . . . . . . 17 (𝑛 = (1st β€˜(πΉβ€˜π‘š)) β†’ (2↑𝑛) = (2↑(1st β€˜(πΉβ€˜π‘š))))
216215oveq2d 7420 . . . . . . . . . . . . . . . 16 (𝑛 = (1st β€˜(πΉβ€˜π‘š)) β†’ (𝐸 / (2↑𝑛)) = (𝐸 / (2↑(1st β€˜(πΉβ€˜π‘š)))))
217214, 216fveq12d 6895 . . . . . . . . . . . . . . 15 (𝑛 = (1st β€˜(πΉβ€˜π‘š)) β†’ ((π·β€˜(π΄β€˜π‘›))β€˜(𝐸 / (2↑𝑛))) = ((π·β€˜(π΄β€˜(1st β€˜(πΉβ€˜π‘š))))β€˜(𝐸 / (2↑(1st β€˜(πΉβ€˜π‘š))))))
21839, 217eleq12d 2828 . . . . . . . . . . . . . 14 (𝑛 = (1st β€˜(πΉβ€˜π‘š)) β†’ ((πΌβ€˜π‘›) ∈ ((π·β€˜(π΄β€˜π‘›))β€˜(𝐸 / (2↑𝑛))) ↔ (πΌβ€˜(1st β€˜(πΉβ€˜π‘š))) ∈ ((π·β€˜(π΄β€˜(1st β€˜(πΉβ€˜π‘š))))β€˜(𝐸 / (2↑(1st β€˜(πΉβ€˜π‘š)))))))
219213, 218imbi12d 345 . . . . . . . . . . . . 13 (𝑛 = (1st β€˜(πΉβ€˜π‘š)) β†’ (((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (πΌβ€˜π‘›) ∈ ((π·β€˜(π΄β€˜π‘›))β€˜(𝐸 / (2↑𝑛)))) ↔ ((πœ‘ ∧ (1st β€˜(πΉβ€˜π‘š)) ∈ β„•) β†’ (πΌβ€˜(1st β€˜(πΉβ€˜π‘š))) ∈ ((π·β€˜(π΄β€˜(1st β€˜(πΉβ€˜π‘š))))β€˜(𝐸 / (2↑(1st β€˜(πΉβ€˜π‘š))))))))
22036, 219, 86vtocl 3549 . . . . . . . . . . . 12 ((πœ‘ ∧ (1st β€˜(πΉβ€˜π‘š)) ∈ β„•) β†’ (πΌβ€˜(1st β€˜(πΉβ€˜π‘š))) ∈ ((π·β€˜(π΄β€˜(1st β€˜(πΉβ€˜π‘š))))β€˜(𝐸 / (2↑(1st β€˜(πΉβ€˜π‘š))))))
22117, 27, 220syl2anc 585 . . . . . . . . . . 11 ((πœ‘ ∧ π‘š ∈ β„•) β†’ (πΌβ€˜(1st β€˜(πΉβ€˜π‘š))) ∈ ((π·β€˜(π΄β€˜(1st β€˜(πΉβ€˜π‘š))))β€˜(𝐸 / (2↑(1st β€˜(πΉβ€˜π‘š))))))
222212, 221sseldd 3982 . . . . . . . . . 10 ((πœ‘ ∧ π‘š ∈ β„•) β†’ (πΌβ€˜(1st β€˜(πΉβ€˜π‘š))) ∈ (πΆβ€˜(π΄β€˜(1st β€˜(πΉβ€˜π‘š)))))
223184, 222sseldd 3982 . . . . . . . . 9 ((πœ‘ ∧ π‘š ∈ β„•) β†’ (πΌβ€˜(1st β€˜(πΉβ€˜π‘š))) ∈ (((ℝ Γ— ℝ) ↑m 𝑋) ↑m β„•))
224 elmapfn 8855 . . . . . . . . 9 ((πΌβ€˜(1st β€˜(πΉβ€˜π‘š))) ∈ (((ℝ Γ— ℝ) ↑m 𝑋) ↑m β„•) β†’ (πΌβ€˜(1st β€˜(πΉβ€˜π‘š))) Fn β„•)
225223, 224syl 17 . . . . . . . 8 ((πœ‘ ∧ π‘š ∈ β„•) β†’ (πΌβ€˜(1st β€˜(πΉβ€˜π‘š))) Fn β„•)
226 elmapi 8839 . . . . . . . . . . 11 ((πΌβ€˜(1st β€˜(πΉβ€˜π‘š))) ∈ (((ℝ Γ— ℝ) ↑m 𝑋) ↑m β„•) β†’ (πΌβ€˜(1st β€˜(πΉβ€˜π‘š))):β„•βŸΆ((ℝ Γ— ℝ) ↑m 𝑋))
227223, 226syl 17 . . . . . . . . . 10 ((πœ‘ ∧ π‘š ∈ β„•) β†’ (πΌβ€˜(1st β€˜(πΉβ€˜π‘š))):β„•βŸΆ((ℝ Γ— ℝ) ↑m 𝑋))
228227ffvelcdmda 7082 . . . . . . . . 9 (((πœ‘ ∧ π‘š ∈ β„•) ∧ 𝑗 ∈ β„•) β†’ ((πΌβ€˜(1st β€˜(πΉβ€˜π‘š)))β€˜π‘—) ∈ ((ℝ Γ— ℝ) ↑m 𝑋))
229228ralrimiva 3147 . . . . . . . 8 ((πœ‘ ∧ π‘š ∈ β„•) β†’ βˆ€π‘— ∈ β„• ((πΌβ€˜(1st β€˜(πΉβ€˜π‘š)))β€˜π‘—) ∈ ((ℝ Γ— ℝ) ↑m 𝑋))
230225, 229jca 513 . . . . . . 7 ((πœ‘ ∧ π‘š ∈ β„•) β†’ ((πΌβ€˜(1st β€˜(πΉβ€˜π‘š))) Fn β„• ∧ βˆ€π‘— ∈ β„• ((πΌβ€˜(1st β€˜(πΉβ€˜π‘š)))β€˜π‘—) ∈ ((ℝ Γ— ℝ) ↑m 𝑋)))
231 ffnfv 7113 . . . . . . 7 ((πΌβ€˜(1st β€˜(πΉβ€˜π‘š))):β„•βŸΆ((ℝ Γ— ℝ) ↑m 𝑋) ↔ ((πΌβ€˜(1st β€˜(πΉβ€˜π‘š))) Fn β„• ∧ βˆ€π‘— ∈ β„• ((πΌβ€˜(1st β€˜(πΉβ€˜π‘š)))β€˜π‘—) ∈ ((ℝ Γ— ℝ) ↑m 𝑋)))
232230, 231sylibr 233 . . . . . 6 ((πœ‘ ∧ π‘š ∈ β„•) β†’ (πΌβ€˜(1st β€˜(πΉβ€˜π‘š))):β„•βŸΆ((ℝ Γ— ℝ) ↑m 𝑋))
233232, 29ffvelcdmd 7083 . . . . 5 ((πœ‘ ∧ π‘š ∈ β„•) β†’ ((πΌβ€˜(1st β€˜(πΉβ€˜π‘š)))β€˜(2nd β€˜(πΉβ€˜π‘š))) ∈ ((ℝ Γ— ℝ) ↑m 𝑋))
234233, 109fmptd 7109 . . . 4 (πœ‘ β†’ 𝐺:β„•βŸΆ((ℝ Γ— ℝ) ↑m 𝑋))
235 simpl 484 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ πœ‘)
23686, 82eleqtrd 2836 . . . . . . . . . 10 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (πΌβ€˜π‘›) ∈ {𝑖 ∈ (πΆβ€˜(π΄β€˜π‘›)) ∣ (Ξ£^β€˜(𝑗 ∈ β„• ↦ (πΏβ€˜(π‘–β€˜π‘—)))) ≀ (((voln*β€˜π‘‹)β€˜(π΄β€˜π‘›)) +𝑒 (𝐸 / (2↑𝑛)))})
23783, 236sselid 3979 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (πΌβ€˜π‘›) ∈ (πΆβ€˜(π΄β€˜π‘›)))
238 simp3 1139 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑛 ∈ β„• ∧ (πΌβ€˜π‘›) ∈ (πΆβ€˜(π΄β€˜π‘›))) β†’ (πΌβ€˜π‘›) ∈ (πΆβ€˜(π΄β€˜π‘›)))
239493adant3 1133 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑛 ∈ β„• ∧ (πΌβ€˜π‘›) ∈ (πΆβ€˜(π΄β€˜π‘›))) β†’ (πΆβ€˜(π΄β€˜π‘›)) = {β„Ž ∈ (((ℝ Γ— ℝ) ↑m 𝑋) ↑m β„•) ∣ (π΄β€˜π‘›) βŠ† βˆͺ 𝑗 ∈ β„• Xπ‘˜ ∈ 𝑋 (([,) ∘ (β„Žβ€˜π‘—))β€˜π‘˜)})
240238, 239eleqtrd 2836 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑛 ∈ β„• ∧ (πΌβ€˜π‘›) ∈ (πΆβ€˜(π΄β€˜π‘›))) β†’ (πΌβ€˜π‘›) ∈ {β„Ž ∈ (((ℝ Γ— ℝ) ↑m 𝑋) ↑m β„•) ∣ (π΄β€˜π‘›) βŠ† βˆͺ 𝑗 ∈ β„• Xπ‘˜ ∈ 𝑋 (([,) ∘ (β„Žβ€˜π‘—))β€˜π‘˜)})
241 fveq1 6887 . . . . . . . . . . . . . . . . 17 (β„Ž = (πΌβ€˜π‘›) β†’ (β„Žβ€˜π‘—) = ((πΌβ€˜π‘›)β€˜π‘—))
242241coeq2d 5860 . . . . . . . . . . . . . . . 16 (β„Ž = (πΌβ€˜π‘›) β†’ ([,) ∘ (β„Žβ€˜π‘—)) = ([,) ∘ ((πΌβ€˜π‘›)β€˜π‘—)))
243242fveq1d 6890 . . . . . . . . . . . . . . 15 (β„Ž = (πΌβ€˜π‘›) β†’ (([,) ∘ (β„Žβ€˜π‘—))β€˜π‘˜) = (([,) ∘ ((πΌβ€˜π‘›)β€˜π‘—))β€˜π‘˜))
244243ixpeq2dv 8903 . . . . . . . . . . . . . 14 (β„Ž = (πΌβ€˜π‘›) β†’ Xπ‘˜ ∈ 𝑋 (([,) ∘ (β„Žβ€˜π‘—))β€˜π‘˜) = Xπ‘˜ ∈ 𝑋 (([,) ∘ ((πΌβ€˜π‘›)β€˜π‘—))β€˜π‘˜))
245244iuneq2d 5025 . . . . . . . . . . . . 13 (β„Ž = (πΌβ€˜π‘›) β†’ βˆͺ 𝑗 ∈ β„• Xπ‘˜ ∈ 𝑋 (([,) ∘ (β„Žβ€˜π‘—))β€˜π‘˜) = βˆͺ 𝑗 ∈ β„• Xπ‘˜ ∈ 𝑋 (([,) ∘ ((πΌβ€˜π‘›)β€˜π‘—))β€˜π‘˜))
246245sseq2d 4013 . . . . . . . . . . . 12 (β„Ž = (πΌβ€˜π‘›) β†’ ((π΄β€˜π‘›) βŠ† βˆͺ 𝑗 ∈ β„• Xπ‘˜ ∈ 𝑋 (([,) ∘ (β„Žβ€˜π‘—))β€˜π‘˜) ↔ (π΄β€˜π‘›) βŠ† βˆͺ 𝑗 ∈ β„• Xπ‘˜ ∈ 𝑋 (([,) ∘ ((πΌβ€˜π‘›)β€˜π‘—))β€˜π‘˜)))
247246elrab 3682 . . . . . . . . . . 11 ((πΌβ€˜π‘›) ∈ {β„Ž ∈ (((ℝ Γ— ℝ) ↑m 𝑋) ↑m β„•) ∣ (π΄β€˜π‘›) βŠ† βˆͺ 𝑗 ∈ β„• Xπ‘˜ ∈ 𝑋 (([,) ∘ (β„Žβ€˜π‘—))β€˜π‘˜)} ↔ ((πΌβ€˜π‘›) ∈ (((ℝ Γ— ℝ) ↑m 𝑋) ↑m β„•) ∧ (π΄β€˜π‘›) βŠ† βˆͺ 𝑗 ∈ β„• Xπ‘˜ ∈ 𝑋 (([,) ∘ ((πΌβ€˜π‘›)β€˜π‘—))β€˜π‘˜)))
248240, 247sylib 217 . . . . . . . . . 10 ((πœ‘ ∧ 𝑛 ∈ β„• ∧ (πΌβ€˜π‘›) ∈ (πΆβ€˜(π΄β€˜π‘›))) β†’ ((πΌβ€˜π‘›) ∈ (((ℝ Γ— ℝ) ↑m 𝑋) ↑m β„•) ∧ (π΄β€˜π‘›) βŠ† βˆͺ 𝑗 ∈ β„• Xπ‘˜ ∈ 𝑋 (([,) ∘ ((πΌβ€˜π‘›)β€˜π‘—))β€˜π‘˜)))
249248simprd 497 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ β„• ∧ (πΌβ€˜π‘›) ∈ (πΆβ€˜(π΄β€˜π‘›))) β†’ (π΄β€˜π‘›) βŠ† βˆͺ 𝑗 ∈ β„• Xπ‘˜ ∈ 𝑋 (([,) ∘ ((πΌβ€˜π‘›)β€˜π‘—))β€˜π‘˜))
250235, 4, 237, 249syl3anc 1372 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (π΄β€˜π‘›) βŠ† βˆͺ 𝑗 ∈ β„• Xπ‘˜ ∈ 𝑋 (([,) ∘ ((πΌβ€˜π‘›)β€˜π‘—))β€˜π‘˜))
251 f1ofo 6837 . . . . . . . . . . . . . 14 (𝐹:ℕ–1-1-ontoβ†’(β„• Γ— β„•) β†’ 𝐹:ℕ–ontoβ†’(β„• Γ— β„•))
25220, 251syl 17 . . . . . . . . . . . . 13 (πœ‘ β†’ 𝐹:ℕ–ontoβ†’(β„• Γ— β„•))
253252ad2antrr 725 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑗 ∈ β„•) β†’ 𝐹:ℕ–ontoβ†’(β„• Γ— β„•))
254 opelxpi 5712 . . . . . . . . . . . . 13 ((𝑛 ∈ β„• ∧ 𝑗 ∈ β„•) β†’ βŸ¨π‘›, π‘—βŸ© ∈ (β„• Γ— β„•))
2554, 254sylan 581 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑗 ∈ β„•) β†’ βŸ¨π‘›, π‘—βŸ© ∈ (β„• Γ— β„•))
256 foelcdmi 6950 . . . . . . . . . . . 12 ((𝐹:ℕ–ontoβ†’(β„• Γ— β„•) ∧ βŸ¨π‘›, π‘—βŸ© ∈ (β„• Γ— β„•)) β†’ βˆƒπ‘š ∈ β„• (πΉβ€˜π‘š) = βŸ¨π‘›, π‘—βŸ©)
257253, 255, 256syl2anc 585 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑗 ∈ β„•) β†’ βˆƒπ‘š ∈ β„• (πΉβ€˜π‘š) = βŸ¨π‘›, π‘—βŸ©)
258 nfv 1918 . . . . . . . . . . . 12 β„²π‘š((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑗 ∈ β„•)
259 nfre1 3283 . . . . . . . . . . . 12 β„²π‘šβˆƒπ‘š ∈ {𝑖 ∈ β„• ∣ (1st β€˜(πΉβ€˜π‘–)) = 𝑛}Xπ‘˜ ∈ 𝑋 (([,) ∘ ((πΌβ€˜π‘›)β€˜π‘—))β€˜π‘˜) βŠ† Xπ‘˜ ∈ 𝑋 (([,) ∘ (πΊβ€˜π‘š))β€˜π‘˜)
260 simpl 484 . . . . . . . . . . . . . . . . 17 ((π‘š ∈ β„• ∧ (πΉβ€˜π‘š) = βŸ¨π‘›, π‘—βŸ©) β†’ π‘š ∈ β„•)
261 fveq2 6888 . . . . . . . . . . . . . . . . . . 19 ((πΉβ€˜π‘š) = βŸ¨π‘›, π‘—βŸ© β†’ (1st β€˜(πΉβ€˜π‘š)) = (1st β€˜βŸ¨π‘›, π‘—βŸ©))
262 op1stg 7982 . . . . . . . . . . . . . . . . . . . . 21 ((𝑛 ∈ V ∧ 𝑗 ∈ V) β†’ (1st β€˜βŸ¨π‘›, π‘—βŸ©) = 𝑛)
263262el2v 3483 . . . . . . . . . . . . . . . . . . . 20 (1st β€˜βŸ¨π‘›, π‘—βŸ©) = 𝑛
264263a1i 11 . . . . . . . . . . . . . . . . . . 19 ((πΉβ€˜π‘š) = βŸ¨π‘›, π‘—βŸ© β†’ (1st β€˜βŸ¨π‘›, π‘—βŸ©) = 𝑛)
265261, 264eqtrd 2773 . . . . . . . . . . . . . . . . . 18 ((πΉβ€˜π‘š) = βŸ¨π‘›, π‘—βŸ© β†’ (1st β€˜(πΉβ€˜π‘š)) = 𝑛)
266265adantl 483 . . . . . . . . . . . . . . . . 17 ((π‘š ∈ β„• ∧ (πΉβ€˜π‘š) = βŸ¨π‘›, π‘—βŸ©) β†’ (1st β€˜(πΉβ€˜π‘š)) = 𝑛)
267260, 266jca 513 . . . . . . . . . . . . . . . 16 ((π‘š ∈ β„• ∧ (πΉβ€˜π‘š) = βŸ¨π‘›, π‘—βŸ©) β†’ (π‘š ∈ β„• ∧ (1st β€˜(πΉβ€˜π‘š)) = 𝑛))
268 2fveq3 6893 . . . . . . . . . . . . . . . . . 18 (𝑖 = π‘š β†’ (1st β€˜(πΉβ€˜π‘–)) = (1st β€˜(πΉβ€˜π‘š)))
269268eqeq1d 2735 . . . . . . . . . . . . . . . . 17 (𝑖 = π‘š β†’ ((1st β€˜(πΉβ€˜π‘–)) = 𝑛 ↔ (1st β€˜(πΉβ€˜π‘š)) = 𝑛))
270269elrab 3682 . . . . . . . . . . . . . . . 16 (π‘š ∈ {𝑖 ∈ β„• ∣ (1st β€˜(πΉβ€˜π‘–)) = 𝑛} ↔ (π‘š ∈ β„• ∧ (1st β€˜(πΉβ€˜π‘š)) = 𝑛))
271267, 270sylibr 233 . . . . . . . . . . . . . . 15 ((π‘š ∈ β„• ∧ (πΉβ€˜π‘š) = βŸ¨π‘›, π‘—βŸ©) β†’ π‘š ∈ {𝑖 ∈ β„• ∣ (1st β€˜(πΉβ€˜π‘–)) = 𝑛})
2722713adant1 1131 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑗 ∈ β„•) ∧ π‘š ∈ β„• ∧ (πΉβ€˜π‘š) = βŸ¨π‘›, π‘—βŸ©) β†’ π‘š ∈ {𝑖 ∈ β„• ∣ (1st β€˜(πΉβ€˜π‘–)) = 𝑛})
273260, 111syl 17 . . . . . . . . . . . . . . . . . . . 20 ((π‘š ∈ β„• ∧ (πΉβ€˜π‘š) = βŸ¨π‘›, π‘—βŸ©) β†’ (πΊβ€˜π‘š) = ((πΌβ€˜(1st β€˜(πΉβ€˜π‘š)))β€˜(2nd β€˜(πΉβ€˜π‘š))))
274265fveq2d 6892 . . . . . . . . . . . . . . . . . . . . . 22 ((πΉβ€˜π‘š) = βŸ¨π‘›, π‘—βŸ© β†’ (πΌβ€˜(1st β€˜(πΉβ€˜π‘š))) = (πΌβ€˜π‘›))
275 vex 3479 . . . . . . . . . . . . . . . . . . . . . . 23 𝑛 ∈ V
276 vex 3479 . . . . . . . . . . . . . . . . . . . . . . 23 𝑗 ∈ V
277275, 276op2ndd 7981 . . . . . . . . . . . . . . . . . . . . . 22 ((πΉβ€˜π‘š) = βŸ¨π‘›, π‘—βŸ© β†’ (2nd β€˜(πΉβ€˜π‘š)) = 𝑗)
278274, 277fveq12d 6895 . . . . . . . . . . . . . . . . . . . . 21 ((πΉβ€˜π‘š) = βŸ¨π‘›, π‘—βŸ© β†’ ((πΌβ€˜(1st β€˜(πΉβ€˜π‘š)))β€˜(2nd β€˜(πΉβ€˜π‘š))) = ((πΌβ€˜π‘›)β€˜π‘—))
279278adantl 483 . . . . . . . . . . . . . . . . . . . 20 ((π‘š ∈ β„• ∧ (πΉβ€˜π‘š) = βŸ¨π‘›, π‘—βŸ©) β†’ ((πΌβ€˜(1st β€˜(πΉβ€˜π‘š)))β€˜(2nd β€˜(πΉβ€˜π‘š))) = ((πΌβ€˜π‘›)β€˜π‘—))
280273, 279eqtr2d 2774 . . . . . . . . . . . . . . . . . . 19 ((π‘š ∈ β„• ∧ (πΉβ€˜π‘š) = βŸ¨π‘›, π‘—βŸ©) β†’ ((πΌβ€˜π‘›)β€˜π‘—) = (πΊβ€˜π‘š))
281280coeq2d 5860 . . . . . . . . . . . . . . . . . 18 ((π‘š ∈ β„• ∧ (πΉβ€˜π‘š) = βŸ¨π‘›, π‘—βŸ©) β†’ ([,) ∘ ((πΌβ€˜π‘›)β€˜π‘—)) = ([,) ∘ (πΊβ€˜π‘š)))
282281fveq1d 6890 . . . . . . . . . . . . . . . . 17 ((π‘š ∈ β„• ∧ (πΉβ€˜π‘š) = βŸ¨π‘›, π‘—βŸ©) β†’ (([,) ∘ ((πΌβ€˜π‘›)β€˜π‘—))β€˜π‘˜) = (([,) ∘ (πΊβ€˜π‘š))β€˜π‘˜))
283282ixpeq2dv 8903 . . . . . . . . . . . . . . . 16 ((π‘š ∈ β„• ∧ (πΉβ€˜π‘š) = βŸ¨π‘›, π‘—βŸ©) β†’ Xπ‘˜ ∈ 𝑋 (([,) ∘ ((πΌβ€˜π‘›)β€˜π‘—))β€˜π‘˜) = Xπ‘˜ ∈ 𝑋 (([,) ∘ (πΊβ€˜π‘š))β€˜π‘˜))
284 eqimss 4039 . . . . . . . . . . . . . . . 16 (Xπ‘˜ ∈ 𝑋 (([,) ∘ ((πΌβ€˜π‘›)β€˜π‘—))β€˜π‘˜) = Xπ‘˜ ∈ 𝑋 (([,) ∘ (πΊβ€˜π‘š))β€˜π‘˜) β†’ Xπ‘˜ ∈ 𝑋 (([,) ∘ ((πΌβ€˜π‘›)β€˜π‘—))β€˜π‘˜) βŠ† Xπ‘˜ ∈ 𝑋 (([,) ∘ (πΊβ€˜π‘š))β€˜π‘˜))
285283, 284syl 17 . . . . . . . . . . . . . . 15 ((π‘š ∈ β„• ∧ (πΉβ€˜π‘š) = βŸ¨π‘›, π‘—βŸ©) β†’ Xπ‘˜ ∈ 𝑋 (([,) ∘ ((πΌβ€˜π‘›)β€˜π‘—))β€˜π‘˜) βŠ† Xπ‘˜ ∈ 𝑋 (([,) ∘ (πΊβ€˜π‘š))β€˜π‘˜))
2862853adant1 1131 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑗 ∈ β„•) ∧ π‘š ∈ β„• ∧ (πΉβ€˜π‘š) = βŸ¨π‘›, π‘—βŸ©) β†’ Xπ‘˜ ∈ 𝑋 (([,) ∘ ((πΌβ€˜π‘›)β€˜π‘—))β€˜π‘˜) βŠ† Xπ‘˜ ∈ 𝑋 (([,) ∘ (πΊβ€˜π‘š))β€˜π‘˜))
287 rspe 3247 . . . . . . . . . . . . . 14 ((π‘š ∈ {𝑖 ∈ β„• ∣ (1st β€˜(πΉβ€˜π‘–)) = 𝑛} ∧ Xπ‘˜ ∈ 𝑋 (([,) ∘ ((πΌβ€˜π‘›)β€˜π‘—))β€˜π‘˜) βŠ† Xπ‘˜ ∈ 𝑋 (([,) ∘ (πΊβ€˜π‘š))β€˜π‘˜)) β†’ βˆƒπ‘š ∈ {𝑖 ∈ β„• ∣ (1st β€˜(πΉβ€˜π‘–)) = 𝑛}Xπ‘˜ ∈ 𝑋 (([,) ∘ ((πΌβ€˜π‘›)β€˜π‘—))β€˜π‘˜) βŠ† Xπ‘˜ ∈ 𝑋 (([,) ∘ (πΊβ€˜π‘š))β€˜π‘˜))
288272, 286, 287syl2anc 585 . . . . . . . . . . . . 13 ((((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑗 ∈ β„•) ∧ π‘š ∈ β„• ∧ (πΉβ€˜π‘š) = βŸ¨π‘›, π‘—βŸ©) β†’ βˆƒπ‘š ∈ {𝑖 ∈ β„• ∣ (1st β€˜(πΉβ€˜π‘–)) = 𝑛}Xπ‘˜ ∈ 𝑋 (([,) ∘ ((πΌβ€˜π‘›)β€˜π‘—))β€˜π‘˜) βŠ† Xπ‘˜ ∈ 𝑋 (([,) ∘ (πΊβ€˜π‘š))β€˜π‘˜))
2892883exp 1120 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑗 ∈ β„•) β†’ (π‘š ∈ β„• β†’ ((πΉβ€˜π‘š) = βŸ¨π‘›, π‘—βŸ© β†’ βˆƒπ‘š ∈ {𝑖 ∈ β„• ∣ (1st β€˜(πΉβ€˜π‘–)) = 𝑛}Xπ‘˜ ∈ 𝑋 (([,) ∘ ((πΌβ€˜π‘›)β€˜π‘—))β€˜π‘˜) βŠ† Xπ‘˜ ∈ 𝑋 (([,) ∘ (πΊβ€˜π‘š))β€˜π‘˜))))
290258, 259, 289rexlimd 3264 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑗 ∈ β„•) β†’ (βˆƒπ‘š ∈ β„• (πΉβ€˜π‘š) = βŸ¨π‘›, π‘—βŸ© β†’ βˆƒπ‘š ∈ {𝑖 ∈ β„• ∣ (1st β€˜(πΉβ€˜π‘–)) = 𝑛}Xπ‘˜ ∈ 𝑋 (([,) ∘ ((πΌβ€˜π‘›)β€˜π‘—))β€˜π‘˜) βŠ† Xπ‘˜ ∈ 𝑋 (([,) ∘ (πΊβ€˜π‘š))β€˜π‘˜)))
291257, 290mpd 15 . . . . . . . . . 10 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑗 ∈ β„•) β†’ βˆƒπ‘š ∈ {𝑖 ∈ β„• ∣ (1st β€˜(πΉβ€˜π‘–)) = 𝑛}Xπ‘˜ ∈ 𝑋 (([,) ∘ ((πΌβ€˜π‘›)β€˜π‘—))β€˜π‘˜) βŠ† Xπ‘˜ ∈ 𝑋 (([,) ∘ (πΊβ€˜π‘š))β€˜π‘˜))
292291ralrimiva 3147 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ βˆ€π‘— ∈ β„• βˆƒπ‘š ∈ {𝑖 ∈ β„• ∣ (1st β€˜(πΉβ€˜π‘–)) = 𝑛}Xπ‘˜ ∈ 𝑋 (([,) ∘ ((πΌβ€˜π‘›)β€˜π‘—))β€˜π‘˜) βŠ† Xπ‘˜ ∈ 𝑋 (([,) ∘ (πΊβ€˜π‘š))β€˜π‘˜))
293 iunss2 5051 . . . . . . . . 9 (βˆ€π‘— ∈ β„• βˆƒπ‘š ∈ {𝑖 ∈ β„• ∣ (1st β€˜(πΉβ€˜π‘–)) = 𝑛}Xπ‘˜ ∈ 𝑋 (([,) ∘ ((πΌβ€˜π‘›)β€˜π‘—))β€˜π‘˜) βŠ† Xπ‘˜ ∈ 𝑋 (([,) ∘ (πΊβ€˜π‘š))β€˜π‘˜) β†’ βˆͺ 𝑗 ∈ β„• Xπ‘˜ ∈ 𝑋 (([,) ∘ ((πΌβ€˜π‘›)β€˜π‘—))β€˜π‘˜) βŠ† βˆͺ π‘š ∈ {𝑖 ∈ β„• ∣ (1st β€˜(πΉβ€˜π‘–)) = 𝑛}Xπ‘˜ ∈ 𝑋 (([,) ∘ (πΊβ€˜π‘š))β€˜π‘˜))
294292, 293syl 17 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ βˆͺ 𝑗 ∈ β„• Xπ‘˜ ∈ 𝑋 (([,) ∘ ((πΌβ€˜π‘›)β€˜π‘—))β€˜π‘˜) βŠ† βˆͺ π‘š ∈ {𝑖 ∈ β„• ∣ (1st β€˜(πΉβ€˜π‘–)) = 𝑛}Xπ‘˜ ∈ 𝑋 (([,) ∘ (πΊβ€˜π‘š))β€˜π‘˜))
295250, 294sstrd 3991 . . . . . . 7 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (π΄β€˜π‘›) βŠ† βˆͺ π‘š ∈ {𝑖 ∈ β„• ∣ (1st β€˜(πΉβ€˜π‘–)) = 𝑛}Xπ‘˜ ∈ 𝑋 (([,) ∘ (πΊβ€˜π‘š))β€˜π‘˜))
296 ssrab2 4076 . . . . . . . . 9 {𝑖 ∈ β„• ∣ (1st β€˜(πΉβ€˜π‘–)) = 𝑛} βŠ† β„•
297 iunss1 5010 . . . . . . . . 9 ({𝑖 ∈ β„• ∣ (1st β€˜(πΉβ€˜π‘–)) = 𝑛} βŠ† β„• β†’ βˆͺ π‘š ∈ {𝑖 ∈ β„• ∣ (1st β€˜(πΉβ€˜π‘–)) = 𝑛}Xπ‘˜ ∈ 𝑋 (([,) ∘ (πΊβ€˜π‘š))β€˜π‘˜) βŠ† βˆͺ π‘š ∈ β„• Xπ‘˜ ∈ 𝑋 (([,) ∘ (πΊβ€˜π‘š))β€˜π‘˜))
298296, 297ax-mp 5 . . . . . . . 8 βˆͺ π‘š ∈ {𝑖 ∈ β„• ∣ (1st β€˜(πΉβ€˜π‘–)) = 𝑛}Xπ‘˜ ∈ 𝑋 (([,) ∘ (πΊβ€˜π‘š))β€˜π‘˜) βŠ† βˆͺ π‘š ∈ β„• Xπ‘˜ ∈ 𝑋 (([,) ∘ (πΊβ€˜π‘š))β€˜π‘˜)
299298a1i 11 . . . . . . 7 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ βˆͺ π‘š ∈ {𝑖 ∈ β„• ∣ (1st β€˜(πΉβ€˜π‘–)) = 𝑛}Xπ‘˜ ∈ 𝑋 (([,) ∘ (πΊβ€˜π‘š))β€˜π‘˜) βŠ† βˆͺ π‘š ∈ β„• Xπ‘˜ ∈ 𝑋 (([,) ∘ (πΊβ€˜π‘š))β€˜π‘˜))
300295, 299sstrd 3991 . . . . . 6 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (π΄β€˜π‘›) βŠ† βˆͺ π‘š ∈ β„• Xπ‘˜ ∈ 𝑋 (([,) ∘ (πΊβ€˜π‘š))β€˜π‘˜))
301300ralrimiva 3147 . . . . 5 (πœ‘ β†’ βˆ€π‘› ∈ β„• (π΄β€˜π‘›) βŠ† βˆͺ π‘š ∈ β„• Xπ‘˜ ∈ 𝑋 (([,) ∘ (πΊβ€˜π‘š))β€˜π‘˜))
302 iunss 5047 . . . . 5 (βˆͺ 𝑛 ∈ β„• (π΄β€˜π‘›) βŠ† βˆͺ π‘š ∈ β„• Xπ‘˜ ∈ 𝑋 (([,) ∘ (πΊβ€˜π‘š))β€˜π‘˜) ↔ βˆ€π‘› ∈ β„• (π΄β€˜π‘›) βŠ† βˆͺ π‘š ∈ β„• Xπ‘˜ ∈ 𝑋 (([,) ∘ (πΊβ€˜π‘š))β€˜π‘˜))
303301, 302sylibr 233 . . . 4 (πœ‘ β†’ βˆͺ 𝑛 ∈ β„• (π΄β€˜π‘›) βŠ† βˆͺ π‘š ∈ β„• Xπ‘˜ ∈ 𝑋 (([,) ∘ (πΊβ€˜π‘š))β€˜π‘˜))
3041, 126, 19, 234, 303ovnlecvr 45209 . . 3 (πœ‘ β†’ ((voln*β€˜π‘‹)β€˜βˆͺ 𝑛 ∈ β„• (π΄β€˜π‘›)) ≀ (Ξ£^β€˜(π‘š ∈ β„• ↦ (πΏβ€˜(πΊβ€˜π‘š)))))
305112fveq2d 6892 . . . . . . 7 ((πœ‘ ∧ π‘š ∈ β„•) β†’ (πΏβ€˜(πΊβ€˜π‘š)) = (πΏβ€˜((πΌβ€˜(1st β€˜(πΉβ€˜π‘š)))β€˜(2nd β€˜(πΉβ€˜π‘š)))))
306305mpteq2dva 5247 . . . . . 6 (πœ‘ β†’ (π‘š ∈ β„• ↦ (πΏβ€˜(πΊβ€˜π‘š))) = (π‘š ∈ β„• ↦ (πΏβ€˜((πΌβ€˜(1st β€˜(πΉβ€˜π‘š)))β€˜(2nd β€˜(πΉβ€˜π‘š))))))
307306fveq2d 6892 . . . . 5 (πœ‘ β†’ (Ξ£^β€˜(π‘š ∈ β„• ↦ (πΏβ€˜(πΊβ€˜π‘š)))) = (Ξ£^β€˜(π‘š ∈ β„• ↦ (πΏβ€˜((πΌβ€˜(1st β€˜(πΉβ€˜π‘š)))β€˜(2nd β€˜(πΉβ€˜π‘š)))))))
308 nfv 1918 . . . . . 6 β„²π‘πœ‘
309 2fveq3 6893 . . . . . . . 8 (𝑝 = (πΉβ€˜π‘š) β†’ (πΌβ€˜(1st β€˜π‘)) = (πΌβ€˜(1st β€˜(πΉβ€˜π‘š))))
310 fveq2 6888 . . . . . . . 8 (𝑝 = (πΉβ€˜π‘š) β†’ (2nd β€˜π‘) = (2nd β€˜(πΉβ€˜π‘š)))
311309, 310fveq12d 6895 . . . . . . 7 (𝑝 = (πΉβ€˜π‘š) β†’ ((πΌβ€˜(1st β€˜π‘))β€˜(2nd β€˜π‘)) = ((πΌβ€˜(1st β€˜(πΉβ€˜π‘š)))β€˜(2nd β€˜(πΉβ€˜π‘š))))
312311fveq2d 6892 . . . . . 6 (𝑝 = (πΉβ€˜π‘š) β†’ (πΏβ€˜((πΌβ€˜(1st β€˜π‘))β€˜(2nd β€˜π‘))) = (πΏβ€˜((πΌβ€˜(1st β€˜(πΉβ€˜π‘š)))β€˜(2nd β€˜(πΉβ€˜π‘š)))))
313 eqidd 2734 . . . . . 6 ((πœ‘ ∧ π‘š ∈ β„•) β†’ (πΉβ€˜π‘š) = (πΉβ€˜π‘š))
314 nfv 1918 . . . . . . . 8 β„²π‘˜(πœ‘ ∧ 𝑝 ∈ (β„• Γ— β„•))
3151adantr 482 . . . . . . . 8 ((πœ‘ ∧ 𝑝 ∈ (β„• Γ— β„•)) β†’ 𝑋 ∈ Fin)
316 simpl 484 . . . . . . . . 9 ((πœ‘ ∧ 𝑝 ∈ (β„• Γ— β„•)) β†’ πœ‘)
317 xp1st 8002 . . . . . . . . . 10 (𝑝 ∈ (β„• Γ— β„•) β†’ (1st β€˜π‘) ∈ β„•)
318317adantl 483 . . . . . . . . 9 ((πœ‘ ∧ 𝑝 ∈ (β„• Γ— β„•)) β†’ (1st β€˜π‘) ∈ β„•)
319 xp2nd 8003 . . . . . . . . . 10 (𝑝 ∈ (β„• Γ— β„•) β†’ (2nd β€˜π‘) ∈ β„•)
320319adantl 483 . . . . . . . . 9 ((πœ‘ ∧ 𝑝 ∈ (β„• Γ— β„•)) β†’ (2nd β€˜π‘) ∈ β„•)
321 fvex 6901 . . . . . . . . . 10 (2nd β€˜π‘) ∈ V
322 eleq1 2822 . . . . . . . . . . . 12 (𝑗 = (2nd β€˜π‘) β†’ (𝑗 ∈ β„• ↔ (2nd β€˜π‘) ∈ β„•))
3233223anbi3d 1443 . . . . . . . . . . 11 (𝑗 = (2nd β€˜π‘) β†’ ((πœ‘ ∧ (1st β€˜π‘) ∈ β„• ∧ 𝑗 ∈ β„•) ↔ (πœ‘ ∧ (1st β€˜π‘) ∈ β„• ∧ (2nd β€˜π‘) ∈ β„•)))
324 fveq2 6888 . . . . . . . . . . . 12 (𝑗 = (2nd β€˜π‘) β†’ ((πΌβ€˜(1st β€˜π‘))β€˜π‘—) = ((πΌβ€˜(1st β€˜π‘))β€˜(2nd β€˜π‘)))
325324feq1d 6699 . . . . . . . . . . 11 (𝑗 = (2nd β€˜π‘) β†’ (((πΌβ€˜(1st β€˜π‘))β€˜π‘—):π‘‹βŸΆ(ℝ Γ— ℝ) ↔ ((πΌβ€˜(1st β€˜π‘))β€˜(2nd β€˜π‘)):π‘‹βŸΆ(ℝ Γ— ℝ)))
326323, 325imbi12d 345 . . . . . . . . . 10 (𝑗 = (2nd β€˜π‘) β†’ (((πœ‘ ∧ (1st β€˜π‘) ∈ β„• ∧ 𝑗 ∈ β„•) β†’ ((πΌβ€˜(1st β€˜π‘))β€˜π‘—):π‘‹βŸΆ(ℝ Γ— ℝ)) ↔ ((πœ‘ ∧ (1st β€˜π‘) ∈ β„• ∧ (2nd β€˜π‘) ∈ β„•) β†’ ((πΌβ€˜(1st β€˜π‘))β€˜(2nd β€˜π‘)):π‘‹βŸΆ(ℝ Γ— ℝ))))
327 fvex 6901 . . . . . . . . . . 11 (1st β€˜π‘) ∈ V
328 eleq1 2822 . . . . . . . . . . . . 13 (𝑛 = (1st β€˜π‘) β†’ (𝑛 ∈ β„• ↔ (1st β€˜π‘) ∈ β„•))
3293283anbi2d 1442 . . . . . . . . . . . 12 (𝑛 = (1st β€˜π‘) β†’ ((πœ‘ ∧ 𝑛 ∈ β„• ∧ 𝑗 ∈ β„•) ↔ (πœ‘ ∧ (1st β€˜π‘) ∈ β„• ∧ 𝑗 ∈ β„•)))
330 fveq2 6888 . . . . . . . . . . . . . 14 (𝑛 = (1st β€˜π‘) β†’ (πΌβ€˜π‘›) = (πΌβ€˜(1st β€˜π‘)))
331330fveq1d 6890 . . . . . . . . . . . . 13 (𝑛 = (1st β€˜π‘) β†’ ((πΌβ€˜π‘›)β€˜π‘—) = ((πΌβ€˜(1st β€˜π‘))β€˜π‘—))
332331feq1d 6699 . . . . . . . . . . . 12 (𝑛 = (1st β€˜π‘) β†’ (((πΌβ€˜π‘›)β€˜π‘—):π‘‹βŸΆ(ℝ Γ— ℝ) ↔ ((πΌβ€˜(1st β€˜π‘))β€˜π‘—):π‘‹βŸΆ(ℝ Γ— ℝ)))
333329, 332imbi12d 345 . . . . . . . . . . 11 (𝑛 = (1st β€˜π‘) β†’ (((πœ‘ ∧ 𝑛 ∈ β„• ∧ 𝑗 ∈ β„•) β†’ ((πΌβ€˜π‘›)β€˜π‘—):π‘‹βŸΆ(ℝ Γ— ℝ)) ↔ ((πœ‘ ∧ (1st β€˜π‘) ∈ β„• ∧ 𝑗 ∈ β„•) β†’ ((πΌβ€˜(1st β€˜π‘))β€˜π‘—):π‘‹βŸΆ(ℝ Γ— ℝ))))
334327, 333, 102vtocl 3549 . . . . . . . . . 10 ((πœ‘ ∧ (1st β€˜π‘) ∈ β„• ∧ 𝑗 ∈ β„•) β†’ ((πΌβ€˜(1st β€˜π‘))β€˜π‘—):π‘‹βŸΆ(ℝ Γ— ℝ))
335321, 326, 334vtocl 3549 . . . . . . . . 9 ((πœ‘ ∧ (1st β€˜π‘) ∈ β„• ∧ (2nd β€˜π‘) ∈ β„•) β†’ ((πΌβ€˜(1st β€˜π‘))β€˜(2nd β€˜π‘)):π‘‹βŸΆ(ℝ Γ— ℝ))
336316, 318, 320, 335syl3anc 1372 . . . . . . . 8 ((πœ‘ ∧ 𝑝 ∈ (β„• Γ— β„•)) β†’ ((πΌβ€˜(1st β€˜π‘))β€˜(2nd β€˜π‘)):π‘‹βŸΆ(ℝ Γ— ℝ))
337314, 315, 19, 336hoiprodcl2 45206 . . . . . . 7 ((πœ‘ ∧ 𝑝 ∈ (β„• Γ— β„•)) β†’ (πΏβ€˜((πΌβ€˜(1st β€˜π‘))β€˜(2nd β€˜π‘))) ∈ (0[,)+∞))
33815, 337sselid 3979 . . . . . 6 ((πœ‘ ∧ 𝑝 ∈ (β„• Γ— β„•)) β†’ (πΏβ€˜((πΌβ€˜(1st β€˜π‘))β€˜(2nd β€˜π‘))) ∈ (0[,]+∞))
339308, 12, 312, 14, 20, 313, 338sge0f1o 45033 . . . . 5 (πœ‘ β†’ (Ξ£^β€˜(𝑝 ∈ (β„• Γ— β„•) ↦ (πΏβ€˜((πΌβ€˜(1st β€˜π‘))β€˜(2nd β€˜π‘))))) = (Ξ£^β€˜(π‘š ∈ β„• ↦ (πΏβ€˜((πΌβ€˜(1st β€˜(πΉβ€˜π‘š)))β€˜(2nd β€˜(πΉβ€˜π‘š)))))))
340307, 339eqtr4d 2776 . . . 4 (πœ‘ β†’ (Ξ£^β€˜(π‘š ∈ β„• ↦ (πΏβ€˜(πΊβ€˜π‘š)))) = (Ξ£^β€˜(𝑝 ∈ (β„• Γ— β„•) ↦ (πΏβ€˜((πΌβ€˜(1st β€˜π‘))β€˜(2nd β€˜π‘))))))
341 nfv 1918 . . . . . . 7 β„²π‘—πœ‘
342275, 276op1std 7980 . . . . . . . . . 10 (𝑝 = βŸ¨π‘›, π‘—βŸ© β†’ (1st β€˜π‘) = 𝑛)
343342fveq2d 6892 . . . . . . . . 9 (𝑝 = βŸ¨π‘›, π‘—βŸ© β†’ (πΌβ€˜(1st β€˜π‘)) = (πΌβ€˜π‘›))
344275, 276op2ndd 7981 . . . . . . . . 9 (𝑝 = βŸ¨π‘›, π‘—βŸ© β†’ (2nd β€˜π‘) = 𝑗)
345343, 344fveq12d 6895 . . . . . . . 8 (𝑝 = βŸ¨π‘›, π‘—βŸ© β†’ ((πΌβ€˜(1st β€˜π‘))β€˜(2nd β€˜π‘)) = ((πΌβ€˜π‘›)β€˜π‘—))
346345fveq2d 6892 . . . . . . 7 (𝑝 = βŸ¨π‘›, π‘—βŸ© β†’ (πΏβ€˜((πΌβ€˜(1st β€˜π‘))β€˜(2nd β€˜π‘))) = (πΏβ€˜((πΌβ€˜π‘›)β€˜π‘—)))
347 nfv 1918 . . . . . . . . . 10 β„²π‘˜((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑗 ∈ β„•)
348123adantr 482 . . . . . . . . . 10 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑗 ∈ β„•) β†’ 𝑋 ∈ Fin)
34993, 101syl 17 . . . . . . . . . 10 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑗 ∈ β„•) β†’ ((πΌβ€˜π‘›)β€˜π‘—):π‘‹βŸΆ(ℝ Γ— ℝ))
350347, 348, 19, 349hoiprodcl2 45206 . . . . . . . . 9 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑗 ∈ β„•) β†’ (πΏβ€˜((πΌβ€˜π‘›)β€˜π‘—)) ∈ (0[,)+∞))
35115, 350sselid 3979 . . . . . . . 8 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑗 ∈ β„•) β†’ (πΏβ€˜((πΌβ€˜π‘›)β€˜π‘—)) ∈ (0[,]+∞))
3523513impa 1111 . . . . . . 7 ((πœ‘ ∧ 𝑛 ∈ β„• ∧ 𝑗 ∈ β„•) β†’ (πΏβ€˜((πΌβ€˜π‘›)β€˜π‘—)) ∈ (0[,]+∞))
353341, 346, 14, 14, 352sge0xp 45080 . . . . . 6 (πœ‘ β†’ (Ξ£^β€˜(𝑛 ∈ β„• ↦ (Ξ£^β€˜(𝑗 ∈ β„• ↦ (πΏβ€˜((πΌβ€˜π‘›)β€˜π‘—)))))) = (Ξ£^β€˜(𝑝 ∈ (β„• Γ— β„•) ↦ (πΏβ€˜((πΌβ€˜(1st β€˜π‘))β€˜(2nd β€˜π‘))))))
354353eqcomd 2739 . . . . 5 (πœ‘ β†’ (Ξ£^β€˜(𝑝 ∈ (β„• Γ— β„•) ↦ (πΏβ€˜((πΌβ€˜(1st β€˜π‘))β€˜(2nd β€˜π‘))))) = (Ξ£^β€˜(𝑛 ∈ β„• ↦ (Ξ£^β€˜(𝑗 ∈ β„• ↦ (πΏβ€˜((πΌβ€˜π‘›)β€˜π‘—)))))))
35513a1i 11 . . . . . . 7 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ β„• ∈ V)
356 eqid 2733 . . . . . . . 8 (𝑗 ∈ β„• ↦ (πΏβ€˜((πΌβ€˜π‘›)β€˜π‘—))) = (𝑗 ∈ β„• ↦ (πΏβ€˜((πΌβ€˜π‘›)β€˜π‘—)))
357351, 356fmptd 7109 . . . . . . 7 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (𝑗 ∈ β„• ↦ (πΏβ€˜((πΌβ€˜π‘›)β€˜π‘—))):β„•βŸΆ(0[,]+∞))
358355, 357sge0cl 45032 . . . . . 6 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (Ξ£^β€˜(𝑗 ∈ β„• ↦ (πΏβ€˜((πΌβ€˜π‘›)β€˜π‘—)))) ∈ (0[,]+∞))
359 fveq1 6887 . . . . . . . . . . . . 13 (𝑖 = (πΌβ€˜π‘›) β†’ (π‘–β€˜π‘—) = ((πΌβ€˜π‘›)β€˜π‘—))
360359fveq2d 6892 . . . . . . . . . . . 12 (𝑖 = (πΌβ€˜π‘›) β†’ (πΏβ€˜(π‘–β€˜π‘—)) = (πΏβ€˜((πΌβ€˜π‘›)β€˜π‘—)))
361360mpteq2dv 5249 . . . . . . . . . . 11 (𝑖 = (πΌβ€˜π‘›) β†’ (𝑗 ∈ β„• ↦ (πΏβ€˜(π‘–β€˜π‘—))) = (𝑗 ∈ β„• ↦ (πΏβ€˜((πΌβ€˜π‘›)β€˜π‘—))))
362361fveq2d 6892 . . . . . . . . . 10 (𝑖 = (πΌβ€˜π‘›) β†’ (Ξ£^β€˜(𝑗 ∈ β„• ↦ (πΏβ€˜(π‘–β€˜π‘—)))) = (Ξ£^β€˜(𝑗 ∈ β„• ↦ (πΏβ€˜((πΌβ€˜π‘›)β€˜π‘—)))))
363362breq1d 5157 . . . . . . . . 9 (𝑖 = (πΌβ€˜π‘›) β†’ ((Ξ£^β€˜(𝑗 ∈ β„• ↦ (πΏβ€˜(π‘–β€˜π‘—)))) ≀ (((voln*β€˜π‘‹)β€˜(π΄β€˜π‘›)) +𝑒 (𝐸 / (2↑𝑛))) ↔ (Ξ£^β€˜(𝑗 ∈ β„• ↦ (πΏβ€˜((πΌβ€˜π‘›)β€˜π‘—)))) ≀ (((voln*β€˜π‘‹)β€˜(π΄β€˜π‘›)) +𝑒 (𝐸 / (2↑𝑛)))))
364363elrab 3682 . . . . . . . 8 ((πΌβ€˜π‘›) ∈ {𝑖 ∈ (πΆβ€˜(π΄β€˜π‘›)) ∣ (Ξ£^β€˜(𝑗 ∈ β„• ↦ (πΏβ€˜(π‘–β€˜π‘—)))) ≀ (((voln*β€˜π‘‹)β€˜(π΄β€˜π‘›)) +𝑒 (𝐸 / (2↑𝑛)))} ↔ ((πΌβ€˜π‘›) ∈ (πΆβ€˜(π΄β€˜π‘›)) ∧ (Ξ£^β€˜(𝑗 ∈ β„• ↦ (πΏβ€˜((πΌβ€˜π‘›)β€˜π‘—)))) ≀ (((voln*β€˜π‘‹)β€˜(π΄β€˜π‘›)) +𝑒 (𝐸 / (2↑𝑛)))))
365236, 364sylib 217 . . . . . . 7 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ ((πΌβ€˜π‘›) ∈ (πΆβ€˜(π΄β€˜π‘›)) ∧ (Ξ£^β€˜(𝑗 ∈ β„• ↦ (πΏβ€˜((πΌβ€˜π‘›)β€˜π‘—)))) ≀ (((voln*β€˜π‘‹)β€˜(π΄β€˜π‘›)) +𝑒 (𝐸 / (2↑𝑛)))))
366365simprd 497 . . . . . 6 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (Ξ£^β€˜(𝑗 ∈ β„• ↦ (πΏβ€˜((πΌβ€˜π‘›)β€˜π‘—)))) ≀ (((voln*β€˜π‘‹)β€˜(π΄β€˜π‘›)) +𝑒 (𝐸 / (2↑𝑛))))
367118, 14, 358, 173, 366sge0lempt 45061 . . . . 5 (πœ‘ β†’ (Ξ£^β€˜(𝑛 ∈ β„• ↦ (Ξ£^β€˜(𝑗 ∈ β„• ↦ (πΏβ€˜((πΌβ€˜π‘›)β€˜π‘—)))))) ≀ (Ξ£^β€˜(𝑛 ∈ β„• ↦ (((voln*β€˜π‘‹)β€˜(π΄β€˜π‘›)) +𝑒 (𝐸 / (2↑𝑛))))))
368354, 367eqbrtrd 5169 . . . 4 (πœ‘ β†’ (Ξ£^β€˜(𝑝 ∈ (β„• Γ— β„•) ↦ (πΏβ€˜((πΌβ€˜(1st β€˜π‘))β€˜(2nd β€˜π‘))))) ≀ (Ξ£^β€˜(𝑛 ∈ β„• ↦ (((voln*β€˜π‘‹)β€˜(π΄β€˜π‘›)) +𝑒 (𝐸 / (2↑𝑛))))))
369340, 368eqbrtrd 5169 . . 3 (πœ‘ β†’ (Ξ£^β€˜(π‘š ∈ β„• ↦ (πΏβ€˜(πΊβ€˜π‘š)))) ≀ (Ξ£^β€˜(𝑛 ∈ β„• ↦ (((voln*β€˜π‘‹)β€˜(π΄β€˜π‘›)) +𝑒 (𝐸 / (2↑𝑛))))))
37011, 117, 174, 304, 369xrletrd 13137 . 2 (πœ‘ β†’ ((voln*β€˜π‘‹)β€˜βˆͺ 𝑛 ∈ β„• (π΄β€˜π‘›)) ≀ (Ξ£^β€˜(𝑛 ∈ β„• ↦ (((voln*β€˜π‘‹)β€˜(π΄β€˜π‘›)) +𝑒 (𝐸 / (2↑𝑛))))))
371118, 14, 160, 168sge0xadd 45086 . . 3 (πœ‘ β†’ (Ξ£^β€˜(𝑛 ∈ β„• ↦ (((voln*β€˜π‘‹)β€˜(π΄β€˜π‘›)) +𝑒 (𝐸 / (2↑𝑛))))) = ((Ξ£^β€˜(𝑛 ∈ β„• ↦ ((voln*β€˜π‘‹)β€˜(π΄β€˜π‘›)))) +𝑒 (Ξ£^β€˜(𝑛 ∈ β„• ↦ (𝐸 / (2↑𝑛))))))
372119a1i 11 . . . . . 6 (πœ‘ β†’ 0 ∈ ℝ*)
373121a1i 11 . . . . . 6 (πœ‘ β†’ +∞ ∈ ℝ*)
374145rexrd 11260 . . . . . 6 (πœ‘ β†’ 𝐸 ∈ ℝ*)
37570rpge0d 13016 . . . . . 6 (πœ‘ β†’ 0 ≀ 𝐸)
376145ltpnfd 13097 . . . . . 6 (πœ‘ β†’ 𝐸 < +∞)
377372, 373, 374, 375, 376elicod 13370 . . . . 5 (πœ‘ β†’ 𝐸 ∈ (0[,)+∞))
378377sge0ad2en 45082 . . . 4 (πœ‘ β†’ (Ξ£^β€˜(𝑛 ∈ β„• ↦ (𝐸 / (2↑𝑛)))) = 𝐸)
379378oveq2d 7420 . . 3 (πœ‘ β†’ ((Ξ£^β€˜(𝑛 ∈ β„• ↦ ((voln*β€˜π‘‹)β€˜(π΄β€˜π‘›)))) +𝑒 (Ξ£^β€˜(𝑛 ∈ β„• ↦ (𝐸 / (2↑𝑛))))) = ((Ξ£^β€˜(𝑛 ∈ β„• ↦ ((voln*β€˜π‘‹)β€˜(π΄β€˜π‘›)))) +𝑒 𝐸))
380371, 379eqtrd 2773 . 2 (πœ‘ β†’ (Ξ£^β€˜(𝑛 ∈ β„• ↦ (((voln*β€˜π‘‹)β€˜(π΄β€˜π‘›)) +𝑒 (𝐸 / (2↑𝑛))))) = ((Ξ£^β€˜(𝑛 ∈ β„• ↦ ((voln*β€˜π‘‹)β€˜(π΄β€˜π‘›)))) +𝑒 𝐸))
381370, 380breqtrd 5173 1 (πœ‘ β†’ ((voln*β€˜π‘‹)β€˜βˆͺ 𝑛 ∈ β„• (π΄β€˜π‘›)) ≀ ((Ξ£^β€˜(𝑛 ∈ β„• ↦ ((voln*β€˜π‘‹)β€˜(π΄β€˜π‘›)))) +𝑒 𝐸))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ∧ wa 397   ∧ w3a 1088   = wceq 1542   ∈ wcel 2107   β‰  wne 2941  βˆ€wral 3062  βˆƒwrex 3071  {crab 3433  Vcvv 3475   βŠ† wss 3947  βˆ…c0 4321  ifcif 4527  π’« cpw 4601  βŸ¨cop 4633  βˆͺ ciun 4996   class class class wbr 5147   ↦ cmpt 5230   Γ— cxp 5673   ∘ ccom 5679   Fn wfn 6535  βŸΆwf 6536  β€“ontoβ†’wfo 6538  β€“1-1-ontoβ†’wf1o 6539  β€˜cfv 6540  (class class class)co 7404  1st c1st 7968  2nd c2nd 7969   ↑m cmap 8816  Xcixp 8887  Fincfn 8935  infcinf 9432  β„cr 11105  0cc0 11106  +∞cpnf 11241  β„*cxr 11243   < clt 11244   ≀ cle 11245   / cdiv 11867  β„•cn 12208  2c2 12263  β„+crp 12970   +𝑒 cxad 13086  [,)cico 13322  [,]cicc 13323  β†‘cexp 14023  βˆcprod 15845  volcvol 24962  Ξ£^csumge0 45013  voln*covoln 45187
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7720  ax-inf2 9632  ax-ac2 10454  ax-cnex 11162  ax-resscn 11163  ax-1cn 11164  ax-icn 11165  ax-addcl 11166  ax-addrcl 11167  ax-mulcl 11168  ax-mulrcl 11169  ax-mulcom 11170  ax-addass 11171  ax-mulass 11172  ax-distr 11173  ax-i2m1 11174  ax-1ne0 11175  ax-1rid 11176  ax-rnegex 11177  ax-rrecex 11178  ax-cnre 11179  ax-pre-lttri 11180  ax-pre-lttrn 11181  ax-pre-ltadd 11182  ax-pre-mulgt0 11183  ax-pre-sup 11184  ax-addf 11185  ax-mulf 11186
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-tp 4632  df-op 4634  df-uni 4908  df-int 4950  df-iun 4998  df-disj 5113  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-se 5631  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6297  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-isom 6549  df-riota 7360  df-ov 7407  df-oprab 7408  df-mpo 7409  df-of 7665  df-om 7851  df-1st 7970  df-2nd 7971  df-tpos 8206  df-frecs 8261  df-wrecs 8292  df-recs 8366  df-rdg 8405  df-1o 8461  df-2o 8462  df-er 8699  df-map 8818  df-pm 8819  df-ixp 8888  df-en 8936  df-dom 8937  df-sdom 8938  df-fin 8939  df-fi 9402  df-sup 9433  df-inf 9434  df-oi 9501  df-dju 9892  df-card 9930  df-acn 9933  df-ac 10107  df-pnf 11246  df-mnf 11247  df-xr 11248  df-ltxr 11249  df-le 11250  df-sub 11442  df-neg 11443  df-div 11868  df-nn 12209  df-2 12271  df-3 12272  df-4 12273  df-5 12274  df-6 12275  df-7 12276  df-8 12277  df-9 12278  df-n0 12469  df-z 12555  df-dec 12674  df-uz 12819  df-q 12929  df-rp 12971  df-xneg 13088  df-xadd 13089  df-xmul 13090  df-ioo 13324  df-ico 13326  df-icc 13327  df-fz 13481  df-fzo 13624  df-fl 13753  df-seq 13963  df-exp 14024  df-hash 14287  df-cj 15042  df-re 15043  df-im 15044  df-sqrt 15178  df-abs 15179  df-clim 15428  df-rlim 15429  df-sum 15629  df-prod 15846  df-struct 17076  df-sets 17093  df-slot 17111  df-ndx 17123  df-base 17141  df-ress 17170  df-plusg 17206  df-mulr 17207  df-starv 17208  df-tset 17212  df-ple 17213  df-ds 17215  df-unif 17216  df-rest 17364  df-0g 17383  df-topgen 17385  df-mgm 18557  df-sgrp 18606  df-mnd 18622  df-grp 18818  df-minusg 18819  df-subg 18997  df-cmn 19643  df-abl 19644  df-mgp 19980  df-ur 19997  df-ring 20049  df-cring 20050  df-oppr 20139  df-dvdsr 20160  df-unit 20161  df-invr 20191  df-dvr 20204  df-drng 20306  df-psmet 20921  df-xmet 20922  df-met 20923  df-bl 20924  df-mopn 20925  df-cnfld 20930  df-top 22378  df-topon 22395  df-bases 22431  df-cmp 22873  df-ovol 24963  df-vol 24964  df-sumge0 45014  df-ovoln 45188
This theorem is referenced by:  ovnsubaddlem2  45222
  Copyright terms: Public domain W3C validator