Metamath Proof Explorer

Theorem dmvolsal

Description: Lebesgue measurable sets form a sigma-algebra. (Contributed by Glauco Siliprandi, 3-Mar-2021)

Ref Expression
Assertion dmvolsal ⊢ dom ⁡ vol ∈ SAlg

Proof

Step Hyp Ref Expression
1 reex ⊢ ℝ ∈ V
2 1 pwex ⊢ 𝒫 ℝ ∈ V
3 dmvolss ⊢ dom ⁡ vol ⊆ 𝒫 ℝ
4 2 3 ssexi ⊢ dom ⁡ vol ∈ V
5 4 a1i ⊢ ⊤ → dom ⁡ vol ∈ V
6 0mbl ⊢ ∅ ∈ dom ⁡ vol
7 6 a1i ⊢ ⊤ → ∅ ∈ dom ⁡ vol
8 unidmvol ⊢ ⋃ dom ⁡ vol = ℝ
9 8 eqcomi ⊢ ℝ = ⋃ dom ⁡ vol
10 cmmbl ⊢ y ∈ dom ⁡ vol → ℝ ∖ y ∈ dom ⁡ vol
11 10 adantl ⊢ ⊤ ∧ y ∈ dom ⁡ vol → ℝ ∖ y ∈ dom ⁡ vol
12 ffvelrn ⊢ e : ℕ ⟶ dom ⁡ vol ∧ n ∈ ℕ → e ⁡ n ∈ dom ⁡ vol
13 12 ralrimiva ⊢ e : ℕ ⟶ dom ⁡ vol → ∀ n ∈ ℕ e ⁡ n ∈ dom ⁡ vol
14 iunmbl ⊢ ∀ n ∈ ℕ e ⁡ n ∈ dom ⁡ vol → ⋃ n ∈ ℕ e ⁡ n ∈ dom ⁡ vol
15 13 14 syl ⊢ e : ℕ ⟶ dom ⁡ vol → ⋃ n ∈ ℕ e ⁡ n ∈ dom ⁡ vol
16 15 adantl ⊢ ⊤ ∧ e : ℕ ⟶ dom ⁡ vol → ⋃ n ∈ ℕ e ⁡ n ∈ dom ⁡ vol
17 5 7 9 11 16 issalnnd ⊢ ⊤ → dom ⁡ vol ∈ SAlg
18 17 mptru ⊢ dom ⁡ vol ∈ SAlg