Metamath Proof Explorer

Theorem voliune

Description: The Lebesgue measure function is countably additive. This formulation on the extended reals, allows for +oo for the measure of any set in the sum. Cf. ovoliun and voliun . (Contributed by Thierry Arnoux, 16-Oct-2017)

Ref Expression
Assertion voliune ⊢ ∀ n ∈ ℕ A ∈ dom ⁡ vol ∧ Disj n ∈ ℕ A → vol ⁡ ⋃ n ∈ ℕ A = ∑ * n ∈ ℕ vol ⁡ A

Proof

Step Hyp Ref Expression
1 r19.26 ⊢ ∀ n ∈ ℕ A ∈ dom ⁡ vol ∧ vol ⁡ A ∈ ℝ ↔ ∀ n ∈ ℕ A ∈ dom ⁡ vol ∧ ∀ n ∈ ℕ vol ⁡ A ∈ ℝ
2 eqid ⊢ seq 1 + n ∈ ℕ ⟼ vol ⁡ A = seq 1 + n ∈ ℕ ⟼ vol ⁡ A
3 eqid ⊢ n ∈ ℕ ⟼ vol ⁡ A = n ∈ ℕ ⟼ vol ⁡ A
4 2 3 voliun ⊢ ∀ n ∈ ℕ A ∈ dom ⁡ vol ∧ vol ⁡ A ∈ ℝ ∧ Disj n ∈ ℕ A → vol ⁡ ⋃ n ∈ ℕ A = sup ran ⁡ seq 1 + n ∈ ℕ ⟼ vol ⁡ A ℝ * <
5 1 4 sylanbr ⊢ ∀ n ∈ ℕ A ∈ dom ⁡ vol ∧ ∀ n ∈ ℕ vol ⁡ A ∈ ℝ ∧ Disj n ∈ ℕ A → vol ⁡ ⋃ n ∈ ℕ A = sup ran ⁡ seq 1 + n ∈ ℕ ⟼ vol ⁡ A ℝ * <
6 5 an32s ⊢ ∀ n ∈ ℕ A ∈ dom ⁡ vol ∧ Disj n ∈ ℕ A ∧ ∀ n ∈ ℕ vol ⁡ A ∈ ℝ → vol ⁡ ⋃ n ∈ ℕ A = sup ran ⁡ seq 1 + n ∈ ℕ ⟼ vol ⁡ A ℝ * <
7 nfra1 ⊢ Ⅎ n ∀ n ∈ ℕ A ∈ dom ⁡ vol
8 nfra1 ⊢ Ⅎ n ∀ n ∈ ℕ vol ⁡ A ∈ ℝ
9 7 8 nfan ⊢ Ⅎ n ∀ n ∈ ℕ A ∈ dom ⁡ vol ∧ ∀ n ∈ ℕ vol ⁡ A ∈ ℝ
10 simpr ⊢ ∀ n ∈ ℕ A ∈ dom ⁡ vol ∧ n ∈ ℕ → n ∈ ℕ
11 rspa ⊢ ∀ n ∈ ℕ A ∈ dom ⁡ vol ∧ n ∈ ℕ → A ∈ dom ⁡ vol
12 volf ⊢ vol : dom ⁡ vol ⟶ 0 +∞
13 12 ffvelrni ⊢ A ∈ dom ⁡ vol → vol ⁡ A ∈ 0 +∞
14 11 13 syl ⊢ ∀ n ∈ ℕ A ∈ dom ⁡ vol ∧ n ∈ ℕ → vol ⁡ A ∈ 0 +∞
15 3 fvmpt2 ⊢ n ∈ ℕ ∧ vol ⁡ A ∈ 0 +∞ → n ∈ ℕ ⟼ vol ⁡ A ⁡ n = vol ⁡ A
16 10 14 15 syl2anc ⊢ ∀ n ∈ ℕ A ∈ dom ⁡ vol ∧ n ∈ ℕ → n ∈ ℕ ⟼ vol ⁡ A ⁡ n = vol ⁡ A
17 16 adantlr ⊢ ∀ n ∈ ℕ A ∈ dom ⁡ vol ∧ ∀ n ∈ ℕ vol ⁡ A ∈ ℝ ∧ n ∈ ℕ → n ∈ ℕ ⟼ vol ⁡ A ⁡ n = vol ⁡ A
18 17 ex ⊢ ∀ n ∈ ℕ A ∈ dom ⁡ vol ∧ ∀ n ∈ ℕ vol ⁡ A ∈ ℝ → n ∈ ℕ → n ∈ ℕ ⟼ vol ⁡ A ⁡ n = vol ⁡ A
19 9 18 ralrimi ⊢ ∀ n ∈ ℕ A ∈ dom ⁡ vol ∧ ∀ n ∈ ℕ vol ⁡ A ∈ ℝ → ∀ n ∈ ℕ n ∈ ℕ ⟼ vol ⁡ A ⁡ n = vol ⁡ A
20 9 19 esumeq2d ⊢ ∀ n ∈ ℕ A ∈ dom ⁡ vol ∧ ∀ n ∈ ℕ vol ⁡ A ∈ ℝ → ∑ * n ∈ ℕ n ∈ ℕ ⟼ vol ⁡ A ⁡ n = ∑ * n ∈ ℕ vol ⁡ A
21 simpr ⊢ ∀ n ∈ ℕ A ∈ dom ⁡ vol ∧ ∀ n ∈ ℕ vol ⁡ A ∈ ℝ → ∀ n ∈ ℕ vol ⁡ A ∈ ℝ
22 21 r19.21bi ⊢ ∀ n ∈ ℕ A ∈ dom ⁡ vol ∧ ∀ n ∈ ℕ vol ⁡ A ∈ ℝ ∧ n ∈ ℕ → vol ⁡ A ∈ ℝ
23 14 adantlr ⊢ ∀ n ∈ ℕ A ∈ dom ⁡ vol ∧ ∀ n ∈ ℕ vol ⁡ A ∈ ℝ ∧ n ∈ ℕ → vol ⁡ A ∈ 0 +∞
24 0xr ⊢ 0 ∈ ℝ *
25 pnfxr ⊢ +∞ ∈ ℝ *
26 elicc1 ⊢ 0 ∈ ℝ * ∧ +∞ ∈ ℝ * → vol ⁡ A ∈ 0 +∞ ↔ vol ⁡ A ∈ ℝ * ∧ 0 ≤ vol ⁡ A ∧ vol ⁡ A ≤ +∞
27 24 25 26 mp2an ⊢ vol ⁡ A ∈ 0 +∞ ↔ vol ⁡ A ∈ ℝ * ∧ 0 ≤ vol ⁡ A ∧ vol ⁡ A ≤ +∞
28 27 simp2bi ⊢ vol ⁡ A ∈ 0 +∞ → 0 ≤ vol ⁡ A
29 23 28 syl ⊢ ∀ n ∈ ℕ A ∈ dom ⁡ vol ∧ ∀ n ∈ ℕ vol ⁡ A ∈ ℝ ∧ n ∈ ℕ → 0 ≤ vol ⁡ A
30 ltpnf ⊢ vol ⁡ A ∈ ℝ → vol ⁡ A < +∞
31 22 30 syl ⊢ ∀ n ∈ ℕ A ∈ dom ⁡ vol ∧ ∀ n ∈ ℕ vol ⁡ A ∈ ℝ ∧ n ∈ ℕ → vol ⁡ A < +∞
32 0re ⊢ 0 ∈ ℝ
33 elico2 ⊢ 0 ∈ ℝ ∧ +∞ ∈ ℝ * → vol ⁡ A ∈ 0 +∞ ↔ vol ⁡ A ∈ ℝ ∧ 0 ≤ vol ⁡ A ∧ vol ⁡ A < +∞
34 32 25 33 mp2an ⊢ vol ⁡ A ∈ 0 +∞ ↔ vol ⁡ A ∈ ℝ ∧ 0 ≤ vol ⁡ A ∧ vol ⁡ A < +∞
35 22 29 31 34 syl3anbrc ⊢ ∀ n ∈ ℕ A ∈ dom ⁡ vol ∧ ∀ n ∈ ℕ vol ⁡ A ∈ ℝ ∧ n ∈ ℕ → vol ⁡ A ∈ 0 +∞
36 9 35 3 fmptdf ⊢ ∀ n ∈ ℕ A ∈ dom ⁡ vol ∧ ∀ n ∈ ℕ vol ⁡ A ∈ ℝ → n ∈ ℕ ⟼ vol ⁡ A : ℕ ⟶ 0 +∞
37 nfmpt1 ⊢ Ⅎ _ n n ∈ ℕ ⟼ vol ⁡ A
38 37 esumfsupre ⊢ n ∈ ℕ ⟼ vol ⁡ A : ℕ ⟶ 0 +∞ → ∑ * n ∈ ℕ n ∈ ℕ ⟼ vol ⁡ A ⁡ n = sup ran ⁡ seq 1 + n ∈ ℕ ⟼ vol ⁡ A ℝ * <
39 36 38 syl ⊢ ∀ n ∈ ℕ A ∈ dom ⁡ vol ∧ ∀ n ∈ ℕ vol ⁡ A ∈ ℝ → ∑ * n ∈ ℕ n ∈ ℕ ⟼ vol ⁡ A ⁡ n = sup ran ⁡ seq 1 + n ∈ ℕ ⟼ vol ⁡ A ℝ * <
40 20 39 eqtr3d ⊢ ∀ n ∈ ℕ A ∈ dom ⁡ vol ∧ ∀ n ∈ ℕ vol ⁡ A ∈ ℝ → ∑ * n ∈ ℕ vol ⁡ A = sup ran ⁡ seq 1 + n ∈ ℕ ⟼ vol ⁡ A ℝ * <
41 40 adantlr ⊢ ∀ n ∈ ℕ A ∈ dom ⁡ vol ∧ Disj n ∈ ℕ A ∧ ∀ n ∈ ℕ vol ⁡ A ∈ ℝ → ∑ * n ∈ ℕ vol ⁡ A = sup ran ⁡ seq 1 + n ∈ ℕ ⟼ vol ⁡ A ℝ * <
42 6 41 eqtr4d ⊢ ∀ n ∈ ℕ A ∈ dom ⁡ vol ∧ Disj n ∈ ℕ A ∧ ∀ n ∈ ℕ vol ⁡ A ∈ ℝ → vol ⁡ ⋃ n ∈ ℕ A = ∑ * n ∈ ℕ vol ⁡ A
43 simpr ⊢ ∀ n ∈ ℕ A ∈ dom ⁡ vol ∧ Disj n ∈ ℕ A ∧ ∃ n ∈ ℕ vol ⁡ A = +∞ → ∃ n ∈ ℕ vol ⁡ A = +∞
44 nfv ⊢ Ⅎ k vol ⁡ A = +∞
45 nfcv ⊢ Ⅎ _ n vol
46 nfcsb1v ⊢ Ⅎ _ n ⦋ k / n⦌ A
47 45 46 nffv ⊢ Ⅎ _ n vol ⁡ ⦋ k / n⦌ A
48 47 nfeq1 ⊢ Ⅎ n vol ⁡ ⦋ k / n⦌ A = +∞
49 csbeq1a ⊢ n = k → A = ⦋ k / n⦌ A
50 49 fveqeq2d ⊢ n = k → vol ⁡ A = +∞ ↔ vol ⁡ ⦋ k / n⦌ A = +∞
51 44 48 50 cbvrexw ⊢ ∃ n ∈ ℕ vol ⁡ A = +∞ ↔ ∃ k ∈ ℕ vol ⁡ ⦋ k / n⦌ A = +∞
52 43 51 sylib ⊢ ∀ n ∈ ℕ A ∈ dom ⁡ vol ∧ Disj n ∈ ℕ A ∧ ∃ n ∈ ℕ vol ⁡ A = +∞ → ∃ k ∈ ℕ vol ⁡ ⦋ k / n⦌ A = +∞
53 46 nfel1 ⊢ Ⅎ n ⦋ k / n⦌ A ∈ dom ⁡ vol
54 49 eleq1d ⊢ n = k → A ∈ dom ⁡ vol ↔ ⦋ k / n⦌ A ∈ dom ⁡ vol
55 53 54 rspc ⊢ k ∈ ℕ → ∀ n ∈ ℕ A ∈ dom ⁡ vol → ⦋ k / n⦌ A ∈ dom ⁡ vol
56 55 impcom ⊢ ∀ n ∈ ℕ A ∈ dom ⁡ vol ∧ k ∈ ℕ → ⦋ k / n⦌ A ∈ dom ⁡ vol
57 iunmbl ⊢ ∀ n ∈ ℕ A ∈ dom ⁡ vol → ⋃ n ∈ ℕ A ∈ dom ⁡ vol
58 57 adantr ⊢ ∀ n ∈ ℕ A ∈ dom ⁡ vol ∧ k ∈ ℕ → ⋃ n ∈ ℕ A ∈ dom ⁡ vol
59 nfcv ⊢ Ⅎ _ n ℕ
60 nfcv ⊢ Ⅎ _ n k
61 59 60 46 49 ssiun2sf ⊢ k ∈ ℕ → ⦋ k / n⦌ A ⊆ ⋃ n ∈ ℕ A
62 61 adantl ⊢ ∀ n ∈ ℕ A ∈ dom ⁡ vol ∧ k ∈ ℕ → ⦋ k / n⦌ A ⊆ ⋃ n ∈ ℕ A
63 volss ⊢ ⦋ k / n⦌ A ∈ dom ⁡ vol ∧ ⋃ n ∈ ℕ A ∈ dom ⁡ vol ∧ ⦋ k / n⦌ A ⊆ ⋃ n ∈ ℕ A → vol ⁡ ⦋ k / n⦌ A ≤ vol ⁡ ⋃ n ∈ ℕ A
64 56 58 62 63 syl3anc ⊢ ∀ n ∈ ℕ A ∈ dom ⁡ vol ∧ k ∈ ℕ → vol ⁡ ⦋ k / n⦌ A ≤ vol ⁡ ⋃ n ∈ ℕ A
65 64 adantlr ⊢ ∀ n ∈ ℕ A ∈ dom ⁡ vol ∧ Disj n ∈ ℕ A ∧ k ∈ ℕ → vol ⁡ ⦋ k / n⦌ A ≤ vol ⁡ ⋃ n ∈ ℕ A
66 65 adantlr ⊢ ∀ n ∈ ℕ A ∈ dom ⁡ vol ∧ Disj n ∈ ℕ A ∧ ∃ n ∈ ℕ vol ⁡ A = +∞ ∧ k ∈ ℕ → vol ⁡ ⦋ k / n⦌ A ≤ vol ⁡ ⋃ n ∈ ℕ A
67 66 ralrimiva ⊢ ∀ n ∈ ℕ A ∈ dom ⁡ vol ∧ Disj n ∈ ℕ A ∧ ∃ n ∈ ℕ vol ⁡ A = +∞ → ∀ k ∈ ℕ vol ⁡ ⦋ k / n⦌ A ≤ vol ⁡ ⋃ n ∈ ℕ A
68 r19.29r ⊢ ∃ k ∈ ℕ vol ⁡ ⦋ k / n⦌ A = +∞ ∧ ∀ k ∈ ℕ vol ⁡ ⦋ k / n⦌ A ≤ vol ⁡ ⋃ n ∈ ℕ A → ∃ k ∈ ℕ vol ⁡ ⦋ k / n⦌ A = +∞ ∧ vol ⁡ ⦋ k / n⦌ A ≤ vol ⁡ ⋃ n ∈ ℕ A
69 52 67 68 syl2anc ⊢ ∀ n ∈ ℕ A ∈ dom ⁡ vol ∧ Disj n ∈ ℕ A ∧ ∃ n ∈ ℕ vol ⁡ A = +∞ → ∃ k ∈ ℕ vol ⁡ ⦋ k / n⦌ A = +∞ ∧ vol ⁡ ⦋ k / n⦌ A ≤ vol ⁡ ⋃ n ∈ ℕ A
70 breq1 ⊢ vol ⁡ ⦋ k / n⦌ A = +∞ → vol ⁡ ⦋ k / n⦌ A ≤ vol ⁡ ⋃ n ∈ ℕ A ↔ +∞ ≤ vol ⁡ ⋃ n ∈ ℕ A
71 70 biimpa ⊢ vol ⁡ ⦋ k / n⦌ A = +∞ ∧ vol ⁡ ⦋ k / n⦌ A ≤ vol ⁡ ⋃ n ∈ ℕ A → +∞ ≤ vol ⁡ ⋃ n ∈ ℕ A
72 71 reximi ⊢ ∃ k ∈ ℕ vol ⁡ ⦋ k / n⦌ A = +∞ ∧ vol ⁡ ⦋ k / n⦌ A ≤ vol ⁡ ⋃ n ∈ ℕ A → ∃ k ∈ ℕ +∞ ≤ vol ⁡ ⋃ n ∈ ℕ A
73 69 72 syl ⊢ ∀ n ∈ ℕ A ∈ dom ⁡ vol ∧ Disj n ∈ ℕ A ∧ ∃ n ∈ ℕ vol ⁡ A = +∞ → ∃ k ∈ ℕ +∞ ≤ vol ⁡ ⋃ n ∈ ℕ A
74 1nn ⊢ 1 ∈ ℕ
75 ne0i ⊢ 1 ∈ ℕ → ℕ ≠ ∅
76 r19.9rzv ⊢ ℕ ≠ ∅ → +∞ ≤ vol ⁡ ⋃ n ∈ ℕ A ↔ ∃ k ∈ ℕ +∞ ≤ vol ⁡ ⋃ n ∈ ℕ A
77 74 75 76 mp2b ⊢ +∞ ≤ vol ⁡ ⋃ n ∈ ℕ A ↔ ∃ k ∈ ℕ +∞ ≤ vol ⁡ ⋃ n ∈ ℕ A
78 73 77 sylibr ⊢ ∀ n ∈ ℕ A ∈ dom ⁡ vol ∧ Disj n ∈ ℕ A ∧ ∃ n ∈ ℕ vol ⁡ A = +∞ → +∞ ≤ vol ⁡ ⋃ n ∈ ℕ A
79 iccssxr ⊢ 0 +∞ ⊆ ℝ *
80 12 ffvelrni ⊢ ⋃ n ∈ ℕ A ∈ dom ⁡ vol → vol ⁡ ⋃ n ∈ ℕ A ∈ 0 +∞
81 79 80 sselid ⊢ ⋃ n ∈ ℕ A ∈ dom ⁡ vol → vol ⁡ ⋃ n ∈ ℕ A ∈ ℝ *
82 57 81 syl ⊢ ∀ n ∈ ℕ A ∈ dom ⁡ vol → vol ⁡ ⋃ n ∈ ℕ A ∈ ℝ *
83 82 ad2antrr ⊢ ∀ n ∈ ℕ A ∈ dom ⁡ vol ∧ Disj n ∈ ℕ A ∧ ∃ n ∈ ℕ vol ⁡ A = +∞ → vol ⁡ ⋃ n ∈ ℕ A ∈ ℝ *
84 xgepnf ⊢ vol ⁡ ⋃ n ∈ ℕ A ∈ ℝ * → +∞ ≤ vol ⁡ ⋃ n ∈ ℕ A ↔ vol ⁡ ⋃ n ∈ ℕ A = +∞
85 83 84 syl ⊢ ∀ n ∈ ℕ A ∈ dom ⁡ vol ∧ Disj n ∈ ℕ A ∧ ∃ n ∈ ℕ vol ⁡ A = +∞ → +∞ ≤ vol ⁡ ⋃ n ∈ ℕ A ↔ vol ⁡ ⋃ n ∈ ℕ A = +∞
86 78 85 mpbid ⊢ ∀ n ∈ ℕ A ∈ dom ⁡ vol ∧ Disj n ∈ ℕ A ∧ ∃ n ∈ ℕ vol ⁡ A = +∞ → vol ⁡ ⋃ n ∈ ℕ A = +∞
87 nfdisj1 ⊢ Ⅎ n Disj n ∈ ℕ A
88 7 87 nfan ⊢ Ⅎ n ∀ n ∈ ℕ A ∈ dom ⁡ vol ∧ Disj n ∈ ℕ A
89 nfre1 ⊢ Ⅎ n ∃ n ∈ ℕ vol ⁡ A = +∞
90 88 89 nfan ⊢ Ⅎ n ∀ n ∈ ℕ A ∈ dom ⁡ vol ∧ Disj n ∈ ℕ A ∧ ∃ n ∈ ℕ vol ⁡ A = +∞
91 nnex ⊢ ℕ ∈ V
92 91 a1i ⊢ ∀ n ∈ ℕ A ∈ dom ⁡ vol ∧ Disj n ∈ ℕ A ∧ ∃ n ∈ ℕ vol ⁡ A = +∞ → ℕ ∈ V
93 14 3ad2antr3 ⊢ ∀ n ∈ ℕ A ∈ dom ⁡ vol ∧ Disj n ∈ ℕ A ∧ ∃ n ∈ ℕ vol ⁡ A = +∞ ∧ n ∈ ℕ → vol ⁡ A ∈ 0 +∞
94 93 3anassrs ⊢ ∀ n ∈ ℕ A ∈ dom ⁡ vol ∧ Disj n ∈ ℕ A ∧ ∃ n ∈ ℕ vol ⁡ A = +∞ ∧ n ∈ ℕ → vol ⁡ A ∈ 0 +∞
95 90 92 94 43 esumpinfval ⊢ ∀ n ∈ ℕ A ∈ dom ⁡ vol ∧ Disj n ∈ ℕ A ∧ ∃ n ∈ ℕ vol ⁡ A = +∞ → ∑ * n ∈ ℕ vol ⁡ A = +∞
96 86 95 eqtr4d ⊢ ∀ n ∈ ℕ A ∈ dom ⁡ vol ∧ Disj n ∈ ℕ A ∧ ∃ n ∈ ℕ vol ⁡ A = +∞ → vol ⁡ ⋃ n ∈ ℕ A = ∑ * n ∈ ℕ vol ⁡ A
97 exmid ⊢ ∀ n ∈ ℕ vol ⁡ A ∈ ℝ ∨ ¬ ∀ n ∈ ℕ vol ⁡ A ∈ ℝ
98 rexnal ⊢ ∃ n ∈ ℕ ¬ vol ⁡ A ∈ ℝ ↔ ¬ ∀ n ∈ ℕ vol ⁡ A ∈ ℝ
99 98 orbi2i ⊢ ∀ n ∈ ℕ vol ⁡ A ∈ ℝ ∨ ∃ n ∈ ℕ ¬ vol ⁡ A ∈ ℝ ↔ ∀ n ∈ ℕ vol ⁡ A ∈ ℝ ∨ ¬ ∀ n ∈ ℕ vol ⁡ A ∈ ℝ
100 97 99 mpbir ⊢ ∀ n ∈ ℕ vol ⁡ A ∈ ℝ ∨ ∃ n ∈ ℕ ¬ vol ⁡ A ∈ ℝ
101 r19.29 ⊢ ∀ n ∈ ℕ A ∈ dom ⁡ vol ∧ ∃ n ∈ ℕ ¬ vol ⁡ A ∈ ℝ → ∃ n ∈ ℕ A ∈ dom ⁡ vol ∧ ¬ vol ⁡ A ∈ ℝ
102 xrge0nre ⊢ vol ⁡ A ∈ 0 +∞ ∧ ¬ vol ⁡ A ∈ ℝ → vol ⁡ A = +∞
103 13 102 sylan ⊢ A ∈ dom ⁡ vol ∧ ¬ vol ⁡ A ∈ ℝ → vol ⁡ A = +∞
104 103 reximi ⊢ ∃ n ∈ ℕ A ∈ dom ⁡ vol ∧ ¬ vol ⁡ A ∈ ℝ → ∃ n ∈ ℕ vol ⁡ A = +∞
105 101 104 syl ⊢ ∀ n ∈ ℕ A ∈ dom ⁡ vol ∧ ∃ n ∈ ℕ ¬ vol ⁡ A ∈ ℝ → ∃ n ∈ ℕ vol ⁡ A = +∞
106 105 ex ⊢ ∀ n ∈ ℕ A ∈ dom ⁡ vol → ∃ n ∈ ℕ ¬ vol ⁡ A ∈ ℝ → ∃ n ∈ ℕ vol ⁡ A = +∞
107 106 orim2d ⊢ ∀ n ∈ ℕ A ∈ dom ⁡ vol → ∀ n ∈ ℕ vol ⁡ A ∈ ℝ ∨ ∃ n ∈ ℕ ¬ vol ⁡ A ∈ ℝ → ∀ n ∈ ℕ vol ⁡ A ∈ ℝ ∨ ∃ n ∈ ℕ vol ⁡ A = +∞
108 100 107 mpi ⊢ ∀ n ∈ ℕ A ∈ dom ⁡ vol → ∀ n ∈ ℕ vol ⁡ A ∈ ℝ ∨ ∃ n ∈ ℕ vol ⁡ A = +∞
109 108 adantr ⊢ ∀ n ∈ ℕ A ∈ dom ⁡ vol ∧ Disj n ∈ ℕ A → ∀ n ∈ ℕ vol ⁡ A ∈ ℝ ∨ ∃ n ∈ ℕ vol ⁡ A = +∞
110 42 96 109 mpjaodan ⊢ ∀ n ∈ ℕ A ∈ dom ⁡ vol ∧ Disj n ∈ ℕ A → vol ⁡ ⋃ n ∈ ℕ A = ∑ * n ∈ ℕ vol ⁡ A