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 simpr ⊢ ( ( ( ∀ 𝑛 ∈ ℕ 𝐴 ∈ dom vol ∧ Disj 𝑛 ∈ ℕ 𝐴 ) ∧ ∃ 𝑛 ∈ ℕ ( vol ‘ 𝐴 ) = +∞ ) → ∃ 𝑛 ∈ ℕ ( vol ‘ 𝐴 ) = +∞ )
44 nfv ⊢ Ⅎ 𝑘 ( vol ‘ 𝐴 ) = +∞
45 nfcv ⊢ Ⅎ 𝑛 vol
46 nfcsb1v ⊢ Ⅎ 𝑛 ⦋ 𝑘 / 𝑛 ⦌ 𝐴
47 45 46 nffv ⊢ Ⅎ 𝑛 ( vol ‘ ⦋ 𝑘 / 𝑛 ⦌ 𝐴 )
48 47 nfeq1 ⊢ Ⅎ 𝑛 ( vol ‘ ⦋ 𝑘 / 𝑛 ⦌ 𝐴 ) = +∞
49 csbeq1a ⊢ ( 𝑛 = 𝑘 → 𝐴 = ⦋ 𝑘 / 𝑛 ⦌ 𝐴 )
50 49 fveqeq2d ⊢ ( 𝑛 = 𝑘 → ( ( vol ‘ 𝐴 ) = +∞ ↔ ( vol ‘ ⦋ 𝑘 / 𝑛 ⦌ 𝐴 ) = +∞ ) )
51 44 48 50 cbvrexw ⊢ ( ∃ 𝑛 ∈ ℕ ( vol ‘ 𝐴 ) = +∞ ↔ ∃ 𝑘 ∈ ℕ ( vol ‘ ⦋ 𝑘 / 𝑛 ⦌ 𝐴 ) = +∞ )
52 43 51 sylib ⊢ ( ( ( ∀ 𝑛 ∈ ℕ 𝐴 ∈ dom vol ∧ Disj 𝑛 ∈ ℕ 𝐴 ) ∧ ∃ 𝑛 ∈ ℕ ( vol ‘ 𝐴 ) = +∞ ) → ∃ 𝑘 ∈ ℕ ( vol ‘ ⦋ 𝑘 / 𝑛 ⦌ 𝐴 ) = +∞ )
53 46 nfel1 ⊢ Ⅎ 𝑛 ⦋ 𝑘 / 𝑛 ⦌ 𝐴 ∈ dom vol
54 49 eleq1d ⊢ ( 𝑛 = 𝑘 → ( 𝐴 ∈ dom vol ↔ ⦋ 𝑘 / 𝑛 ⦌ 𝐴 ∈ dom vol ) )
55 53 54 rspc ⊢ ( 𝑘 ∈ ℕ → ( ∀ 𝑛 ∈ ℕ 𝐴 ∈ dom vol → ⦋ 𝑘 / 𝑛 ⦌ 𝐴 ∈ dom vol ) )
56 55 impcom ⊢ ( ( ∀ 𝑛 ∈ ℕ 𝐴 ∈ dom vol ∧ 𝑘 ∈ ℕ ) → ⦋ 𝑘 / 𝑛 ⦌ 𝐴 ∈ dom vol )
57 iunmbl ⊢ ( ∀ 𝑛 ∈ ℕ 𝐴 ∈ dom vol → ∪ 𝑛 ∈ ℕ 𝐴 ∈ dom vol )
58 57 adantr ⊢ ( ( ∀ 𝑛 ∈ ℕ 𝐴 ∈ dom vol ∧ 𝑘 ∈ ℕ ) → ∪ 𝑛 ∈ ℕ 𝐴 ∈ dom vol )
59 nfcv ⊢ Ⅎ 𝑛 ℕ
60 nfcv ⊢ Ⅎ 𝑛 𝑘
61 59 60 46 49 ssiun2sf ⊢ ( 𝑘 ∈ ℕ → ⦋ 𝑘 / 𝑛 ⦌ 𝐴 ⊆ ∪ 𝑛 ∈ ℕ 𝐴 )
62 61 adantl ⊢ ( ( ∀ 𝑛 ∈ ℕ 𝐴 ∈ dom vol ∧ 𝑘 ∈ ℕ ) → ⦋ 𝑘 / 𝑛 ⦌ 𝐴 ⊆ ∪ 𝑛 ∈ ℕ 𝐴 )
63 volss ⊢ ( ( ⦋ 𝑘 / 𝑛 ⦌ 𝐴 ∈ dom vol ∧ ∪ 𝑛 ∈ ℕ 𝐴 ∈ dom vol ∧ ⦋ 𝑘 / 𝑛 ⦌ 𝐴 ⊆ ∪ 𝑛 ∈ ℕ 𝐴 ) → ( vol ‘ ⦋ 𝑘 / 𝑛 ⦌ 𝐴 ) ≤ ( vol ‘ ∪ 𝑛 ∈ ℕ 𝐴 ) )
64 56 58 62 63 syl3anc ⊢ ( ( ∀ 𝑛 ∈ ℕ 𝐴 ∈ dom vol ∧ 𝑘 ∈ ℕ ) → ( vol ‘ ⦋ 𝑘 / 𝑛 ⦌ 𝐴 ) ≤ ( vol ‘ ∪ 𝑛 ∈ ℕ 𝐴 ) )
65 64 adantlr ⊢ ( ( ( ∀ 𝑛 ∈ ℕ 𝐴 ∈ dom vol ∧ Disj 𝑛 ∈ ℕ 𝐴 ) ∧ 𝑘 ∈ ℕ ) → ( vol ‘ ⦋ 𝑘 / 𝑛 ⦌ 𝐴 ) ≤ ( vol ‘ ∪ 𝑛 ∈ ℕ 𝐴 ) )
66 65 adantlr ⊢ ( ( ( ( ∀ 𝑛 ∈ ℕ 𝐴 ∈ dom vol ∧ Disj 𝑛 ∈ ℕ 𝐴 ) ∧ ∃ 𝑛 ∈ ℕ ( vol ‘ 𝐴 ) = +∞ ) ∧ 𝑘 ∈ ℕ ) → ( vol ‘ ⦋ 𝑘 / 𝑛 ⦌ 𝐴 ) ≤ ( vol ‘ ∪ 𝑛 ∈ ℕ 𝐴 ) )
67 66 ralrimiva ⊢ ( ( ( ∀ 𝑛 ∈ ℕ 𝐴 ∈ dom vol ∧ Disj 𝑛 ∈ ℕ 𝐴 ) ∧ ∃ 𝑛 ∈ ℕ ( vol ‘ 𝐴 ) = +∞ ) → ∀ 𝑘 ∈ ℕ ( vol ‘ ⦋ 𝑘 / 𝑛 ⦌ 𝐴 ) ≤ ( vol ‘ ∪ 𝑛 ∈ ℕ 𝐴 ) )
68 r19.29r ⊢ ( ( ∃ 𝑘 ∈ ℕ ( vol ‘ ⦋ 𝑘 / 𝑛 ⦌ 𝐴 ) = +∞ ∧ ∀ 𝑘 ∈ ℕ ( vol ‘ ⦋ 𝑘 / 𝑛 ⦌ 𝐴 ) ≤ ( vol ‘ ∪ 𝑛 ∈ ℕ 𝐴 ) ) → ∃ 𝑘 ∈ ℕ ( ( vol ‘ ⦋ 𝑘 / 𝑛 ⦌ 𝐴 ) = +∞ ∧ ( vol ‘ ⦋ 𝑘 / 𝑛 ⦌ 𝐴 ) ≤ ( vol ‘ ∪ 𝑛 ∈ ℕ 𝐴 ) ) )
69 52 67 68 syl2anc ⊢ ( ( ( ∀ 𝑛 ∈ ℕ 𝐴 ∈ dom vol ∧ Disj 𝑛 ∈ ℕ 𝐴 ) ∧ ∃ 𝑛 ∈ ℕ ( vol ‘ 𝐴 ) = +∞ ) → ∃ 𝑘 ∈ ℕ ( ( vol ‘ ⦋ 𝑘 / 𝑛 ⦌ 𝐴 ) = +∞ ∧ ( vol ‘ ⦋ 𝑘 / 𝑛 ⦌ 𝐴 ) ≤ ( vol ‘ ∪ 𝑛 ∈ ℕ 𝐴 ) ) )
70 breq1 ⊢ ( ( vol ‘ ⦋ 𝑘 / 𝑛 ⦌ 𝐴 ) = +∞ → ( ( vol ‘ ⦋ 𝑘 / 𝑛 ⦌ 𝐴 ) ≤ ( vol ‘ ∪ 𝑛 ∈ ℕ 𝐴 ) ↔ +∞ ≤ ( vol ‘ ∪ 𝑛 ∈ ℕ 𝐴 ) ) )
71 70 biimpa ⊢ ( ( ( vol ‘ ⦋ 𝑘 / 𝑛 ⦌ 𝐴 ) = +∞ ∧ ( vol ‘ ⦋ 𝑘 / 𝑛 ⦌ 𝐴 ) ≤ ( vol ‘ ∪ 𝑛 ∈ ℕ 𝐴 ) ) → +∞ ≤ ( vol ‘ ∪ 𝑛 ∈ ℕ 𝐴 ) )
72 71 reximi ⊢ ( ∃ 𝑘 ∈ ℕ ( ( vol ‘ ⦋ 𝑘 / 𝑛 ⦌ 𝐴 ) = +∞ ∧ ( vol ‘ ⦋ 𝑘 / 𝑛 ⦌ 𝐴 ) ≤ ( vol ‘ ∪ 𝑛 ∈ ℕ 𝐴 ) ) → ∃ 𝑘 ∈ ℕ +∞ ≤ ( vol ‘ ∪ 𝑛 ∈ ℕ 𝐴 ) )
73 69 72 syl ⊢ ( ( ( ∀ 𝑛 ∈ ℕ 𝐴 ∈ dom vol ∧ Disj 𝑛 ∈ ℕ 𝐴 ) ∧ ∃ 𝑛 ∈ ℕ ( vol ‘ 𝐴 ) = +∞ ) → ∃ 𝑘 ∈ ℕ +∞ ≤ ( vol ‘ ∪ 𝑛 ∈ ℕ 𝐴 ) )
74 1nn ⊢ 1 ∈ ℕ
75 ne0i ⊢ ( 1 ∈ ℕ → ℕ ≠ ∅ )
76 r19.9rzv ⊢ ( ℕ ≠ ∅ → ( +∞ ≤ ( vol ‘ ∪ 𝑛 ∈ ℕ 𝐴 ) ↔ ∃ 𝑘 ∈ ℕ +∞ ≤ ( vol ‘ ∪ 𝑛 ∈ ℕ 𝐴 ) ) )
77 74 75 76 mp2b ⊢ ( +∞ ≤ ( vol ‘ ∪ 𝑛 ∈ ℕ 𝐴 ) ↔ ∃ 𝑘 ∈ ℕ +∞ ≤ ( vol ‘ ∪ 𝑛 ∈ ℕ 𝐴 ) )
78 73 77 sylibr ⊢ ( ( ( ∀ 𝑛 ∈ ℕ 𝐴 ∈ dom vol ∧ Disj 𝑛 ∈ ℕ 𝐴 ) ∧ ∃ 𝑛 ∈ ℕ ( vol ‘ 𝐴 ) = +∞ ) → +∞ ≤ ( vol ‘ ∪ 𝑛 ∈ ℕ 𝐴 ) )
79 iccssxr ⊢ ( 0 [,] +∞ ) ⊆ ℝ*
80 12 ffvelcdmi ⊢ ( ∪ 𝑛 ∈ ℕ 𝐴 ∈ dom vol → ( vol ‘ ∪ 𝑛 ∈ ℕ 𝐴 ) ∈ ( 0 [,] +∞ ) )
81 79 80 sselid ⊢ ( ∪ 𝑛 ∈ ℕ 𝐴 ∈ dom vol → ( vol ‘ ∪ 𝑛 ∈ ℕ 𝐴 ) ∈ ℝ* )
82 57 81 syl ⊢ ( ∀ 𝑛 ∈ ℕ 𝐴 ∈ dom vol → ( vol ‘ ∪ 𝑛 ∈ ℕ 𝐴 ) ∈ ℝ* )
83 82 ad2antrr ⊢ ( ( ( ∀ 𝑛 ∈ ℕ 𝐴 ∈ dom vol ∧ Disj 𝑛 ∈ ℕ 𝐴 ) ∧ ∃ 𝑛 ∈ ℕ ( vol ‘ 𝐴 ) = +∞ ) → ( vol ‘ ∪ 𝑛 ∈ ℕ 𝐴 ) ∈ ℝ* )
84 xgepnf ⊢ ( ( vol ‘ ∪ 𝑛 ∈ ℕ 𝐴 ) ∈ ℝ* → ( +∞ ≤ ( vol ‘ ∪ 𝑛 ∈ ℕ 𝐴 ) ↔ ( vol ‘ ∪ 𝑛 ∈ ℕ 𝐴 ) = +∞ ) )
85 83 84 syl ⊢ ( ( ( ∀ 𝑛 ∈ ℕ 𝐴 ∈ dom vol ∧ Disj 𝑛 ∈ ℕ 𝐴 ) ∧ ∃ 𝑛 ∈ ℕ ( vol ‘ 𝐴 ) = +∞ ) → ( +∞ ≤ ( vol ‘ ∪ 𝑛 ∈ ℕ 𝐴 ) ↔ ( vol ‘ ∪ 𝑛 ∈ ℕ 𝐴 ) = +∞ ) )
86 78 85 mpbid ⊢ ( ( ( ∀ 𝑛 ∈ ℕ 𝐴 ∈ dom vol ∧ Disj 𝑛 ∈ ℕ 𝐴 ) ∧ ∃ 𝑛 ∈ ℕ ( vol ‘ 𝐴 ) = +∞ ) → ( vol ‘ ∪ 𝑛 ∈ ℕ 𝐴 ) = +∞ )
87 nfdisj1 ⊢ Ⅎ 𝑛 Disj 𝑛 ∈ ℕ 𝐴
88 7 87 nfan ⊢ Ⅎ 𝑛 ( ∀ 𝑛 ∈ ℕ 𝐴 ∈ dom vol ∧ Disj 𝑛 ∈ ℕ 𝐴 )
89 nfre1 ⊢ Ⅎ 𝑛 ∃ 𝑛 ∈ ℕ ( vol ‘ 𝐴 ) = +∞
90 88 89 nfan ⊢ Ⅎ 𝑛 ( ( ∀ 𝑛 ∈ ℕ 𝐴 ∈ dom vol ∧ Disj 𝑛 ∈ ℕ 𝐴 ) ∧ ∃ 𝑛 ∈ ℕ ( vol ‘ 𝐴 ) = +∞ )
91 nnex ⊢ ℕ ∈ V
92 91 a1i ⊢ ( ( ( ∀ 𝑛 ∈ ℕ 𝐴 ∈ dom vol ∧ Disj 𝑛 ∈ ℕ 𝐴 ) ∧ ∃ 𝑛 ∈ ℕ ( vol ‘ 𝐴 ) = +∞ ) → ℕ ∈ V )
93 14 3ad2antr3 ⊢ ( ( ∀ 𝑛 ∈ ℕ 𝐴 ∈ dom vol ∧ ( Disj 𝑛 ∈ ℕ 𝐴 ∧ ∃ 𝑛 ∈ ℕ ( vol ‘ 𝐴 ) = +∞ ∧ 𝑛 ∈ ℕ ) ) → ( vol ‘ 𝐴 ) ∈ ( 0 [,] +∞ ) )
94 93 3anassrs ⊢ ( ( ( ( ∀ 𝑛 ∈ ℕ 𝐴 ∈ dom vol ∧ Disj 𝑛 ∈ ℕ 𝐴 ) ∧ ∃ 𝑛 ∈ ℕ ( vol ‘ 𝐴 ) = +∞ ) ∧ 𝑛 ∈ ℕ ) → ( vol ‘ 𝐴 ) ∈ ( 0 [,] +∞ ) )
95 90 92 94 43 esumpinfval ⊢ ( ( ( ∀ 𝑛 ∈ ℕ 𝐴 ∈ dom vol ∧ Disj 𝑛 ∈ ℕ 𝐴 ) ∧ ∃ 𝑛 ∈ ℕ ( vol ‘ 𝐴 ) = +∞ ) → Σ* 𝑛 ∈ ℕ ( vol ‘ 𝐴 ) = +∞ )
96 86 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 ‘ 𝐴 ) )