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 sseldi ⊢ ( 𝜑 → ( 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 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) )