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 \in sigAlgebra (ℝ)$

Proof

Step	Hyp	Ref	Expression
1		pwssb	$⊢ dom vol \subseteq 𝒫 ℝ \leftrightarrow \forall x \in dom vol x \subseteq ℝ$
2		mblss	$⊢ x \in dom vol \to x \subseteq ℝ$
3	1 2	mprgbir	$⊢ dom vol \subseteq 𝒫 ℝ$
4		rembl	$⊢ ℝ \in dom vol$
5		cmmbl	$⊢ x \in dom vol \to ℝ ∖ x \in dom vol$
6	5	rgen	$⊢ \forall x \in dom vol ℝ ∖ x \in dom vol$
7		nnenom	$⊢ ℕ \approx ω$
8	7	ensymi	$⊢ ω \approx ℕ$
9		domentr	$⊢ (x ≼ ω \land ω \approx ℕ) \to x ≼ ℕ$
10	8 9	mpan2	$⊢ x ≼ ω \to x ≼ ℕ$
11		elpwi	$⊢ x \in 𝒫 dom vol \to x \subseteq dom vol$
12		dfss3	$⊢ x \subseteq dom vol \leftrightarrow \forall y \in x y \in dom vol$
13	11 12	sylib	$⊢ x \in 𝒫 dom vol \to \forall y \in x y \in dom vol$
14		iunmbl2	$⊢ (x ≼ ℕ \land \forall y \in x y \in dom vol) \to ⋃_{y \in x} y \in dom vol$
15	10 13 14	syl2anr	$⊢ (x \in 𝒫 dom vol \land x ≼ ω) \to ⋃_{y \in x} y \in dom vol$
16	15	ex	$⊢ x \in 𝒫 dom vol \to (x ≼ ω \to ⋃_{y \in x} y \in dom vol)$
17		uniiun	$⊢ ⋃ x = ⋃_{y \in x} y$
18	17	eleq1i	$⊢ ⋃ x \in dom vol \leftrightarrow ⋃_{y \in x} y \in dom vol$
19	16 18	syl6ibr	$⊢ x \in 𝒫 dom vol \to (x ≼ ω \to ⋃ x \in dom vol)$
20	19	rgen	$⊢ \forall x \in 𝒫 dom vol (x ≼ ω \to ⋃ x \in dom vol)$
21	4 6 20	3pm3.2i	$⊢ (ℝ \in dom vol \land \forall x \in dom vol ℝ ∖ x \in dom vol \land \forall x \in 𝒫 dom vol (x ≼ ω \to ⋃ x \in dom vol))$
22		reex	$⊢ ℝ \in V$
23	22	pwex	$⊢ 𝒫 ℝ \in V$
24	23 3	ssexi	$⊢ dom vol \in V$
25		issiga	$⊢ dom vol \in V \to (dom vol \in sigAlgebra (ℝ) \leftrightarrow (dom vol \subseteq 𝒫 ℝ \land (ℝ \in dom vol \land \forall x \in dom vol ℝ ∖ x \in dom vol \land \forall x \in 𝒫 dom vol (x ≼ ω \to ⋃ x \in dom vol))))$
26	24 25	ax-mp	$⊢ dom vol \in sigAlgebra (ℝ) \leftrightarrow (dom vol \subseteq 𝒫 ℝ \land (ℝ \in dom vol \land \forall x \in dom vol ℝ ∖ x \in dom vol \land \forall x \in 𝒫 dom vol (x ≼ ω \to ⋃ x \in dom vol)))$
27	3 21 26	mpbir2an	$⊢ dom vol \in sigAlgebra (ℝ)$

Metamath Proof Explorer

Theorem dmvlsiga

Proof