dmvolsal

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

		Ref	Expression
	Assertion	dmvolsal	$⊢ dom vol \in SAlg$

Step	Hyp	Ref	Expression
1		reex	$⊢ ℝ \in V$
2	1	pwex	$⊢ 𝒫 ℝ \in V$
3		dmvolss	$⊢ dom vol \subseteq 𝒫 ℝ$
4	2 3	ssexi	$⊢ dom vol \in V$
5	4	a1i	$⊢ ⊤ \to dom vol \in V$
6		0mbl	$⊢ \emptyset \in dom vol$
7	6	a1i	$⊢ ⊤ \to \emptyset \in dom vol$
8		unidmvol	$⊢ ⋃ dom vol = ℝ$
9	8	eqcomi	$⊢ ℝ = ⋃ dom vol$
10		cmmbl	$⊢ y \in dom vol \to ℝ ∖ y \in dom vol$
11	10	adantl	$⊢ (⊤ \land y \in dom vol) \to ℝ ∖ y \in dom vol$
12		ffvelcdm	$⊢ (e : ℕ ⟶ dom vol \land n \in ℕ) \to e (n) \in dom vol$
13	12	ralrimiva	$⊢ e : ℕ ⟶ dom vol \to \forall n \in ℕ e (n) \in dom vol$
14		iunmbl	$⊢ \forall n \in ℕ e (n) \in dom vol \to ⋃_{n \in ℕ} e (n) \in dom vol$
15	13 14	syl	$⊢ e : ℕ ⟶ dom vol \to ⋃_{n \in ℕ} e (n) \in dom vol$
16	15	adantl	$⊢ (⊤ \land e : ℕ ⟶ dom vol) \to ⋃_{n \in ℕ} e (n) \in dom vol$
17	5 7 9 11 16	issalnnd	$⊢ ⊤ \to dom vol \in SAlg$
18	17	mptru	$⊢ dom vol \in SAlg$

Metamath Proof Explorer