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	⊢ ( 𝑦 ∈ dom vol → ( ℝ ∖ 𝑦 ) ∈ dom vol )
11	10	adantl	⊢ ( ( ⊤ ∧ 𝑦 ∈ dom vol ) → ( ℝ ∖ 𝑦 ) ∈ dom vol )
12		ffvelrn	⊢ ( ( 𝑒 : ℕ ⟶ dom vol ∧ 𝑛 ∈ ℕ ) → ( 𝑒 ‘ 𝑛 ) ∈ dom vol )
13	12	ralrimiva	⊢ ( 𝑒 : ℕ ⟶ dom vol → ∀ 𝑛 ∈ ℕ ( 𝑒 ‘ 𝑛 ) ∈ dom vol )
14		iunmbl	⊢ ( ∀ 𝑛 ∈ ℕ ( 𝑒 ‘ 𝑛 ) ∈ dom vol → ∪ 𝑛 ∈ ℕ ( 𝑒 ‘ 𝑛 ) ∈ dom vol )
15	13 14	syl	⊢ ( 𝑒 : ℕ ⟶ dom vol → ∪ 𝑛 ∈ ℕ ( 𝑒 ‘ 𝑛 ) ∈ dom vol )
16	15	adantl	⊢ ( ( ⊤ ∧ 𝑒 : ℕ ⟶ dom vol ) → ∪ 𝑛 ∈ ℕ ( 𝑒 ‘ 𝑛 ) ∈ dom vol )
17	5 7 9 11 16	issalnnd	⊢ ( ⊤ → dom vol ∈ SAlg )
18	17	mptru	⊢ dom vol ∈ SAlg