Metamath Proof Explorer

Theorem dmvlsiga

Description: Lebesgue-measurable subsets of RR form a sigma-algebra. (Contributed by Thierry Arnoux, 10-Sep-2016) (Revised by Thierry Arnoux, 24-Oct-2016)

Ref Expression
Assertion dmvlsiga ⊢ dom ⁡ vol ∈ sigAlgebra ⁡ ℝ

Proof

Step Hyp Ref Expression
1 pwssb ⊢ dom ⁡ vol ⊆ 𝒫 ℝ ↔ ∀ x ∈ dom ⁡ vol x ⊆ ℝ
2 mblss ⊢ x ∈ dom ⁡ vol → x ⊆ ℝ
3 1 2 mprgbir ⊢ dom ⁡ vol ⊆ 𝒫 ℝ
4 rembl ⊢ ℝ ∈ dom ⁡ vol
5 cmmbl ⊢ x ∈ dom ⁡ vol → ℝ ∖ x ∈ dom ⁡ vol
6 5 rgen ⊢ ∀ x ∈ dom ⁡ vol ℝ ∖ x ∈ dom ⁡ vol
7 nnenom ⊢ ℕ ≈ ω
8 7 ensymi ⊢ ω ≈ ℕ
9 domentr ⊢ x ≼ ω ∧ ω ≈ ℕ → x ≼ ℕ
10 8 9 mpan2 ⊢ x ≼ ω → x ≼ ℕ
11 elpwi ⊢ x ∈ 𝒫 dom ⁡ vol → x ⊆ dom ⁡ vol
12 dfss3 ⊢ x ⊆ dom ⁡ vol ↔ ∀ y ∈ x y ∈ dom ⁡ vol
13 11 12 sylib ⊢ x ∈ 𝒫 dom ⁡ vol → ∀ y ∈ x y ∈ dom ⁡ vol
14 iunmbl2 ⊢ x ≼ ℕ ∧ ∀ y ∈ x y ∈ dom ⁡ vol → ⋃ y ∈ x y ∈ dom ⁡ vol
15 10 13 14 syl2anr ⊢ x ∈ 𝒫 dom ⁡ vol ∧ x ≼ ω → ⋃ y ∈ x y ∈ dom ⁡ vol
16 15 ex ⊢ x ∈ 𝒫 dom ⁡ vol → x ≼ ω → ⋃ y ∈ x y ∈ dom ⁡ vol
17 uniiun ⊢ ⋃ x = ⋃ y ∈ x y
18 17 eleq1i ⊢ ⋃ x ∈ dom ⁡ vol ↔ ⋃ y ∈ x y ∈ dom ⁡ vol
19 16 18 imbitrrdi ⊢ x ∈ 𝒫 dom ⁡ vol → x ≼ ω → ⋃ x ∈ dom ⁡ vol
20 19 rgen ⊢ ∀ x ∈ 𝒫 dom ⁡ vol x ≼ ω → ⋃ x ∈ dom ⁡ vol
21 4 6 20 3pm3.2i ⊢ ℝ ∈ dom ⁡ vol ∧ ∀ x ∈ dom ⁡ vol ℝ ∖ x ∈ dom ⁡ vol ∧ ∀ x ∈ 𝒫 dom ⁡ vol x ≼ ω → ⋃ x ∈ dom ⁡ vol
22 reex ⊢ ℝ ∈ V
23 22 pwex ⊢ 𝒫 ℝ ∈ V
24 23 3 ssexi ⊢ dom ⁡ vol ∈ V
25 issiga ⊢ dom ⁡ vol ∈ V → dom ⁡ vol ∈ sigAlgebra ⁡ ℝ ↔ dom ⁡ vol ⊆ 𝒫 ℝ ∧ ℝ ∈ dom ⁡ vol ∧ ∀ x ∈ dom ⁡ vol ℝ ∖ x ∈ dom ⁡ vol ∧ ∀ x ∈ 𝒫 dom ⁡ vol x ≼ ω → ⋃ x ∈ dom ⁡ vol
26 24 25 ax-mp ⊢ dom ⁡ vol ∈ sigAlgebra ⁡ ℝ ↔ dom ⁡ vol ⊆ 𝒫 ℝ ∧ ℝ ∈ dom ⁡ vol ∧ ∀ x ∈ dom ⁡ vol ℝ ∖ x ∈ dom ⁡ vol ∧ ∀ x ∈ 𝒫 dom ⁡ vol x ≼ ω → ⋃ x ∈ dom ⁡ vol
27 3 21 26 mpbir2an ⊢ dom ⁡ vol ∈ sigAlgebra ⁡ ℝ