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∧Disjn∈ℕ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 ⊢seq1+n∈ℕ⟼vol⁡A=seq1+n∈ℕ⟼vol⁡A
3 eqid ⊢n∈ℕ⟼vol⁡A=n∈ℕ⟼vol⁡A
4 2 3 voliun ⊢∀n∈ℕA∈dom⁡vol∧vol⁡A∈ℝ∧Disjn∈ℕA→vol⁡⋃n∈ℕA=supran⁡seq1+n∈ℕ⟼vol⁡Aℝ*<
5 1 4 sylanbr ⊢∀n∈ℕA∈dom⁡vol∧∀n∈ℕvol⁡A∈ℝ∧Disjn∈ℕA→vol⁡⋃n∈ℕA=supran⁡seq1+n∈ℕ⟼vol⁡Aℝ*<
6 5 an32s ⊢∀n∈ℕA∈dom⁡vol∧Disjn∈ℕA∧∀n∈ℕvol⁡A∈ℝ→vol⁡⋃n∈ℕA=supran⁡seq1+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 ffvelcdmi ⊢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 ⊢Ⅎ_nn∈ℕ⟼vol⁡A
38 37 esumfsupre ⊢n∈ℕ⟼vol⁡A:ℕ⟶0+∞→∑*n∈ℕn∈ℕ⟼vol⁡A⁡n=supran⁡seq1+n∈ℕ⟼vol⁡Aℝ*<
39 36 38 syl ⊢∀n∈ℕA∈dom⁡vol∧∀n∈ℕvol⁡A∈ℝ→∑*n∈ℕn∈ℕ⟼vol⁡A⁡n=supran⁡seq1+n∈ℕ⟼vol⁡Aℝ*<
40 20 39 eqtr3d ⊢∀n∈ℕA∈dom⁡vol∧∀n∈ℕvol⁡A∈ℝ→∑*n∈ℕvol⁡A=supran⁡seq1+n∈ℕ⟼vol⁡Aℝ*<
41 40 adantlr ⊢∀n∈ℕA∈dom⁡vol∧Disjn∈ℕA∧∀n∈ℕvol⁡A∈ℝ→∑*n∈ℕvol⁡A=supran⁡seq1+n∈ℕ⟼vol⁡Aℝ*<
42 6 41 eqtr4d ⊢∀n∈ℕA∈dom⁡vol∧Disjn∈ℕA∧∀n∈ℕvol⁡A∈ℝ→vol⁡⋃n∈ℕA=∑*n∈ℕvol⁡A
43 simpr ⊢∀n∈ℕA∈dom⁡vol∧Disjn∈ℕA∧∃n∈ℕvol⁡A=+∞→∃n∈ℕvol⁡A=+∞
44 nfv ⊢Ⅎkvol⁡A=+∞
45 nfcv ⊢Ⅎ_nvol
46 nfcsb1v ⊢Ⅎ_n⦋k/n⦌A
47 45 46 nffv ⊢Ⅎ_nvol⁡⦋k/n⦌A
48 47 nfeq1 ⊢Ⅎnvol⁡⦋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∧Disjn∈ℕ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 ⊢Ⅎ_nk
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∧Disjn∈ℕA∧k∈ℕ→vol⁡⦋k/n⦌A≤vol⁡⋃n∈ℕA
66 65 adantlr ⊢∀n∈ℕA∈dom⁡vol∧Disjn∈ℕA∧∃n∈ℕvol⁡A=+∞∧k∈ℕ→vol⁡⦋k/n⦌A≤vol⁡⋃n∈ℕA
67 66 ralrimiva ⊢∀n∈ℕA∈dom⁡vol∧Disjn∈ℕ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∧Disjn∈ℕ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∧Disjn∈ℕ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∧Disjn∈ℕA∧∃n∈ℕvol⁡A=+∞→+∞≤vol⁡⋃n∈ℕA
79 iccssxr ⊢0+∞⊆ℝ*
80 12 ffvelcdmi ⊢⋃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∧Disjn∈ℕ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∧Disjn∈ℕA∧∃n∈ℕvol⁡A=+∞→+∞≤vol⁡⋃n∈ℕA↔vol⁡⋃n∈ℕA=+∞
86 78 85 mpbid ⊢∀n∈ℕA∈dom⁡vol∧Disjn∈ℕA∧∃n∈ℕvol⁡A=+∞→vol⁡⋃n∈ℕA=+∞
87 nfdisj1 ⊢ℲnDisjn∈ℕA
88 7 87 nfan ⊢Ⅎn∀n∈ℕA∈dom⁡vol∧Disjn∈ℕA
89 nfre1 ⊢Ⅎn∃n∈ℕvol⁡A=+∞
90 88 89 nfan ⊢Ⅎn∀n∈ℕA∈dom⁡vol∧Disjn∈ℕA∧∃n∈ℕvol⁡A=+∞
91 nnex ⊢ℕ∈V
92 91 a1i ⊢∀n∈ℕA∈dom⁡vol∧Disjn∈ℕA∧∃n∈ℕvol⁡A=+∞→ℕ∈V
93 14 3ad2antr3 ⊢∀n∈ℕA∈dom⁡vol∧Disjn∈ℕA∧∃n∈ℕvol⁡A=+∞∧n∈ℕ→vol⁡A∈0+∞
94 93 3anassrs ⊢∀n∈ℕA∈dom⁡vol∧Disjn∈ℕA∧∃n∈ℕvol⁡A=+∞∧n∈ℕ→vol⁡A∈0+∞
95 90 92 94 43 esumpinfval ⊢∀n∈ℕA∈dom⁡vol∧Disjn∈ℕA∧∃n∈ℕvol⁡A=+∞→∑*n∈ℕvol⁡A=+∞
96 86 95 eqtr4d ⊢∀n∈ℕA∈dom⁡vol∧Disjn∈ℕ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∧Disjn∈ℕA→∀n∈ℕvol⁡A∈ℝ∨∃n∈ℕvol⁡A=+∞
110 42 96 109 mpjaodan ⊢∀n∈ℕA∈dom⁡vol∧Disjn∈ℕA→vol⁡⋃n∈ℕA=∑*n∈ℕvol⁡A