Metamath Proof Explorer


Theorem ovnsubadd

Description: ( voln*X ) is subadditive. Proposition 115D (a)(iv) of Fremlin1 p. 31 . (Contributed by Glauco Siliprandi, 11-Oct-2020)

Ref Expression
Hypotheses ovnsubadd.1 ( 𝜑𝑋 ∈ Fin )
ovnsubadd.2 ( 𝜑𝐴 : ℕ ⟶ 𝒫 ( ℝ ↑m 𝑋 ) )
Assertion ovnsubadd ( 𝜑 → ( ( voln* ‘ 𝑋 ) ‘ 𝑛 ∈ ℕ ( 𝐴𝑛 ) ) ≤ ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴𝑛 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 ovnsubadd.1 ( 𝜑𝑋 ∈ Fin )
2 ovnsubadd.2 ( 𝜑𝐴 : ℕ ⟶ 𝒫 ( ℝ ↑m 𝑋 ) )
3 fveq2 ( 𝑋 = ∅ → ( voln* ‘ 𝑋 ) = ( voln* ‘ ∅ ) )
4 3 fveq1d ( 𝑋 = ∅ → ( ( voln* ‘ 𝑋 ) ‘ 𝑛 ∈ ℕ ( 𝐴𝑛 ) ) = ( ( voln* ‘ ∅ ) ‘ 𝑛 ∈ ℕ ( 𝐴𝑛 ) ) )
5 4 adantl ( ( 𝜑𝑋 = ∅ ) → ( ( voln* ‘ 𝑋 ) ‘ 𝑛 ∈ ℕ ( 𝐴𝑛 ) ) = ( ( voln* ‘ ∅ ) ‘ 𝑛 ∈ ℕ ( 𝐴𝑛 ) ) )
6 2 adantr ( ( 𝜑𝑛 ∈ ℕ ) → 𝐴 : ℕ ⟶ 𝒫 ( ℝ ↑m 𝑋 ) )
7 simpr ( ( 𝜑𝑛 ∈ ℕ ) → 𝑛 ∈ ℕ )
8 6 7 ffvelrnd ( ( 𝜑𝑛 ∈ ℕ ) → ( 𝐴𝑛 ) ∈ 𝒫 ( ℝ ↑m 𝑋 ) )
9 elpwi ( ( 𝐴𝑛 ) ∈ 𝒫 ( ℝ ↑m 𝑋 ) → ( 𝐴𝑛 ) ⊆ ( ℝ ↑m 𝑋 ) )
10 8 9 syl ( ( 𝜑𝑛 ∈ ℕ ) → ( 𝐴𝑛 ) ⊆ ( ℝ ↑m 𝑋 ) )
11 10 ralrimiva ( 𝜑 → ∀ 𝑛 ∈ ℕ ( 𝐴𝑛 ) ⊆ ( ℝ ↑m 𝑋 ) )
12 iunss ( 𝑛 ∈ ℕ ( 𝐴𝑛 ) ⊆ ( ℝ ↑m 𝑋 ) ↔ ∀ 𝑛 ∈ ℕ ( 𝐴𝑛 ) ⊆ ( ℝ ↑m 𝑋 ) )
13 11 12 sylibr ( 𝜑 𝑛 ∈ ℕ ( 𝐴𝑛 ) ⊆ ( ℝ ↑m 𝑋 ) )
14 13 adantr ( ( 𝜑𝑋 = ∅ ) → 𝑛 ∈ ℕ ( 𝐴𝑛 ) ⊆ ( ℝ ↑m 𝑋 ) )
15 oveq2 ( 𝑋 = ∅ → ( ℝ ↑m 𝑋 ) = ( ℝ ↑m ∅ ) )
16 15 adantl ( ( 𝜑𝑋 = ∅ ) → ( ℝ ↑m 𝑋 ) = ( ℝ ↑m ∅ ) )
17 14 16 sseqtrd ( ( 𝜑𝑋 = ∅ ) → 𝑛 ∈ ℕ ( 𝐴𝑛 ) ⊆ ( ℝ ↑m ∅ ) )
18 17 ovn0val ( ( 𝜑𝑋 = ∅ ) → ( ( voln* ‘ ∅ ) ‘ 𝑛 ∈ ℕ ( 𝐴𝑛 ) ) = 0 )
19 5 18 eqtrd ( ( 𝜑𝑋 = ∅ ) → ( ( voln* ‘ 𝑋 ) ‘ 𝑛 ∈ ℕ ( 𝐴𝑛 ) ) = 0 )
20 nnex ℕ ∈ V
21 20 a1i ( 𝜑 → ℕ ∈ V )
22 1 adantr ( ( 𝜑𝑛 ∈ ℕ ) → 𝑋 ∈ Fin )
23 22 10 ovncl ( ( 𝜑𝑛 ∈ ℕ ) → ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴𝑛 ) ) ∈ ( 0 [,] +∞ ) )
24 eqid ( 𝑛 ∈ ℕ ↦ ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴𝑛 ) ) ) = ( 𝑛 ∈ ℕ ↦ ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴𝑛 ) ) )
25 23 24 fmptd ( 𝜑 → ( 𝑛 ∈ ℕ ↦ ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴𝑛 ) ) ) : ℕ ⟶ ( 0 [,] +∞ ) )
26 21 25 sge0ge0 ( 𝜑 → 0 ≤ ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴𝑛 ) ) ) ) )
27 26 adantr ( ( 𝜑𝑋 = ∅ ) → 0 ≤ ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴𝑛 ) ) ) ) )
28 19 27 eqbrtrd ( ( 𝜑𝑋 = ∅ ) → ( ( voln* ‘ 𝑋 ) ‘ 𝑛 ∈ ℕ ( 𝐴𝑛 ) ) ≤ ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴𝑛 ) ) ) ) )
29 1 13 ovnxrcl ( 𝜑 → ( ( voln* ‘ 𝑋 ) ‘ 𝑛 ∈ ℕ ( 𝐴𝑛 ) ) ∈ ℝ* )
30 29 adantr ( ( 𝜑 ∧ ¬ 𝑋 = ∅ ) → ( ( voln* ‘ 𝑋 ) ‘ 𝑛 ∈ ℕ ( 𝐴𝑛 ) ) ∈ ℝ* )
31 21 25 sge0xrcl ( 𝜑 → ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴𝑛 ) ) ) ) ∈ ℝ* )
32 31 adantr ( ( 𝜑 ∧ ¬ 𝑋 = ∅ ) → ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴𝑛 ) ) ) ) ∈ ℝ* )
33 1 ad2antrr ( ( ( 𝜑 ∧ ¬ 𝑋 = ∅ ) ∧ 𝑦 ∈ ℝ+ ) → 𝑋 ∈ Fin )
34 neqne ( ¬ 𝑋 = ∅ → 𝑋 ≠ ∅ )
35 34 ad2antlr ( ( ( 𝜑 ∧ ¬ 𝑋 = ∅ ) ∧ 𝑦 ∈ ℝ+ ) → 𝑋 ≠ ∅ )
36 2 ad2antrr ( ( ( 𝜑 ∧ ¬ 𝑋 = ∅ ) ∧ 𝑦 ∈ ℝ+ ) → 𝐴 : ℕ ⟶ 𝒫 ( ℝ ↑m 𝑋 ) )
37 simpr ( ( ( 𝜑 ∧ ¬ 𝑋 = ∅ ) ∧ 𝑦 ∈ ℝ+ ) → 𝑦 ∈ ℝ+ )
38 eqid ( 𝑎 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↦ { 𝑧 ∈ ℝ* ∣ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ( 𝑎 𝑗 ∈ ℕ X 𝑘𝑋 ( ( [,) ∘ ( 𝑖𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖𝑗 ) ) ‘ 𝑘 ) ) ) ) ) } ) = ( 𝑎 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↦ { 𝑧 ∈ ℝ* ∣ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ( 𝑎 𝑗 ∈ ℕ X 𝑘𝑋 ( ( [,) ∘ ( 𝑖𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖𝑗 ) ) ‘ 𝑘 ) ) ) ) ) } )
39 sseq1 ( 𝑏 = 𝑎 → ( 𝑏 𝑗 ∈ ℕ X 𝑘𝑋 ( ( [,) ∘ ( 𝑙𝑗 ) ) ‘ 𝑘 ) ↔ 𝑎 𝑗 ∈ ℕ X 𝑘𝑋 ( ( [,) ∘ ( 𝑙𝑗 ) ) ‘ 𝑘 ) ) )
40 39 rabbidv ( 𝑏 = 𝑎 → { 𝑙 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∣ 𝑏 𝑗 ∈ ℕ X 𝑘𝑋 ( ( [,) ∘ ( 𝑙𝑗 ) ) ‘ 𝑘 ) } = { 𝑙 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∣ 𝑎 𝑗 ∈ ℕ X 𝑘𝑋 ( ( [,) ∘ ( 𝑙𝑗 ) ) ‘ 𝑘 ) } )
41 40 cbvmptv ( 𝑏 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↦ { 𝑙 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∣ 𝑏 𝑗 ∈ ℕ X 𝑘𝑋 ( ( [,) ∘ ( 𝑙𝑗 ) ) ‘ 𝑘 ) } ) = ( 𝑎 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↦ { 𝑙 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∣ 𝑎 𝑗 ∈ ℕ X 𝑘𝑋 ( ( [,) ∘ ( 𝑙𝑗 ) ) ‘ 𝑘 ) } )
42 eqid ( ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑘𝑋 ( vol ‘ ( ( [,) ∘ ) ‘ 𝑘 ) ) ) = ( ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑘𝑋 ( vol ‘ ( ( [,) ∘ ) ‘ 𝑘 ) ) )
43 fveq2 ( 𝑜 = 𝑗 → ( 𝑙𝑜 ) = ( 𝑙𝑗 ) )
44 43 coeq2d ( 𝑜 = 𝑗 → ( [,) ∘ ( 𝑙𝑜 ) ) = ( [,) ∘ ( 𝑙𝑗 ) ) )
45 44 fveq1d ( 𝑜 = 𝑗 → ( ( [,) ∘ ( 𝑙𝑜 ) ) ‘ 𝑑 ) = ( ( [,) ∘ ( 𝑙𝑗 ) ) ‘ 𝑑 ) )
46 45 ixpeq2dv ( 𝑜 = 𝑗X 𝑑𝑋 ( ( [,) ∘ ( 𝑙𝑜 ) ) ‘ 𝑑 ) = X 𝑑𝑋 ( ( [,) ∘ ( 𝑙𝑗 ) ) ‘ 𝑑 ) )
47 fveq2 ( 𝑑 = 𝑘 → ( ( [,) ∘ ( 𝑙𝑗 ) ) ‘ 𝑑 ) = ( ( [,) ∘ ( 𝑙𝑗 ) ) ‘ 𝑘 ) )
48 47 cbvixpv X 𝑑𝑋 ( ( [,) ∘ ( 𝑙𝑗 ) ) ‘ 𝑑 ) = X 𝑘𝑋 ( ( [,) ∘ ( 𝑙𝑗 ) ) ‘ 𝑘 )
49 46 48 eqtrdi ( 𝑜 = 𝑗X 𝑑𝑋 ( ( [,) ∘ ( 𝑙𝑜 ) ) ‘ 𝑑 ) = X 𝑘𝑋 ( ( [,) ∘ ( 𝑙𝑗 ) ) ‘ 𝑘 ) )
50 49 cbviunv 𝑜 ∈ ℕ X 𝑑𝑋 ( ( [,) ∘ ( 𝑙𝑜 ) ) ‘ 𝑑 ) = 𝑗 ∈ ℕ X 𝑘𝑋 ( ( [,) ∘ ( 𝑙𝑗 ) ) ‘ 𝑘 )
51 50 sseq2i ( 𝑏 𝑜 ∈ ℕ X 𝑑𝑋 ( ( [,) ∘ ( 𝑙𝑜 ) ) ‘ 𝑑 ) ↔ 𝑏 𝑗 ∈ ℕ X 𝑘𝑋 ( ( [,) ∘ ( 𝑙𝑗 ) ) ‘ 𝑘 ) )
52 51 rabbii { 𝑙 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∣ 𝑏 𝑜 ∈ ℕ X 𝑑𝑋 ( ( [,) ∘ ( 𝑙𝑜 ) ) ‘ 𝑑 ) } = { 𝑙 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∣ 𝑏 𝑗 ∈ ℕ X 𝑘𝑋 ( ( [,) ∘ ( 𝑙𝑗 ) ) ‘ 𝑘 ) }
53 52 mpteq2i ( 𝑏 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↦ { 𝑙 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∣ 𝑏 𝑜 ∈ ℕ X 𝑑𝑋 ( ( [,) ∘ ( 𝑙𝑜 ) ) ‘ 𝑑 ) } ) = ( 𝑏 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↦ { 𝑙 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∣ 𝑏 𝑗 ∈ ℕ X 𝑘𝑋 ( ( [,) ∘ ( 𝑙𝑗 ) ) ‘ 𝑘 ) } )
54 53 fveq1i ( ( 𝑏 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↦ { 𝑙 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∣ 𝑏 𝑜 ∈ ℕ X 𝑑𝑋 ( ( [,) ∘ ( 𝑙𝑜 ) ) ‘ 𝑑 ) } ) ‘ 𝑑 ) = ( ( 𝑏 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↦ { 𝑙 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∣ 𝑏 𝑗 ∈ ℕ X 𝑘𝑋 ( ( [,) ∘ ( 𝑙𝑗 ) ) ‘ 𝑘 ) } ) ‘ 𝑑 )
55 fveq2 ( 𝑑 = 𝑎 → ( ( 𝑏 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↦ { 𝑙 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∣ 𝑏 𝑗 ∈ ℕ X 𝑘𝑋 ( ( [,) ∘ ( 𝑙𝑗 ) ) ‘ 𝑘 ) } ) ‘ 𝑑 ) = ( ( 𝑏 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↦ { 𝑙 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∣ 𝑏 𝑗 ∈ ℕ X 𝑘𝑋 ( ( [,) ∘ ( 𝑙𝑗 ) ) ‘ 𝑘 ) } ) ‘ 𝑎 ) )
56 54 55 syl5eq ( 𝑑 = 𝑎 → ( ( 𝑏 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↦ { 𝑙 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∣ 𝑏 𝑜 ∈ ℕ X 𝑑𝑋 ( ( [,) ∘ ( 𝑙𝑜 ) ) ‘ 𝑑 ) } ) ‘ 𝑑 ) = ( ( 𝑏 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↦ { 𝑙 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∣ 𝑏 𝑗 ∈ ℕ X 𝑘𝑋 ( ( [,) ∘ ( 𝑙𝑗 ) ) ‘ 𝑘 ) } ) ‘ 𝑎 ) )
57 56 eleq2d ( 𝑑 = 𝑎 → ( 𝑚 ∈ ( ( 𝑏 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↦ { 𝑙 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∣ 𝑏 𝑜 ∈ ℕ X 𝑑𝑋 ( ( [,) ∘ ( 𝑙𝑜 ) ) ‘ 𝑑 ) } ) ‘ 𝑑 ) ↔ 𝑚 ∈ ( ( 𝑏 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↦ { 𝑙 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∣ 𝑏 𝑗 ∈ ℕ X 𝑘𝑋 ( ( [,) ∘ ( 𝑙𝑗 ) ) ‘ 𝑘 ) } ) ‘ 𝑎 ) ) )
58 2fveq3 ( 𝑑 = 𝑘 → ( vol ‘ ( ( [,) ∘ ) ‘ 𝑑 ) ) = ( vol ‘ ( ( [,) ∘ ) ‘ 𝑘 ) ) )
59 58 cbvprodv 𝑑𝑋 ( vol ‘ ( ( [,) ∘ ) ‘ 𝑑 ) ) = ∏ 𝑘𝑋 ( vol ‘ ( ( [,) ∘ ) ‘ 𝑘 ) )
60 59 mpteq2i ( ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑑𝑋 ( vol ‘ ( ( [,) ∘ ) ‘ 𝑑 ) ) ) = ( ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑘𝑋 ( vol ‘ ( ( [,) ∘ ) ‘ 𝑘 ) ) )
61 60 a1i ( 𝑜 = 𝑗 → ( ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑑𝑋 ( vol ‘ ( ( [,) ∘ ) ‘ 𝑑 ) ) ) = ( ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑘𝑋 ( vol ‘ ( ( [,) ∘ ) ‘ 𝑘 ) ) ) )
62 fveq2 ( 𝑜 = 𝑗 → ( 𝑚𝑜 ) = ( 𝑚𝑗 ) )
63 61 62 fveq12d ( 𝑜 = 𝑗 → ( ( ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑑𝑋 ( vol ‘ ( ( [,) ∘ ) ‘ 𝑑 ) ) ) ‘ ( 𝑚𝑜 ) ) = ( ( ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑘𝑋 ( vol ‘ ( ( [,) ∘ ) ‘ 𝑘 ) ) ) ‘ ( 𝑚𝑗 ) ) )
64 63 cbvmptv ( 𝑜 ∈ ℕ ↦ ( ( ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑑𝑋 ( vol ‘ ( ( [,) ∘ ) ‘ 𝑑 ) ) ) ‘ ( 𝑚𝑜 ) ) ) = ( 𝑗 ∈ ℕ ↦ ( ( ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑘𝑋 ( vol ‘ ( ( [,) ∘ ) ‘ 𝑘 ) ) ) ‘ ( 𝑚𝑗 ) ) )
65 64 fveq2i ( Σ^ ‘ ( 𝑜 ∈ ℕ ↦ ( ( ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑑𝑋 ( vol ‘ ( ( [,) ∘ ) ‘ 𝑑 ) ) ) ‘ ( 𝑚𝑜 ) ) ) ) = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑘𝑋 ( vol ‘ ( ( [,) ∘ ) ‘ 𝑘 ) ) ) ‘ ( 𝑚𝑗 ) ) ) )
66 65 a1i ( 𝑑 = 𝑎 → ( Σ^ ‘ ( 𝑜 ∈ ℕ ↦ ( ( ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑑𝑋 ( vol ‘ ( ( [,) ∘ ) ‘ 𝑑 ) ) ) ‘ ( 𝑚𝑜 ) ) ) ) = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑘𝑋 ( vol ‘ ( ( [,) ∘ ) ‘ 𝑘 ) ) ) ‘ ( 𝑚𝑗 ) ) ) ) )
67 fveq2 ( 𝑑 = 𝑎 → ( ( voln* ‘ 𝑋 ) ‘ 𝑑 ) = ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) )
68 67 oveq1d ( 𝑑 = 𝑎 → ( ( ( voln* ‘ 𝑋 ) ‘ 𝑑 ) +𝑒 𝑓 ) = ( ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) +𝑒 𝑓 ) )
69 66 68 breq12d ( 𝑑 = 𝑎 → ( ( Σ^ ‘ ( 𝑜 ∈ ℕ ↦ ( ( ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑑𝑋 ( vol ‘ ( ( [,) ∘ ) ‘ 𝑑 ) ) ) ‘ ( 𝑚𝑜 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑑 ) +𝑒 𝑓 ) ↔ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑘𝑋 ( vol ‘ ( ( [,) ∘ ) ‘ 𝑘 ) ) ) ‘ ( 𝑚𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) +𝑒 𝑓 ) ) )
70 57 69 anbi12d ( 𝑑 = 𝑎 → ( ( 𝑚 ∈ ( ( 𝑏 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↦ { 𝑙 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∣ 𝑏 𝑜 ∈ ℕ X 𝑑𝑋 ( ( [,) ∘ ( 𝑙𝑜 ) ) ‘ 𝑑 ) } ) ‘ 𝑑 ) ∧ ( Σ^ ‘ ( 𝑜 ∈ ℕ ↦ ( ( ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑑𝑋 ( vol ‘ ( ( [,) ∘ ) ‘ 𝑑 ) ) ) ‘ ( 𝑚𝑜 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑑 ) +𝑒 𝑓 ) ) ↔ ( 𝑚 ∈ ( ( 𝑏 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↦ { 𝑙 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∣ 𝑏 𝑗 ∈ ℕ X 𝑘𝑋 ( ( [,) ∘ ( 𝑙𝑗 ) ) ‘ 𝑘 ) } ) ‘ 𝑎 ) ∧ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑘𝑋 ( vol ‘ ( ( [,) ∘ ) ‘ 𝑘 ) ) ) ‘ ( 𝑚𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) +𝑒 𝑓 ) ) ) )
71 70 rabbidva2 ( 𝑑 = 𝑎 → { 𝑚 ∈ ( ( 𝑏 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↦ { 𝑙 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∣ 𝑏 𝑜 ∈ ℕ X 𝑑𝑋 ( ( [,) ∘ ( 𝑙𝑜 ) ) ‘ 𝑑 ) } ) ‘ 𝑑 ) ∣ ( Σ^ ‘ ( 𝑜 ∈ ℕ ↦ ( ( ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑑𝑋 ( vol ‘ ( ( [,) ∘ ) ‘ 𝑑 ) ) ) ‘ ( 𝑚𝑜 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑑 ) +𝑒 𝑓 ) } = { 𝑚 ∈ ( ( 𝑏 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↦ { 𝑙 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∣ 𝑏 𝑗 ∈ ℕ X 𝑘𝑋 ( ( [,) ∘ ( 𝑙𝑗 ) ) ‘ 𝑘 ) } ) ‘ 𝑎 ) ∣ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑘𝑋 ( vol ‘ ( ( [,) ∘ ) ‘ 𝑘 ) ) ) ‘ ( 𝑚𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) +𝑒 𝑓 ) } )
72 fveq1 ( 𝑚 = 𝑖 → ( 𝑚𝑗 ) = ( 𝑖𝑗 ) )
73 72 fveq2d ( 𝑚 = 𝑖 → ( ( ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑘𝑋 ( vol ‘ ( ( [,) ∘ ) ‘ 𝑘 ) ) ) ‘ ( 𝑚𝑗 ) ) = ( ( ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑘𝑋 ( vol ‘ ( ( [,) ∘ ) ‘ 𝑘 ) ) ) ‘ ( 𝑖𝑗 ) ) )
74 73 mpteq2dv ( 𝑚 = 𝑖 → ( 𝑗 ∈ ℕ ↦ ( ( ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑘𝑋 ( vol ‘ ( ( [,) ∘ ) ‘ 𝑘 ) ) ) ‘ ( 𝑚𝑗 ) ) ) = ( 𝑗 ∈ ℕ ↦ ( ( ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑘𝑋 ( vol ‘ ( ( [,) ∘ ) ‘ 𝑘 ) ) ) ‘ ( 𝑖𝑗 ) ) ) )
75 74 fveq2d ( 𝑚 = 𝑖 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑘𝑋 ( vol ‘ ( ( [,) ∘ ) ‘ 𝑘 ) ) ) ‘ ( 𝑚𝑗 ) ) ) ) = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑘𝑋 ( vol ‘ ( ( [,) ∘ ) ‘ 𝑘 ) ) ) ‘ ( 𝑖𝑗 ) ) ) ) )
76 75 breq1d ( 𝑚 = 𝑖 → ( ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑘𝑋 ( vol ‘ ( ( [,) ∘ ) ‘ 𝑘 ) ) ) ‘ ( 𝑚𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) +𝑒 𝑓 ) ↔ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑘𝑋 ( vol ‘ ( ( [,) ∘ ) ‘ 𝑘 ) ) ) ‘ ( 𝑖𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) +𝑒 𝑓 ) ) )
77 76 cbvrabv { 𝑚 ∈ ( ( 𝑏 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↦ { 𝑙 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∣ 𝑏 𝑗 ∈ ℕ X 𝑘𝑋 ( ( [,) ∘ ( 𝑙𝑗 ) ) ‘ 𝑘 ) } ) ‘ 𝑎 ) ∣ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑘𝑋 ( vol ‘ ( ( [,) ∘ ) ‘ 𝑘 ) ) ) ‘ ( 𝑚𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) +𝑒 𝑓 ) } = { 𝑖 ∈ ( ( 𝑏 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↦ { 𝑙 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∣ 𝑏 𝑗 ∈ ℕ X 𝑘𝑋 ( ( [,) ∘ ( 𝑙𝑗 ) ) ‘ 𝑘 ) } ) ‘ 𝑎 ) ∣ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑘𝑋 ( vol ‘ ( ( [,) ∘ ) ‘ 𝑘 ) ) ) ‘ ( 𝑖𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) +𝑒 𝑓 ) }
78 71 77 eqtrdi ( 𝑑 = 𝑎 → { 𝑚 ∈ ( ( 𝑏 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↦ { 𝑙 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∣ 𝑏 𝑜 ∈ ℕ X 𝑑𝑋 ( ( [,) ∘ ( 𝑙𝑜 ) ) ‘ 𝑑 ) } ) ‘ 𝑑 ) ∣ ( Σ^ ‘ ( 𝑜 ∈ ℕ ↦ ( ( ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑑𝑋 ( vol ‘ ( ( [,) ∘ ) ‘ 𝑑 ) ) ) ‘ ( 𝑚𝑜 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑑 ) +𝑒 𝑓 ) } = { 𝑖 ∈ ( ( 𝑏 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↦ { 𝑙 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∣ 𝑏 𝑗 ∈ ℕ X 𝑘𝑋 ( ( [,) ∘ ( 𝑙𝑗 ) ) ‘ 𝑘 ) } ) ‘ 𝑎 ) ∣ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑘𝑋 ( vol ‘ ( ( [,) ∘ ) ‘ 𝑘 ) ) ) ‘ ( 𝑖𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) +𝑒 𝑓 ) } )
79 78 mpteq2dv ( 𝑑 = 𝑎 → ( 𝑓 ∈ ℝ+ ↦ { 𝑚 ∈ ( ( 𝑏 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↦ { 𝑙 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∣ 𝑏 𝑜 ∈ ℕ X 𝑑𝑋 ( ( [,) ∘ ( 𝑙𝑜 ) ) ‘ 𝑑 ) } ) ‘ 𝑑 ) ∣ ( Σ^ ‘ ( 𝑜 ∈ ℕ ↦ ( ( ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑑𝑋 ( vol ‘ ( ( [,) ∘ ) ‘ 𝑑 ) ) ) ‘ ( 𝑚𝑜 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑑 ) +𝑒 𝑓 ) } ) = ( 𝑓 ∈ ℝ+ ↦ { 𝑖 ∈ ( ( 𝑏 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↦ { 𝑙 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∣ 𝑏 𝑗 ∈ ℕ X 𝑘𝑋 ( ( [,) ∘ ( 𝑙𝑗 ) ) ‘ 𝑘 ) } ) ‘ 𝑎 ) ∣ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑘𝑋 ( vol ‘ ( ( [,) ∘ ) ‘ 𝑘 ) ) ) ‘ ( 𝑖𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) +𝑒 𝑓 ) } ) )
80 oveq2 ( 𝑓 = 𝑒 → ( ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) +𝑒 𝑓 ) = ( ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) +𝑒 𝑒 ) )
81 80 breq2d ( 𝑓 = 𝑒 → ( ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑘𝑋 ( vol ‘ ( ( [,) ∘ ) ‘ 𝑘 ) ) ) ‘ ( 𝑖𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) +𝑒 𝑓 ) ↔ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑘𝑋 ( vol ‘ ( ( [,) ∘ ) ‘ 𝑘 ) ) ) ‘ ( 𝑖𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) +𝑒 𝑒 ) ) )
82 81 rabbidv ( 𝑓 = 𝑒 → { 𝑖 ∈ ( ( 𝑏 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↦ { 𝑙 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∣ 𝑏 𝑗 ∈ ℕ X 𝑘𝑋 ( ( [,) ∘ ( 𝑙𝑗 ) ) ‘ 𝑘 ) } ) ‘ 𝑎 ) ∣ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑘𝑋 ( vol ‘ ( ( [,) ∘ ) ‘ 𝑘 ) ) ) ‘ ( 𝑖𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) +𝑒 𝑓 ) } = { 𝑖 ∈ ( ( 𝑏 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↦ { 𝑙 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∣ 𝑏 𝑗 ∈ ℕ X 𝑘𝑋 ( ( [,) ∘ ( 𝑙𝑗 ) ) ‘ 𝑘 ) } ) ‘ 𝑎 ) ∣ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑘𝑋 ( vol ‘ ( ( [,) ∘ ) ‘ 𝑘 ) ) ) ‘ ( 𝑖𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) +𝑒 𝑒 ) } )
83 82 cbvmptv ( 𝑓 ∈ ℝ+ ↦ { 𝑖 ∈ ( ( 𝑏 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↦ { 𝑙 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∣ 𝑏 𝑗 ∈ ℕ X 𝑘𝑋 ( ( [,) ∘ ( 𝑙𝑗 ) ) ‘ 𝑘 ) } ) ‘ 𝑎 ) ∣ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑘𝑋 ( vol ‘ ( ( [,) ∘ ) ‘ 𝑘 ) ) ) ‘ ( 𝑖𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) +𝑒 𝑓 ) } ) = ( 𝑒 ∈ ℝ+ ↦ { 𝑖 ∈ ( ( 𝑏 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↦ { 𝑙 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∣ 𝑏 𝑗 ∈ ℕ X 𝑘𝑋 ( ( [,) ∘ ( 𝑙𝑗 ) ) ‘ 𝑘 ) } ) ‘ 𝑎 ) ∣ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑘𝑋 ( vol ‘ ( ( [,) ∘ ) ‘ 𝑘 ) ) ) ‘ ( 𝑖𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) +𝑒 𝑒 ) } )
84 79 83 eqtrdi ( 𝑑 = 𝑎 → ( 𝑓 ∈ ℝ+ ↦ { 𝑚 ∈ ( ( 𝑏 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↦ { 𝑙 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∣ 𝑏 𝑜 ∈ ℕ X 𝑑𝑋 ( ( [,) ∘ ( 𝑙𝑜 ) ) ‘ 𝑑 ) } ) ‘ 𝑑 ) ∣ ( Σ^ ‘ ( 𝑜 ∈ ℕ ↦ ( ( ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑑𝑋 ( vol ‘ ( ( [,) ∘ ) ‘ 𝑑 ) ) ) ‘ ( 𝑚𝑜 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑑 ) +𝑒 𝑓 ) } ) = ( 𝑒 ∈ ℝ+ ↦ { 𝑖 ∈ ( ( 𝑏 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↦ { 𝑙 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∣ 𝑏 𝑗 ∈ ℕ X 𝑘𝑋 ( ( [,) ∘ ( 𝑙𝑗 ) ) ‘ 𝑘 ) } ) ‘ 𝑎 ) ∣ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑘𝑋 ( vol ‘ ( ( [,) ∘ ) ‘ 𝑘 ) ) ) ‘ ( 𝑖𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) +𝑒 𝑒 ) } ) )
85 84 cbvmptv ( 𝑑 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↦ ( 𝑓 ∈ ℝ+ ↦ { 𝑚 ∈ ( ( 𝑏 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↦ { 𝑙 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∣ 𝑏 𝑜 ∈ ℕ X 𝑑𝑋 ( ( [,) ∘ ( 𝑙𝑜 ) ) ‘ 𝑑 ) } ) ‘ 𝑑 ) ∣ ( Σ^ ‘ ( 𝑜 ∈ ℕ ↦ ( ( ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑑𝑋 ( vol ‘ ( ( [,) ∘ ) ‘ 𝑑 ) ) ) ‘ ( 𝑚𝑜 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑑 ) +𝑒 𝑓 ) } ) ) = ( 𝑎 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↦ ( 𝑒 ∈ ℝ+ ↦ { 𝑖 ∈ ( ( 𝑏 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↦ { 𝑙 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∣ 𝑏 𝑗 ∈ ℕ X 𝑘𝑋 ( ( [,) ∘ ( 𝑙𝑗 ) ) ‘ 𝑘 ) } ) ‘ 𝑎 ) ∣ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑘𝑋 ( vol ‘ ( ( [,) ∘ ) ‘ 𝑘 ) ) ) ‘ ( 𝑖𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) +𝑒 𝑒 ) } ) )
86 33 35 36 37 38 41 42 85 ovnsubaddlem2 ( ( ( 𝜑 ∧ ¬ 𝑋 = ∅ ) ∧ 𝑦 ∈ ℝ+ ) → ( ( voln* ‘ 𝑋 ) ‘ 𝑛 ∈ ℕ ( 𝐴𝑛 ) ) ≤ ( ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴𝑛 ) ) ) ) +𝑒 𝑦 ) )
87 30 32 86 xrlexaddrp ( ( 𝜑 ∧ ¬ 𝑋 = ∅ ) → ( ( voln* ‘ 𝑋 ) ‘ 𝑛 ∈ ℕ ( 𝐴𝑛 ) ) ≤ ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴𝑛 ) ) ) ) )
88 28 87 pm2.61dan ( 𝜑 → ( ( voln* ‘ 𝑋 ) ‘ 𝑛 ∈ ℕ ( 𝐴𝑛 ) ) ≤ ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴𝑛 ) ) ) ) )