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 ( ( ∀ 𝑛 ∈ ℕ 𝐴 ∈ dom vol ∧ Disj 𝑛 ∈ ℕ 𝐴 ) → ( vol ‘ ∪ 𝑛 ∈ ℕ 𝐴 ) = Σ* 𝑛 ∈ ℕ ( vol ‘ 𝐴 ) )

Proof

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