Metamath Proof Explorer


Theorem voliunsge0lem

Description: The Lebesgue measure function is countably additive. (Contributed by Glauco Siliprandi, 3-Mar-2021)

Ref Expression
Hypotheses voliunsge0lem.s 𝑆 = seq 1 ( + , 𝐺 )
voliunsge0lem.g 𝐺 = ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( 𝐸𝑛 ) ) )
voliunsge0lem.e ( 𝜑𝐸 : ℕ ⟶ dom vol )
voliunsge0lem.d ( 𝜑Disj 𝑛 ∈ ℕ ( 𝐸𝑛 ) )
Assertion voliunsge0lem ( 𝜑 → ( vol ‘ 𝑛 ∈ ℕ ( 𝐸𝑛 ) ) = ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( 𝐸𝑛 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 voliunsge0lem.s 𝑆 = seq 1 ( + , 𝐺 )
2 voliunsge0lem.g 𝐺 = ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( 𝐸𝑛 ) ) )
3 voliunsge0lem.e ( 𝜑𝐸 : ℕ ⟶ dom vol )
4 voliunsge0lem.d ( 𝜑Disj 𝑛 ∈ ℕ ( 𝐸𝑛 ) )
5 nfv 𝑛 𝜑
6 nfcv 𝑛 vol
7 nfiu1 𝑛 𝑛 ∈ ℕ ( 𝐸𝑛 )
8 6 7 nffv 𝑛 ( vol ‘ 𝑛 ∈ ℕ ( 𝐸𝑛 ) )
9 8 nfeq1 𝑛 ( vol ‘ 𝑛 ∈ ℕ ( 𝐸𝑛 ) ) = +∞
10 iccssxr ( 0 [,] +∞ ) ⊆ ℝ*
11 volf vol : dom vol ⟶ ( 0 [,] +∞ )
12 11 a1i ( 𝜑 → vol : dom vol ⟶ ( 0 [,] +∞ ) )
13 3 ffvelrnda ( ( 𝜑𝑛 ∈ ℕ ) → ( 𝐸𝑛 ) ∈ dom vol )
14 13 ralrimiva ( 𝜑 → ∀ 𝑛 ∈ ℕ ( 𝐸𝑛 ) ∈ dom vol )
15 iunmbl ( ∀ 𝑛 ∈ ℕ ( 𝐸𝑛 ) ∈ dom vol → 𝑛 ∈ ℕ ( 𝐸𝑛 ) ∈ dom vol )
16 14 15 syl ( 𝜑 𝑛 ∈ ℕ ( 𝐸𝑛 ) ∈ dom vol )
17 12 16 ffvelrnd ( 𝜑 → ( vol ‘ 𝑛 ∈ ℕ ( 𝐸𝑛 ) ) ∈ ( 0 [,] +∞ ) )
18 10 17 sselid ( 𝜑 → ( vol ‘ 𝑛 ∈ ℕ ( 𝐸𝑛 ) ) ∈ ℝ* )
19 18 adantr ( ( 𝜑𝑛 ∈ ℕ ) → ( vol ‘ 𝑛 ∈ ℕ ( 𝐸𝑛 ) ) ∈ ℝ* )
20 19 3adant3 ( ( 𝜑𝑛 ∈ ℕ ∧ ( vol ‘ ( 𝐸𝑛 ) ) = +∞ ) → ( vol ‘ 𝑛 ∈ ℕ ( 𝐸𝑛 ) ) ∈ ℝ* )
21 id ( ( vol ‘ ( 𝐸𝑛 ) ) = +∞ → ( vol ‘ ( 𝐸𝑛 ) ) = +∞ )
22 21 eqcomd ( ( vol ‘ ( 𝐸𝑛 ) ) = +∞ → +∞ = ( vol ‘ ( 𝐸𝑛 ) ) )
23 22 3ad2ant3 ( ( 𝜑𝑛 ∈ ℕ ∧ ( vol ‘ ( 𝐸𝑛 ) ) = +∞ ) → +∞ = ( vol ‘ ( 𝐸𝑛 ) ) )
24 16 adantr ( ( 𝜑𝑛 ∈ ℕ ) → 𝑛 ∈ ℕ ( 𝐸𝑛 ) ∈ dom vol )
25 ssiun2 ( 𝑛 ∈ ℕ → ( 𝐸𝑛 ) ⊆ 𝑛 ∈ ℕ ( 𝐸𝑛 ) )
26 25 adantl ( ( 𝜑𝑛 ∈ ℕ ) → ( 𝐸𝑛 ) ⊆ 𝑛 ∈ ℕ ( 𝐸𝑛 ) )
27 volss ( ( ( 𝐸𝑛 ) ∈ dom vol ∧ 𝑛 ∈ ℕ ( 𝐸𝑛 ) ∈ dom vol ∧ ( 𝐸𝑛 ) ⊆ 𝑛 ∈ ℕ ( 𝐸𝑛 ) ) → ( vol ‘ ( 𝐸𝑛 ) ) ≤ ( vol ‘ 𝑛 ∈ ℕ ( 𝐸𝑛 ) ) )
28 13 24 26 27 syl3anc ( ( 𝜑𝑛 ∈ ℕ ) → ( vol ‘ ( 𝐸𝑛 ) ) ≤ ( vol ‘ 𝑛 ∈ ℕ ( 𝐸𝑛 ) ) )
29 28 3adant3 ( ( 𝜑𝑛 ∈ ℕ ∧ ( vol ‘ ( 𝐸𝑛 ) ) = +∞ ) → ( vol ‘ ( 𝐸𝑛 ) ) ≤ ( vol ‘ 𝑛 ∈ ℕ ( 𝐸𝑛 ) ) )
30 23 29 eqbrtrd ( ( 𝜑𝑛 ∈ ℕ ∧ ( vol ‘ ( 𝐸𝑛 ) ) = +∞ ) → +∞ ≤ ( vol ‘ 𝑛 ∈ ℕ ( 𝐸𝑛 ) ) )
31 20 30 xrgepnfd ( ( 𝜑𝑛 ∈ ℕ ∧ ( vol ‘ ( 𝐸𝑛 ) ) = +∞ ) → ( vol ‘ 𝑛 ∈ ℕ ( 𝐸𝑛 ) ) = +∞ )
32 31 3exp ( 𝜑 → ( 𝑛 ∈ ℕ → ( ( vol ‘ ( 𝐸𝑛 ) ) = +∞ → ( vol ‘ 𝑛 ∈ ℕ ( 𝐸𝑛 ) ) = +∞ ) ) )
33 5 9 32 rexlimd ( 𝜑 → ( ∃ 𝑛 ∈ ℕ ( vol ‘ ( 𝐸𝑛 ) ) = +∞ → ( vol ‘ 𝑛 ∈ ℕ ( 𝐸𝑛 ) ) = +∞ ) )
34 33 imp ( ( 𝜑 ∧ ∃ 𝑛 ∈ ℕ ( vol ‘ ( 𝐸𝑛 ) ) = +∞ ) → ( vol ‘ 𝑛 ∈ ℕ ( 𝐸𝑛 ) ) = +∞ )
35 nfre1 𝑛𝑛 ∈ ℕ ( vol ‘ ( 𝐸𝑛 ) ) = +∞
36 5 35 nfan 𝑛 ( 𝜑 ∧ ∃ 𝑛 ∈ ℕ ( vol ‘ ( 𝐸𝑛 ) ) = +∞ )
37 nnex ℕ ∈ V
38 37 a1i ( ( 𝜑 ∧ ∃ 𝑛 ∈ ℕ ( vol ‘ ( 𝐸𝑛 ) ) = +∞ ) → ℕ ∈ V )
39 11 a1i ( ( 𝜑𝑛 ∈ ℕ ) → vol : dom vol ⟶ ( 0 [,] +∞ ) )
40 39 13 ffvelrnd ( ( 𝜑𝑛 ∈ ℕ ) → ( vol ‘ ( 𝐸𝑛 ) ) ∈ ( 0 [,] +∞ ) )
41 40 adantlr ( ( ( 𝜑 ∧ ∃ 𝑛 ∈ ℕ ( vol ‘ ( 𝐸𝑛 ) ) = +∞ ) ∧ 𝑛 ∈ ℕ ) → ( vol ‘ ( 𝐸𝑛 ) ) ∈ ( 0 [,] +∞ ) )
42 simpr ( ( 𝜑 ∧ ∃ 𝑛 ∈ ℕ ( vol ‘ ( 𝐸𝑛 ) ) = +∞ ) → ∃ 𝑛 ∈ ℕ ( vol ‘ ( 𝐸𝑛 ) ) = +∞ )
43 36 38 41 42 sge0pnfmpt ( ( 𝜑 ∧ ∃ 𝑛 ∈ ℕ ( vol ‘ ( 𝐸𝑛 ) ) = +∞ ) → ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( 𝐸𝑛 ) ) ) ) = +∞ )
44 34 43 eqtr4d ( ( 𝜑 ∧ ∃ 𝑛 ∈ ℕ ( vol ‘ ( 𝐸𝑛 ) ) = +∞ ) → ( vol ‘ 𝑛 ∈ ℕ ( 𝐸𝑛 ) ) = ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( 𝐸𝑛 ) ) ) ) )
45 ralnex ( ∀ 𝑛 ∈ ℕ ¬ ( vol ‘ ( 𝐸𝑛 ) ) = +∞ ↔ ¬ ∃ 𝑛 ∈ ℕ ( vol ‘ ( 𝐸𝑛 ) ) = +∞ )
46 45 biimpri ( ¬ ∃ 𝑛 ∈ ℕ ( vol ‘ ( 𝐸𝑛 ) ) = +∞ → ∀ 𝑛 ∈ ℕ ¬ ( vol ‘ ( 𝐸𝑛 ) ) = +∞ )
47 46 adantl ( ( 𝜑 ∧ ¬ ∃ 𝑛 ∈ ℕ ( vol ‘ ( 𝐸𝑛 ) ) = +∞ ) → ∀ 𝑛 ∈ ℕ ¬ ( vol ‘ ( 𝐸𝑛 ) ) = +∞ )
48 40 adantr ( ( ( 𝜑𝑛 ∈ ℕ ) ∧ ¬ ( vol ‘ ( 𝐸𝑛 ) ) = +∞ ) → ( vol ‘ ( 𝐸𝑛 ) ) ∈ ( 0 [,] +∞ ) )
49 21 necon3bi ( ¬ ( vol ‘ ( 𝐸𝑛 ) ) = +∞ → ( vol ‘ ( 𝐸𝑛 ) ) ≠ +∞ )
50 49 adantl ( ( ( 𝜑𝑛 ∈ ℕ ) ∧ ¬ ( vol ‘ ( 𝐸𝑛 ) ) = +∞ ) → ( vol ‘ ( 𝐸𝑛 ) ) ≠ +∞ )
51 ge0xrre ( ( ( vol ‘ ( 𝐸𝑛 ) ) ∈ ( 0 [,] +∞ ) ∧ ( vol ‘ ( 𝐸𝑛 ) ) ≠ +∞ ) → ( vol ‘ ( 𝐸𝑛 ) ) ∈ ℝ )
52 48 50 51 syl2anc ( ( ( 𝜑𝑛 ∈ ℕ ) ∧ ¬ ( vol ‘ ( 𝐸𝑛 ) ) = +∞ ) → ( vol ‘ ( 𝐸𝑛 ) ) ∈ ℝ )
53 52 ex ( ( 𝜑𝑛 ∈ ℕ ) → ( ¬ ( vol ‘ ( 𝐸𝑛 ) ) = +∞ → ( vol ‘ ( 𝐸𝑛 ) ) ∈ ℝ ) )
54 renepnf ( ( vol ‘ ( 𝐸𝑛 ) ) ∈ ℝ → ( vol ‘ ( 𝐸𝑛 ) ) ≠ +∞ )
55 54 neneqd ( ( vol ‘ ( 𝐸𝑛 ) ) ∈ ℝ → ¬ ( vol ‘ ( 𝐸𝑛 ) ) = +∞ )
56 55 a1i ( ( 𝜑𝑛 ∈ ℕ ) → ( ( vol ‘ ( 𝐸𝑛 ) ) ∈ ℝ → ¬ ( vol ‘ ( 𝐸𝑛 ) ) = +∞ ) )
57 53 56 impbid ( ( 𝜑𝑛 ∈ ℕ ) → ( ¬ ( vol ‘ ( 𝐸𝑛 ) ) = +∞ ↔ ( vol ‘ ( 𝐸𝑛 ) ) ∈ ℝ ) )
58 57 ralbidva ( 𝜑 → ( ∀ 𝑛 ∈ ℕ ¬ ( vol ‘ ( 𝐸𝑛 ) ) = +∞ ↔ ∀ 𝑛 ∈ ℕ ( vol ‘ ( 𝐸𝑛 ) ) ∈ ℝ ) )
59 58 adantr ( ( 𝜑 ∧ ¬ ∃ 𝑛 ∈ ℕ ( vol ‘ ( 𝐸𝑛 ) ) = +∞ ) → ( ∀ 𝑛 ∈ ℕ ¬ ( vol ‘ ( 𝐸𝑛 ) ) = +∞ ↔ ∀ 𝑛 ∈ ℕ ( vol ‘ ( 𝐸𝑛 ) ) ∈ ℝ ) )
60 47 59 mpbid ( ( 𝜑 ∧ ¬ ∃ 𝑛 ∈ ℕ ( vol ‘ ( 𝐸𝑛 ) ) = +∞ ) → ∀ 𝑛 ∈ ℕ ( vol ‘ ( 𝐸𝑛 ) ) ∈ ℝ )
61 nfra1 𝑛𝑛 ∈ ℕ ( vol ‘ ( 𝐸𝑛 ) ) ∈ ℝ
62 5 61 nfan 𝑛 ( 𝜑 ∧ ∀ 𝑛 ∈ ℕ ( vol ‘ ( 𝐸𝑛 ) ) ∈ ℝ )
63 13 adantlr ( ( ( 𝜑 ∧ ∀ 𝑛 ∈ ℕ ( vol ‘ ( 𝐸𝑛 ) ) ∈ ℝ ) ∧ 𝑛 ∈ ℕ ) → ( 𝐸𝑛 ) ∈ dom vol )
64 rspa ( ( ∀ 𝑛 ∈ ℕ ( vol ‘ ( 𝐸𝑛 ) ) ∈ ℝ ∧ 𝑛 ∈ ℕ ) → ( vol ‘ ( 𝐸𝑛 ) ) ∈ ℝ )
65 64 adantll ( ( ( 𝜑 ∧ ∀ 𝑛 ∈ ℕ ( vol ‘ ( 𝐸𝑛 ) ) ∈ ℝ ) ∧ 𝑛 ∈ ℕ ) → ( vol ‘ ( 𝐸𝑛 ) ) ∈ ℝ )
66 63 65 jca ( ( ( 𝜑 ∧ ∀ 𝑛 ∈ ℕ ( vol ‘ ( 𝐸𝑛 ) ) ∈ ℝ ) ∧ 𝑛 ∈ ℕ ) → ( ( 𝐸𝑛 ) ∈ dom vol ∧ ( vol ‘ ( 𝐸𝑛 ) ) ∈ ℝ ) )
67 66 ex ( ( 𝜑 ∧ ∀ 𝑛 ∈ ℕ ( vol ‘ ( 𝐸𝑛 ) ) ∈ ℝ ) → ( 𝑛 ∈ ℕ → ( ( 𝐸𝑛 ) ∈ dom vol ∧ ( vol ‘ ( 𝐸𝑛 ) ) ∈ ℝ ) ) )
68 62 67 ralrimi ( ( 𝜑 ∧ ∀ 𝑛 ∈ ℕ ( vol ‘ ( 𝐸𝑛 ) ) ∈ ℝ ) → ∀ 𝑛 ∈ ℕ ( ( 𝐸𝑛 ) ∈ dom vol ∧ ( vol ‘ ( 𝐸𝑛 ) ) ∈ ℝ ) )
69 4 adantr ( ( 𝜑 ∧ ∀ 𝑛 ∈ ℕ ( vol ‘ ( 𝐸𝑛 ) ) ∈ ℝ ) → Disj 𝑛 ∈ ℕ ( 𝐸𝑛 ) )
70 1 2 voliun ( ( ∀ 𝑛 ∈ ℕ ( ( 𝐸𝑛 ) ∈ dom vol ∧ ( vol ‘ ( 𝐸𝑛 ) ) ∈ ℝ ) ∧ Disj 𝑛 ∈ ℕ ( 𝐸𝑛 ) ) → ( vol ‘ 𝑛 ∈ ℕ ( 𝐸𝑛 ) ) = sup ( ran 𝑆 , ℝ* , < ) )
71 68 69 70 syl2anc ( ( 𝜑 ∧ ∀ 𝑛 ∈ ℕ ( vol ‘ ( 𝐸𝑛 ) ) ∈ ℝ ) → ( vol ‘ 𝑛 ∈ ℕ ( 𝐸𝑛 ) ) = sup ( ran 𝑆 , ℝ* , < ) )
72 1zzd ( ( 𝜑 ∧ ∀ 𝑛 ∈ ℕ ( vol ‘ ( 𝐸𝑛 ) ) ∈ ℝ ) → 1 ∈ ℤ )
73 nnuz ℕ = ( ℤ ‘ 1 )
74 nfv 𝑛 𝑚 ∈ ℕ
75 62 74 nfan 𝑛 ( ( 𝜑 ∧ ∀ 𝑛 ∈ ℕ ( vol ‘ ( 𝐸𝑛 ) ) ∈ ℝ ) ∧ 𝑚 ∈ ℕ )
76 nfv 𝑛 ( vol ‘ ( 𝐸𝑚 ) ) ∈ ( 0 [,) +∞ )
77 75 76 nfim 𝑛 ( ( ( 𝜑 ∧ ∀ 𝑛 ∈ ℕ ( vol ‘ ( 𝐸𝑛 ) ) ∈ ℝ ) ∧ 𝑚 ∈ ℕ ) → ( vol ‘ ( 𝐸𝑚 ) ) ∈ ( 0 [,) +∞ ) )
78 eleq1w ( 𝑛 = 𝑚 → ( 𝑛 ∈ ℕ ↔ 𝑚 ∈ ℕ ) )
79 78 anbi2d ( 𝑛 = 𝑚 → ( ( ( 𝜑 ∧ ∀ 𝑛 ∈ ℕ ( vol ‘ ( 𝐸𝑛 ) ) ∈ ℝ ) ∧ 𝑛 ∈ ℕ ) ↔ ( ( 𝜑 ∧ ∀ 𝑛 ∈ ℕ ( vol ‘ ( 𝐸𝑛 ) ) ∈ ℝ ) ∧ 𝑚 ∈ ℕ ) ) )
80 2fveq3 ( 𝑛 = 𝑚 → ( vol ‘ ( 𝐸𝑛 ) ) = ( vol ‘ ( 𝐸𝑚 ) ) )
81 80 eleq1d ( 𝑛 = 𝑚 → ( ( vol ‘ ( 𝐸𝑛 ) ) ∈ ( 0 [,) +∞ ) ↔ ( vol ‘ ( 𝐸𝑚 ) ) ∈ ( 0 [,) +∞ ) ) )
82 79 81 imbi12d ( 𝑛 = 𝑚 → ( ( ( ( 𝜑 ∧ ∀ 𝑛 ∈ ℕ ( vol ‘ ( 𝐸𝑛 ) ) ∈ ℝ ) ∧ 𝑛 ∈ ℕ ) → ( vol ‘ ( 𝐸𝑛 ) ) ∈ ( 0 [,) +∞ ) ) ↔ ( ( ( 𝜑 ∧ ∀ 𝑛 ∈ ℕ ( vol ‘ ( 𝐸𝑛 ) ) ∈ ℝ ) ∧ 𝑚 ∈ ℕ ) → ( vol ‘ ( 𝐸𝑚 ) ) ∈ ( 0 [,) +∞ ) ) ) )
83 0xr 0 ∈ ℝ*
84 83 a1i ( ( ( 𝜑 ∧ ∀ 𝑛 ∈ ℕ ( vol ‘ ( 𝐸𝑛 ) ) ∈ ℝ ) ∧ 𝑛 ∈ ℕ ) → 0 ∈ ℝ* )
85 pnfxr +∞ ∈ ℝ*
86 85 a1i ( ( ( 𝜑 ∧ ∀ 𝑛 ∈ ℕ ( vol ‘ ( 𝐸𝑛 ) ) ∈ ℝ ) ∧ 𝑛 ∈ ℕ ) → +∞ ∈ ℝ* )
87 65 rexrd ( ( ( 𝜑 ∧ ∀ 𝑛 ∈ ℕ ( vol ‘ ( 𝐸𝑛 ) ) ∈ ℝ ) ∧ 𝑛 ∈ ℕ ) → ( vol ‘ ( 𝐸𝑛 ) ) ∈ ℝ* )
88 volge0 ( ( 𝐸𝑛 ) ∈ dom vol → 0 ≤ ( vol ‘ ( 𝐸𝑛 ) ) )
89 13 88 syl ( ( 𝜑𝑛 ∈ ℕ ) → 0 ≤ ( vol ‘ ( 𝐸𝑛 ) ) )
90 89 adantlr ( ( ( 𝜑 ∧ ∀ 𝑛 ∈ ℕ ( vol ‘ ( 𝐸𝑛 ) ) ∈ ℝ ) ∧ 𝑛 ∈ ℕ ) → 0 ≤ ( vol ‘ ( 𝐸𝑛 ) ) )
91 65 ltpnfd ( ( ( 𝜑 ∧ ∀ 𝑛 ∈ ℕ ( vol ‘ ( 𝐸𝑛 ) ) ∈ ℝ ) ∧ 𝑛 ∈ ℕ ) → ( vol ‘ ( 𝐸𝑛 ) ) < +∞ )
92 84 86 87 90 91 elicod ( ( ( 𝜑 ∧ ∀ 𝑛 ∈ ℕ ( vol ‘ ( 𝐸𝑛 ) ) ∈ ℝ ) ∧ 𝑛 ∈ ℕ ) → ( vol ‘ ( 𝐸𝑛 ) ) ∈ ( 0 [,) +∞ ) )
93 77 82 92 chvarfv ( ( ( 𝜑 ∧ ∀ 𝑛 ∈ ℕ ( vol ‘ ( 𝐸𝑛 ) ) ∈ ℝ ) ∧ 𝑚 ∈ ℕ ) → ( vol ‘ ( 𝐸𝑚 ) ) ∈ ( 0 [,) +∞ ) )
94 80 cbvmptv ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( 𝐸𝑛 ) ) ) = ( 𝑚 ∈ ℕ ↦ ( vol ‘ ( 𝐸𝑚 ) ) )
95 93 94 fmptd ( ( 𝜑 ∧ ∀ 𝑛 ∈ ℕ ( vol ‘ ( 𝐸𝑛 ) ) ∈ ℝ ) → ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( 𝐸𝑛 ) ) ) : ℕ ⟶ ( 0 [,) +∞ ) )
96 seqeq3 ( 𝐺 = ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( 𝐸𝑛 ) ) ) → seq 1 ( + , 𝐺 ) = seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( 𝐸𝑛 ) ) ) ) )
97 2 96 ax-mp seq 1 ( + , 𝐺 ) = seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( 𝐸𝑛 ) ) ) )
98 1 97 eqtri 𝑆 = seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( 𝐸𝑛 ) ) ) )
99 72 73 95 98 sge0seq ( ( 𝜑 ∧ ∀ 𝑛 ∈ ℕ ( vol ‘ ( 𝐸𝑛 ) ) ∈ ℝ ) → ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( 𝐸𝑛 ) ) ) ) = sup ( ran 𝑆 , ℝ* , < ) )
100 71 99 eqtr4d ( ( 𝜑 ∧ ∀ 𝑛 ∈ ℕ ( vol ‘ ( 𝐸𝑛 ) ) ∈ ℝ ) → ( vol ‘ 𝑛 ∈ ℕ ( 𝐸𝑛 ) ) = ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( 𝐸𝑛 ) ) ) ) )
101 60 100 syldan ( ( 𝜑 ∧ ¬ ∃ 𝑛 ∈ ℕ ( vol ‘ ( 𝐸𝑛 ) ) = +∞ ) → ( vol ‘ 𝑛 ∈ ℕ ( 𝐸𝑛 ) ) = ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( 𝐸𝑛 ) ) ) ) )
102 44 101 pm2.61dan ( 𝜑 → ( vol ‘ 𝑛 ∈ ℕ ( 𝐸𝑛 ) ) = ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( 𝐸𝑛 ) ) ) ) )