Metamath Proof Explorer

Theorem volmeas

Description: The Lebesgue measure is a measure. (Contributed by Thierry Arnoux, 16-Oct-2017)

Ref Expression
Assertion volmeas vol ∈ ( measures ‘ dom vol )

Proof

Step Hyp Ref Expression
1 volf ⊢ vol : dom vol ⟶ ( 0 [,] +∞ )
2 fvssunirn ⊢ ( sigAlgebra ‘ ℝ ) ⊆ ∪ ran sigAlgebra
3 dmvlsiga ⊢ dom vol ∈ ( sigAlgebra ‘ ℝ )
4 2 3 sselii ⊢ dom vol ∈ ∪ ran sigAlgebra
5 0elsiga ⊢ ( dom vol ∈ ∪ ran sigAlgebra → ∅ ∈ dom vol )
6 4 5 ax-mp ⊢ ∅ ∈ dom vol
7 mblvol ⊢ ( ∅ ∈ dom vol → ( vol ‘ ∅ ) = ( vol* ‘ ∅ ) )
8 6 7 ax-mp ⊢ ( vol ‘ ∅ ) = ( vol* ‘ ∅ )
9 ovol0 ⊢ ( vol* ‘ ∅ ) = 0
10 8 9 eqtri ⊢ ( vol ‘ ∅ ) = 0
11 simpr ⊢ ( ( ( 𝑥 ∈ 𝒫 dom vol ∧ ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ) ∧ 𝑥 ∈ Fin ) → 𝑥 ∈ Fin )
12 nfv ⊢ Ⅎ 𝑦 𝑥 ∈ 𝒫 dom vol
13 nfv ⊢ Ⅎ 𝑦 𝑥 ≼ ω
14 nfdisj1 ⊢ Ⅎ 𝑦 Disj 𝑦 ∈ 𝑥 𝑦
15 13 14 nfan ⊢ Ⅎ 𝑦 ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 )
16 12 15 nfan ⊢ Ⅎ 𝑦 ( 𝑥 ∈ 𝒫 dom vol ∧ ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) )
17 nfv ⊢ Ⅎ 𝑦 𝑥 ∈ Fin
18 16 17 nfan ⊢ Ⅎ 𝑦 ( ( 𝑥 ∈ 𝒫 dom vol ∧ ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ) ∧ 𝑥 ∈ Fin )
19 elpwi ⊢ ( 𝑥 ∈ 𝒫 dom vol → 𝑥 ⊆ dom vol )
20 19 ad3antrrr ⊢ ( ( ( ( 𝑥 ∈ 𝒫 dom vol ∧ ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ) ∧ 𝑥 ∈ Fin ) ∧ 𝑦 ∈ 𝑥 ) → 𝑥 ⊆ dom vol )
21 simpr ⊢ ( ( ( ( 𝑥 ∈ 𝒫 dom vol ∧ ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ) ∧ 𝑥 ∈ Fin ) ∧ 𝑦 ∈ 𝑥 ) → 𝑦 ∈ 𝑥 )
22 20 21 sseldd ⊢ ( ( ( ( 𝑥 ∈ 𝒫 dom vol ∧ ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ) ∧ 𝑥 ∈ Fin ) ∧ 𝑦 ∈ 𝑥 ) → 𝑦 ∈ dom vol )
23 22 ex ⊢ ( ( ( 𝑥 ∈ 𝒫 dom vol ∧ ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ) ∧ 𝑥 ∈ Fin ) → ( 𝑦 ∈ 𝑥 → 𝑦 ∈ dom vol ) )
24 18 23 ralrimi ⊢ ( ( ( 𝑥 ∈ 𝒫 dom vol ∧ ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ) ∧ 𝑥 ∈ Fin ) → ∀ 𝑦 ∈ 𝑥 𝑦 ∈ dom vol )
25 simplrr ⊢ ( ( ( 𝑥 ∈ 𝒫 dom vol ∧ ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ) ∧ 𝑥 ∈ Fin ) → Disj 𝑦 ∈ 𝑥 𝑦 )
26 uniiun ⊢ ∪ 𝑥 = ∪ 𝑦 ∈ 𝑥 𝑦
27 26 fveq2i ⊢ ( vol ‘ ∪ 𝑥 ) = ( vol ‘ ∪ 𝑦 ∈ 𝑥 𝑦 )
28 volfiniune ⊢ ( ( 𝑥 ∈ Fin ∧ ∀ 𝑦 ∈ 𝑥 𝑦 ∈ dom vol ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ( vol ‘ ∪ 𝑦 ∈ 𝑥 𝑦 ) = Σ* 𝑦 ∈ 𝑥 ( vol ‘ 𝑦 ) )
29 27 28 eqtrid ⊢ ( ( 𝑥 ∈ Fin ∧ ∀ 𝑦 ∈ 𝑥 𝑦 ∈ dom vol ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ( vol ‘ ∪ 𝑥 ) = Σ* 𝑦 ∈ 𝑥 ( vol ‘ 𝑦 ) )
30 11 24 25 29 syl3anc ⊢ ( ( ( 𝑥 ∈ 𝒫 dom vol ∧ ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ) ∧ 𝑥 ∈ Fin ) → ( vol ‘ ∪ 𝑥 ) = Σ* 𝑦 ∈ 𝑥 ( vol ‘ 𝑦 ) )
31 bren ⊢ ( ℕ ≈ 𝑥 ↔ ∃ 𝑓 𝑓 : ℕ –1-1-onto→ 𝑥 )
32 nfv ⊢ Ⅎ 𝑛 ( 𝑥 ∈ 𝒫 dom vol ∧ 𝑓 : ℕ –1-1-onto→ 𝑥 )
33 nfcv ⊢ Ⅎ 𝑛 ( vol ‘ 𝑦 )
34 nfcv ⊢ Ⅎ 𝑦 ( vol ‘ ( 𝑓 ‘ 𝑛 ) )
35 nfcv ⊢ Ⅎ 𝑛 𝑥
36 nfcv ⊢ Ⅎ 𝑛 ℕ
37 nfcv ⊢ Ⅎ 𝑛 𝑓
38 fveq2 ⊢ ( 𝑦 = ( 𝑓 ‘ 𝑛 ) → ( vol ‘ 𝑦 ) = ( vol ‘ ( 𝑓 ‘ 𝑛 ) ) )
39 simpl ⊢ ( ( 𝑥 ∈ 𝒫 dom vol ∧ 𝑓 : ℕ –1-1-onto→ 𝑥 ) → 𝑥 ∈ 𝒫 dom vol )
40 simpr ⊢ ( ( 𝑥 ∈ 𝒫 dom vol ∧ 𝑓 : ℕ –1-1-onto→ 𝑥 ) → 𝑓 : ℕ –1-1-onto→ 𝑥 )
41 eqidd ⊢ ( ( ( 𝑥 ∈ 𝒫 dom vol ∧ 𝑓 : ℕ –1-1-onto→ 𝑥 ) ∧ 𝑛 ∈ ℕ ) → ( 𝑓 ‘ 𝑛 ) = ( 𝑓 ‘ 𝑛 ) )
42 1 a1i ⊢ ( ( ( 𝑥 ∈ 𝒫 dom vol ∧ 𝑓 : ℕ –1-1-onto→ 𝑥 ) ∧ 𝑦 ∈ 𝑥 ) → vol : dom vol ⟶ ( 0 [,] +∞ ) )
43 39 19 syl ⊢ ( ( 𝑥 ∈ 𝒫 dom vol ∧ 𝑓 : ℕ –1-1-onto→ 𝑥 ) → 𝑥 ⊆ dom vol )
44 43 sselda ⊢ ( ( ( 𝑥 ∈ 𝒫 dom vol ∧ 𝑓 : ℕ –1-1-onto→ 𝑥 ) ∧ 𝑦 ∈ 𝑥 ) → 𝑦 ∈ dom vol )
45 42 44 ffvelcdmd ⊢ ( ( ( 𝑥 ∈ 𝒫 dom vol ∧ 𝑓 : ℕ –1-1-onto→ 𝑥 ) ∧ 𝑦 ∈ 𝑥 ) → ( vol ‘ 𝑦 ) ∈ ( 0 [,] +∞ ) )
46 32 33 34 35 36 37 38 39 40 41 45 esumf1o ⊢ ( ( 𝑥 ∈ 𝒫 dom vol ∧ 𝑓 : ℕ –1-1-onto→ 𝑥 ) → Σ* 𝑦 ∈ 𝑥 ( vol ‘ 𝑦 ) = Σ* 𝑛 ∈ ℕ ( vol ‘ ( 𝑓 ‘ 𝑛 ) ) )
47 46 adantlr ⊢ ( ( ( 𝑥 ∈ 𝒫 dom vol ∧ ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ) ∧ 𝑓 : ℕ –1-1-onto→ 𝑥 ) → Σ* 𝑦 ∈ 𝑥 ( vol ‘ 𝑦 ) = Σ* 𝑛 ∈ ℕ ( vol ‘ ( 𝑓 ‘ 𝑛 ) ) )
48 19 ad3antrrr ⊢ ( ( ( ( 𝑥 ∈ 𝒫 dom vol ∧ ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ) ∧ 𝑓 : ℕ –1-1-onto→ 𝑥 ) ∧ 𝑛 ∈ ℕ ) → 𝑥 ⊆ dom vol )
49 f1of ⊢ ( 𝑓 : ℕ –1-1-onto→ 𝑥 → 𝑓 : ℕ ⟶ 𝑥 )
50 49 adantl ⊢ ( ( ( 𝑥 ∈ 𝒫 dom vol ∧ ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ) ∧ 𝑓 : ℕ –1-1-onto→ 𝑥 ) → 𝑓 : ℕ ⟶ 𝑥 )
51 50 ffvelcdmda ⊢ ( ( ( ( 𝑥 ∈ 𝒫 dom vol ∧ ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ) ∧ 𝑓 : ℕ –1-1-onto→ 𝑥 ) ∧ 𝑛 ∈ ℕ ) → ( 𝑓 ‘ 𝑛 ) ∈ 𝑥 )
52 48 51 sseldd ⊢ ( ( ( ( 𝑥 ∈ 𝒫 dom vol ∧ ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ) ∧ 𝑓 : ℕ –1-1-onto→ 𝑥 ) ∧ 𝑛 ∈ ℕ ) → ( 𝑓 ‘ 𝑛 ) ∈ dom vol )
53 52 ralrimiva ⊢ ( ( ( 𝑥 ∈ 𝒫 dom vol ∧ ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ) ∧ 𝑓 : ℕ –1-1-onto→ 𝑥 ) → ∀ 𝑛 ∈ ℕ ( 𝑓 ‘ 𝑛 ) ∈ dom vol )
54 simpr ⊢ ( ( ( 𝑥 ∈ 𝒫 dom vol ∧ ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ) ∧ 𝑓 : ℕ –1-1-onto→ 𝑥 ) → 𝑓 : ℕ –1-1-onto→ 𝑥 )
55 simplrr ⊢ ( ( ( 𝑥 ∈ 𝒫 dom vol ∧ ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ) ∧ 𝑓 : ℕ –1-1-onto→ 𝑥 ) → Disj 𝑦 ∈ 𝑥 𝑦 )
56 id ⊢ ( 𝑓 : ℕ –1-1-onto→ 𝑥 → 𝑓 : ℕ –1-1-onto→ 𝑥 )
57 simpr ⊢ ( ( 𝑓 : ℕ –1-1-onto→ 𝑥 ∧ 𝑦 = ( 𝑓 ‘ 𝑛 ) ) → 𝑦 = ( 𝑓 ‘ 𝑛 ) )
58 56 57 disjrdx ⊢ ( 𝑓 : ℕ –1-1-onto→ 𝑥 → ( Disj 𝑛 ∈ ℕ ( 𝑓 ‘ 𝑛 ) ↔ Disj 𝑦 ∈ 𝑥 𝑦 ) )
59 58 biimpar ⊢ ( ( 𝑓 : ℕ –1-1-onto→ 𝑥 ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → Disj 𝑛 ∈ ℕ ( 𝑓 ‘ 𝑛 ) )
60 54 55 59 syl2anc ⊢ ( ( ( 𝑥 ∈ 𝒫 dom vol ∧ ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ) ∧ 𝑓 : ℕ –1-1-onto→ 𝑥 ) → Disj 𝑛 ∈ ℕ ( 𝑓 ‘ 𝑛 ) )
61 voliune ⊢ ( ( ∀ 𝑛 ∈ ℕ ( 𝑓 ‘ 𝑛 ) ∈ dom vol ∧ Disj 𝑛 ∈ ℕ ( 𝑓 ‘ 𝑛 ) ) → ( vol ‘ ∪ 𝑛 ∈ ℕ ( 𝑓 ‘ 𝑛 ) ) = Σ* 𝑛 ∈ ℕ ( vol ‘ ( 𝑓 ‘ 𝑛 ) ) )
62 53 60 61 syl2anc ⊢ ( ( ( 𝑥 ∈ 𝒫 dom vol ∧ ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ) ∧ 𝑓 : ℕ –1-1-onto→ 𝑥 ) → ( vol ‘ ∪ 𝑛 ∈ ℕ ( 𝑓 ‘ 𝑛 ) ) = Σ* 𝑛 ∈ ℕ ( vol ‘ ( 𝑓 ‘ 𝑛 ) ) )
63 f1ofo ⊢ ( 𝑓 : ℕ –1-1-onto→ 𝑥 → 𝑓 : ℕ –onto→ 𝑥 )
64 63 57 iunrdx ⊢ ( 𝑓 : ℕ –1-1-onto→ 𝑥 → ∪ 𝑛 ∈ ℕ ( 𝑓 ‘ 𝑛 ) = ∪ 𝑦 ∈ 𝑥 𝑦 )
65 64 26 eqtr4di ⊢ ( 𝑓 : ℕ –1-1-onto→ 𝑥 → ∪ 𝑛 ∈ ℕ ( 𝑓 ‘ 𝑛 ) = ∪ 𝑥 )
66 65 fveq2d ⊢ ( 𝑓 : ℕ –1-1-onto→ 𝑥 → ( vol ‘ ∪ 𝑛 ∈ ℕ ( 𝑓 ‘ 𝑛 ) ) = ( vol ‘ ∪ 𝑥 ) )
67 66 adantl ⊢ ( ( ( 𝑥 ∈ 𝒫 dom vol ∧ ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ) ∧ 𝑓 : ℕ –1-1-onto→ 𝑥 ) → ( vol ‘ ∪ 𝑛 ∈ ℕ ( 𝑓 ‘ 𝑛 ) ) = ( vol ‘ ∪ 𝑥 ) )
68 47 62 67 3eqtr2rd ⊢ ( ( ( 𝑥 ∈ 𝒫 dom vol ∧ ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ) ∧ 𝑓 : ℕ –1-1-onto→ 𝑥 ) → ( vol ‘ ∪ 𝑥 ) = Σ* 𝑦 ∈ 𝑥 ( vol ‘ 𝑦 ) )
69 68 ex ⊢ ( ( 𝑥 ∈ 𝒫 dom vol ∧ ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ) → ( 𝑓 : ℕ –1-1-onto→ 𝑥 → ( vol ‘ ∪ 𝑥 ) = Σ* 𝑦 ∈ 𝑥 ( vol ‘ 𝑦 ) ) )
70 69 exlimdv ⊢ ( ( 𝑥 ∈ 𝒫 dom vol ∧ ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ) → ( ∃ 𝑓 𝑓 : ℕ –1-1-onto→ 𝑥 → ( vol ‘ ∪ 𝑥 ) = Σ* 𝑦 ∈ 𝑥 ( vol ‘ 𝑦 ) ) )
71 70 imp ⊢ ( ( ( 𝑥 ∈ 𝒫 dom vol ∧ ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ) ∧ ∃ 𝑓 𝑓 : ℕ –1-1-onto→ 𝑥 ) → ( vol ‘ ∪ 𝑥 ) = Σ* 𝑦 ∈ 𝑥 ( vol ‘ 𝑦 ) )
72 31 71 sylan2b ⊢ ( ( ( 𝑥 ∈ 𝒫 dom vol ∧ ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ) ∧ ℕ ≈ 𝑥 ) → ( vol ‘ ∪ 𝑥 ) = Σ* 𝑦 ∈ 𝑥 ( vol ‘ 𝑦 ) )
73 brdom2 ⊢ ( 𝑥 ≼ ω ↔ ( 𝑥 ≺ ω ∨ 𝑥 ≈ ω ) )
74 73 biimpi ⊢ ( 𝑥 ≼ ω → ( 𝑥 ≺ ω ∨ 𝑥 ≈ ω ) )
75 isfinite2 ⊢ ( 𝑥 ≺ ω → 𝑥 ∈ Fin )
76 ensymb ⊢ ( 𝑥 ≈ ω ↔ ω ≈ 𝑥 )
77 nnenom ⊢ ℕ ≈ ω
78 entr ⊢ ( ( ℕ ≈ ω ∧ ω ≈ 𝑥 ) → ℕ ≈ 𝑥 )
79 77 78 mpan ⊢ ( ω ≈ 𝑥 → ℕ ≈ 𝑥 )
80 76 79 sylbi ⊢ ( 𝑥 ≈ ω → ℕ ≈ 𝑥 )
81 75 80 orim12i ⊢ ( ( 𝑥 ≺ ω ∨ 𝑥 ≈ ω ) → ( 𝑥 ∈ Fin ∨ ℕ ≈ 𝑥 ) )
82 74 81 syl ⊢ ( 𝑥 ≼ ω → ( 𝑥 ∈ Fin ∨ ℕ ≈ 𝑥 ) )
83 82 ad2antrl ⊢ ( ( 𝑥 ∈ 𝒫 dom vol ∧ ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ) → ( 𝑥 ∈ Fin ∨ ℕ ≈ 𝑥 ) )
84 30 72 83 mpjaodan ⊢ ( ( 𝑥 ∈ 𝒫 dom vol ∧ ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ) → ( vol ‘ ∪ 𝑥 ) = Σ* 𝑦 ∈ 𝑥 ( vol ‘ 𝑦 ) )
85 84 ex ⊢ ( 𝑥 ∈ 𝒫 dom vol → ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ( vol ‘ ∪ 𝑥 ) = Σ* 𝑦 ∈ 𝑥 ( vol ‘ 𝑦 ) ) )
86 85 rgen ⊢ ∀ 𝑥 ∈ 𝒫 dom vol ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ( vol ‘ ∪ 𝑥 ) = Σ* 𝑦 ∈ 𝑥 ( vol ‘ 𝑦 ) )
87 ismeas ⊢ ( dom vol ∈ ∪ ran sigAlgebra → ( vol ∈ ( measures ‘ dom vol ) ↔ ( vol : dom vol ⟶ ( 0 [,] +∞ ) ∧ ( vol ‘ ∅ ) = 0 ∧ ∀ 𝑥 ∈ 𝒫 dom vol ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ( vol ‘ ∪ 𝑥 ) = Σ* 𝑦 ∈ 𝑥 ( vol ‘ 𝑦 ) ) ) ) )
88 4 87 ax-mp ⊢ ( vol ∈ ( measures ‘ dom vol ) ↔ ( vol : dom vol ⟶ ( 0 [,] +∞ ) ∧ ( vol ‘ ∅ ) = 0 ∧ ∀ 𝑥 ∈ 𝒫 dom vol ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ( vol ‘ ∪ 𝑥 ) = Σ* 𝑦 ∈ 𝑥 ( vol ‘ 𝑦 ) ) ) )
89 1 10 86 88 mpbir3an ⊢ vol ∈ ( measures ‘ dom vol )