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 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐸 ‘ 𝑛 ) ∈ dom vol )
14 13 ralrimiva ⊢ ( 𝜑 → ∀ 𝑛 ∈ ℕ ( 𝐸 ‘ 𝑛 ) ∈ dom vol )
15 iunmbl ⊢ ( ∀ 𝑛 ∈ ℕ ( 𝐸 ‘ 𝑛 ) ∈ dom vol → ∪ 𝑛 ∈ ℕ ( 𝐸 ‘ 𝑛 ) ∈ dom vol )
16 14 15 syl ⊢ ( 𝜑 → ∪ 𝑛 ∈ ℕ ( 𝐸 ‘ 𝑛 ) ∈ dom vol )
17 12 16 ffvelcdmd ⊢ ( 𝜑 → ( 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 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 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 bilanri ⊢ ( ( 𝜑 ∧ ¬ ∃ 𝑛 ∈ ℕ ( vol ‘ ( 𝐸 ‘ 𝑛 ) ) = +∞ ) → ∀ 𝑛 ∈ ℕ ¬ ( vol ‘ ( 𝐸 ‘ 𝑛 ) ) = +∞ )
47 40 adantr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ ¬ ( vol ‘ ( 𝐸 ‘ 𝑛 ) ) = +∞ ) → ( vol ‘ ( 𝐸 ‘ 𝑛 ) ) ∈ ( 0 [,] +∞ ) )
48 21 necon3bi ⊢ ( ¬ ( vol ‘ ( 𝐸 ‘ 𝑛 ) ) = +∞ → ( vol ‘ ( 𝐸 ‘ 𝑛 ) ) ≠ +∞ )
49 48 adantl ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ ¬ ( vol ‘ ( 𝐸 ‘ 𝑛 ) ) = +∞ ) → ( vol ‘ ( 𝐸 ‘ 𝑛 ) ) ≠ +∞ )
50 ge0xrre ⊢ ( ( ( vol ‘ ( 𝐸 ‘ 𝑛 ) ) ∈ ( 0 [,] +∞ ) ∧ ( vol ‘ ( 𝐸 ‘ 𝑛 ) ) ≠ +∞ ) → ( vol ‘ ( 𝐸 ‘ 𝑛 ) ) ∈ ℝ )
51 47 49 50 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ ¬ ( vol ‘ ( 𝐸 ‘ 𝑛 ) ) = +∞ ) → ( vol ‘ ( 𝐸 ‘ 𝑛 ) ) ∈ ℝ )
52 51 ex ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ¬ ( vol ‘ ( 𝐸 ‘ 𝑛 ) ) = +∞ → ( vol ‘ ( 𝐸 ‘ 𝑛 ) ) ∈ ℝ ) )
53 renepnf ⊢ ( ( vol ‘ ( 𝐸 ‘ 𝑛 ) ) ∈ ℝ → ( vol ‘ ( 𝐸 ‘ 𝑛 ) ) ≠ +∞ )
54 53 neneqd ⊢ ( ( vol ‘ ( 𝐸 ‘ 𝑛 ) ) ∈ ℝ → ¬ ( vol ‘ ( 𝐸 ‘ 𝑛 ) ) = +∞ )
55 54 a1i ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( vol ‘ ( 𝐸 ‘ 𝑛 ) ) ∈ ℝ → ¬ ( vol ‘ ( 𝐸 ‘ 𝑛 ) ) = +∞ ) )
56 52 55 impbid ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ¬ ( vol ‘ ( 𝐸 ‘ 𝑛 ) ) = +∞ ↔ ( vol ‘ ( 𝐸 ‘ 𝑛 ) ) ∈ ℝ ) )
57 56 ralbidva ⊢ ( 𝜑 → ( ∀ 𝑛 ∈ ℕ ¬ ( vol ‘ ( 𝐸 ‘ 𝑛 ) ) = +∞ ↔ ∀ 𝑛 ∈ ℕ ( vol ‘ ( 𝐸 ‘ 𝑛 ) ) ∈ ℝ ) )
58 57 adantr ⊢ ( ( 𝜑 ∧ ¬ ∃ 𝑛 ∈ ℕ ( vol ‘ ( 𝐸 ‘ 𝑛 ) ) = +∞ ) → ( ∀ 𝑛 ∈ ℕ ¬ ( vol ‘ ( 𝐸 ‘ 𝑛 ) ) = +∞ ↔ ∀ 𝑛 ∈ ℕ ( vol ‘ ( 𝐸 ‘ 𝑛 ) ) ∈ ℝ ) )
59 46 58 mpbid ⊢ ( ( 𝜑 ∧ ¬ ∃ 𝑛 ∈ ℕ ( vol ‘ ( 𝐸 ‘ 𝑛 ) ) = +∞ ) → ∀ 𝑛 ∈ ℕ ( vol ‘ ( 𝐸 ‘ 𝑛 ) ) ∈ ℝ )
60 nfra1 ⊢ Ⅎ 𝑛 ∀ 𝑛 ∈ ℕ ( vol ‘ ( 𝐸 ‘ 𝑛 ) ) ∈ ℝ
61 5 60 nfan ⊢ Ⅎ 𝑛 ( 𝜑 ∧ ∀ 𝑛 ∈ ℕ ( vol ‘ ( 𝐸 ‘ 𝑛 ) ) ∈ ℝ )
62 13 adantlr ⊢ ( ( ( 𝜑 ∧ ∀ 𝑛 ∈ ℕ ( vol ‘ ( 𝐸 ‘ 𝑛 ) ) ∈ ℝ ) ∧ 𝑛 ∈ ℕ ) → ( 𝐸 ‘ 𝑛 ) ∈ dom vol )
63 rspa ⊢ ( ( ∀ 𝑛 ∈ ℕ ( vol ‘ ( 𝐸 ‘ 𝑛 ) ) ∈ ℝ ∧ 𝑛 ∈ ℕ ) → ( vol ‘ ( 𝐸 ‘ 𝑛 ) ) ∈ ℝ )
64 63 adantll ⊢ ( ( ( 𝜑 ∧ ∀ 𝑛 ∈ ℕ ( vol ‘ ( 𝐸 ‘ 𝑛 ) ) ∈ ℝ ) ∧ 𝑛 ∈ ℕ ) → ( vol ‘ ( 𝐸 ‘ 𝑛 ) ) ∈ ℝ )
65 62 64 jca ⊢ ( ( ( 𝜑 ∧ ∀ 𝑛 ∈ ℕ ( vol ‘ ( 𝐸 ‘ 𝑛 ) ) ∈ ℝ ) ∧ 𝑛 ∈ ℕ ) → ( ( 𝐸 ‘ 𝑛 ) ∈ dom vol ∧ ( vol ‘ ( 𝐸 ‘ 𝑛 ) ) ∈ ℝ ) )
66 65 ex ⊢ ( ( 𝜑 ∧ ∀ 𝑛 ∈ ℕ ( vol ‘ ( 𝐸 ‘ 𝑛 ) ) ∈ ℝ ) → ( 𝑛 ∈ ℕ → ( ( 𝐸 ‘ 𝑛 ) ∈ dom vol ∧ ( vol ‘ ( 𝐸 ‘ 𝑛 ) ) ∈ ℝ ) ) )
67 61 66 ralrimi ⊢ ( ( 𝜑 ∧ ∀ 𝑛 ∈ ℕ ( vol ‘ ( 𝐸 ‘ 𝑛 ) ) ∈ ℝ ) → ∀ 𝑛 ∈ ℕ ( ( 𝐸 ‘ 𝑛 ) ∈ dom vol ∧ ( vol ‘ ( 𝐸 ‘ 𝑛 ) ) ∈ ℝ ) )
68 4 adantr ⊢ ( ( 𝜑 ∧ ∀ 𝑛 ∈ ℕ ( vol ‘ ( 𝐸 ‘ 𝑛 ) ) ∈ ℝ ) → Disj 𝑛 ∈ ℕ ( 𝐸 ‘ 𝑛 ) )
69 1 2 voliun ⊢ ( ( ∀ 𝑛 ∈ ℕ ( ( 𝐸 ‘ 𝑛 ) ∈ dom vol ∧ ( vol ‘ ( 𝐸 ‘ 𝑛 ) ) ∈ ℝ ) ∧ Disj 𝑛 ∈ ℕ ( 𝐸 ‘ 𝑛 ) ) → ( vol ‘ ∪ 𝑛 ∈ ℕ ( 𝐸 ‘ 𝑛 ) ) = sup ( ran 𝑆 , ℝ* , < ) )
70 67 68 69 syl2anc ⊢ ( ( 𝜑 ∧ ∀ 𝑛 ∈ ℕ ( vol ‘ ( 𝐸 ‘ 𝑛 ) ) ∈ ℝ ) → ( vol ‘ ∪ 𝑛 ∈ ℕ ( 𝐸 ‘ 𝑛 ) ) = sup ( ran 𝑆 , ℝ* , < ) )
71 1zzd ⊢ ( ( 𝜑 ∧ ∀ 𝑛 ∈ ℕ ( vol ‘ ( 𝐸 ‘ 𝑛 ) ) ∈ ℝ ) → 1 ∈ ℤ )
72 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
73 nfv ⊢ Ⅎ 𝑛 𝑚 ∈ ℕ
74 61 73 nfan ⊢ Ⅎ 𝑛 ( ( 𝜑 ∧ ∀ 𝑛 ∈ ℕ ( vol ‘ ( 𝐸 ‘ 𝑛 ) ) ∈ ℝ ) ∧ 𝑚 ∈ ℕ )
75 nfv ⊢ Ⅎ 𝑛 ( vol ‘ ( 𝐸 ‘ 𝑚 ) ) ∈ ( 0 [,) +∞ )
76 74 75 nfim ⊢ Ⅎ 𝑛 ( ( ( 𝜑 ∧ ∀ 𝑛 ∈ ℕ ( vol ‘ ( 𝐸 ‘ 𝑛 ) ) ∈ ℝ ) ∧ 𝑚 ∈ ℕ ) → ( vol ‘ ( 𝐸 ‘ 𝑚 ) ) ∈ ( 0 [,) +∞ ) )
77 eleq1w ⊢ ( 𝑛 = 𝑚 → ( 𝑛 ∈ ℕ ↔ 𝑚 ∈ ℕ ) )
78 77 anbi2d ⊢ ( 𝑛 = 𝑚 → ( ( ( 𝜑 ∧ ∀ 𝑛 ∈ ℕ ( vol ‘ ( 𝐸 ‘ 𝑛 ) ) ∈ ℝ ) ∧ 𝑛 ∈ ℕ ) ↔ ( ( 𝜑 ∧ ∀ 𝑛 ∈ ℕ ( vol ‘ ( 𝐸 ‘ 𝑛 ) ) ∈ ℝ ) ∧ 𝑚 ∈ ℕ ) ) )
79 2fveq3 ⊢ ( 𝑛 = 𝑚 → ( vol ‘ ( 𝐸 ‘ 𝑛 ) ) = ( vol ‘ ( 𝐸 ‘ 𝑚 ) ) )
80 79 eleq1d ⊢ ( 𝑛 = 𝑚 → ( ( vol ‘ ( 𝐸 ‘ 𝑛 ) ) ∈ ( 0 [,) +∞ ) ↔ ( vol ‘ ( 𝐸 ‘ 𝑚 ) ) ∈ ( 0 [,) +∞ ) ) )
81 78 80 imbi12d ⊢ ( 𝑛 = 𝑚 → ( ( ( ( 𝜑 ∧ ∀ 𝑛 ∈ ℕ ( vol ‘ ( 𝐸 ‘ 𝑛 ) ) ∈ ℝ ) ∧ 𝑛 ∈ ℕ ) → ( vol ‘ ( 𝐸 ‘ 𝑛 ) ) ∈ ( 0 [,) +∞ ) ) ↔ ( ( ( 𝜑 ∧ ∀ 𝑛 ∈ ℕ ( vol ‘ ( 𝐸 ‘ 𝑛 ) ) ∈ ℝ ) ∧ 𝑚 ∈ ℕ ) → ( vol ‘ ( 𝐸 ‘ 𝑚 ) ) ∈ ( 0 [,) +∞ ) ) ) )
82 0xr ⊢ 0 ∈ ℝ*
83 82 a1i ⊢ ( ( ( 𝜑 ∧ ∀ 𝑛 ∈ ℕ ( vol ‘ ( 𝐸 ‘ 𝑛 ) ) ∈ ℝ ) ∧ 𝑛 ∈ ℕ ) → 0 ∈ ℝ* )
84 pnfxr ⊢ +∞ ∈ ℝ*
85 84 a1i ⊢ ( ( ( 𝜑 ∧ ∀ 𝑛 ∈ ℕ ( vol ‘ ( 𝐸 ‘ 𝑛 ) ) ∈ ℝ ) ∧ 𝑛 ∈ ℕ ) → +∞ ∈ ℝ* )
86 64 rexrd ⊢ ( ( ( 𝜑 ∧ ∀ 𝑛 ∈ ℕ ( vol ‘ ( 𝐸 ‘ 𝑛 ) ) ∈ ℝ ) ∧ 𝑛 ∈ ℕ ) → ( vol ‘ ( 𝐸 ‘ 𝑛 ) ) ∈ ℝ* )
87 volge0 ⊢ ( ( 𝐸 ‘ 𝑛 ) ∈ dom vol → 0 ≤ ( vol ‘ ( 𝐸 ‘ 𝑛 ) ) )
88 13 87 syl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 0 ≤ ( vol ‘ ( 𝐸 ‘ 𝑛 ) ) )
89 88 adantlr ⊢ ( ( ( 𝜑 ∧ ∀ 𝑛 ∈ ℕ ( vol ‘ ( 𝐸 ‘ 𝑛 ) ) ∈ ℝ ) ∧ 𝑛 ∈ ℕ ) → 0 ≤ ( vol ‘ ( 𝐸 ‘ 𝑛 ) ) )
90 64 ltpnfd ⊢ ( ( ( 𝜑 ∧ ∀ 𝑛 ∈ ℕ ( vol ‘ ( 𝐸 ‘ 𝑛 ) ) ∈ ℝ ) ∧ 𝑛 ∈ ℕ ) → ( vol ‘ ( 𝐸 ‘ 𝑛 ) ) < +∞ )
91 83 85 86 89 90 elicod ⊢ ( ( ( 𝜑 ∧ ∀ 𝑛 ∈ ℕ ( vol ‘ ( 𝐸 ‘ 𝑛 ) ) ∈ ℝ ) ∧ 𝑛 ∈ ℕ ) → ( vol ‘ ( 𝐸 ‘ 𝑛 ) ) ∈ ( 0 [,) +∞ ) )
92 76 81 91 chvarfv ⊢ ( ( ( 𝜑 ∧ ∀ 𝑛 ∈ ℕ ( vol ‘ ( 𝐸 ‘ 𝑛 ) ) ∈ ℝ ) ∧ 𝑚 ∈ ℕ ) → ( vol ‘ ( 𝐸 ‘ 𝑚 ) ) ∈ ( 0 [,) +∞ ) )
93 79 cbvmptv ⊢ ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( 𝐸 ‘ 𝑛 ) ) ) = ( 𝑚 ∈ ℕ ↦ ( vol ‘ ( 𝐸 ‘ 𝑚 ) ) )
94 92 93 fmptd ⊢ ( ( 𝜑 ∧ ∀ 𝑛 ∈ ℕ ( vol ‘ ( 𝐸 ‘ 𝑛 ) ) ∈ ℝ ) → ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( 𝐸 ‘ 𝑛 ) ) ) : ℕ ⟶ ( 0 [,) +∞ ) )
95 seqeq3 ⊢ ( 𝐺 = ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( 𝐸 ‘ 𝑛 ) ) ) → seq 1 ( + , 𝐺 ) = seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) )
96 2 95 ax-mp ⊢ seq 1 ( + , 𝐺 ) = seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( 𝐸 ‘ 𝑛 ) ) ) )
97 1 96 eqtri ⊢ 𝑆 = seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( 𝐸 ‘ 𝑛 ) ) ) )
98 71 72 94 97 sge0seq ⊢ ( ( 𝜑 ∧ ∀ 𝑛 ∈ ℕ ( vol ‘ ( 𝐸 ‘ 𝑛 ) ) ∈ ℝ ) → ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) = sup ( ran 𝑆 , ℝ* , < ) )
99 70 98 eqtr4d ⊢ ( ( 𝜑 ∧ ∀ 𝑛 ∈ ℕ ( vol ‘ ( 𝐸 ‘ 𝑛 ) ) ∈ ℝ ) → ( vol ‘ ∪ 𝑛 ∈ ℕ ( 𝐸 ‘ 𝑛 ) ) = ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) )
100 59 99 syldan ⊢ ( ( 𝜑 ∧ ¬ ∃ 𝑛 ∈ ℕ ( vol ‘ ( 𝐸 ‘ 𝑛 ) ) = +∞ ) → ( vol ‘ ∪ 𝑛 ∈ ℕ ( 𝐸 ‘ 𝑛 ) ) = ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) )
101 44 100 pm2.61dan ⊢ ( 𝜑 → ( vol ‘ ∪ 𝑛 ∈ ℕ ( 𝐸 ‘ 𝑛 ) ) = ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) )