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 ⊆ 𝒫 ℝ ↔ ∀ 𝑥 ∈ dom vol 𝑥 ⊆ ℝ )
2		mblss	⊢ ( 𝑥 ∈ dom vol → 𝑥 ⊆ ℝ )
3	1 2	mprgbir	⊢ dom vol ⊆ 𝒫 ℝ
4		rembl	⊢ ℝ ∈ dom vol
5		cmmbl	⊢ ( 𝑥 ∈ dom vol → ( ℝ ∖ 𝑥 ) ∈ dom vol )
6	5	rgen	⊢ ∀ 𝑥 ∈ dom vol ( ℝ ∖ 𝑥 ) ∈ dom vol
7		nnenom	⊢ ℕ ≈ ω
8	7	ensymi	⊢ ω ≈ ℕ
9		domentr	⊢ ( ( 𝑥 ≼ ω ∧ ω ≈ ℕ ) → 𝑥 ≼ ℕ )
10	8 9	mpan2	⊢ ( 𝑥 ≼ ω → 𝑥 ≼ ℕ )
11		elpwi	⊢ ( 𝑥 ∈ 𝒫 dom vol → 𝑥 ⊆ dom vol )
12		dfss3	⊢ ( 𝑥 ⊆ dom vol ↔ ∀ 𝑦 ∈ 𝑥 𝑦 ∈ dom vol )
13	11 12	sylib	⊢ ( 𝑥 ∈ 𝒫 dom vol → ∀ 𝑦 ∈ 𝑥 𝑦 ∈ dom vol )
14		iunmbl2	⊢ ( ( 𝑥 ≼ ℕ ∧ ∀ 𝑦 ∈ 𝑥 𝑦 ∈ dom vol ) → ∪ 𝑦 ∈ 𝑥 𝑦 ∈ dom vol )
15	10 13 14	syl2anr	⊢ ( ( 𝑥 ∈ 𝒫 dom vol ∧ 𝑥 ≼ ω ) → ∪ 𝑦 ∈ 𝑥 𝑦 ∈ dom vol )
16	15	ex	⊢ ( 𝑥 ∈ 𝒫 dom vol → ( 𝑥 ≼ ω → ∪ 𝑦 ∈ 𝑥 𝑦 ∈ dom vol ) )
17		uniiun	⊢ ∪ 𝑥 = ∪ 𝑦 ∈ 𝑥 𝑦
18	17	eleq1i	⊢ ( ∪ 𝑥 ∈ dom vol ↔ ∪ 𝑦 ∈ 𝑥 𝑦 ∈ dom vol )
19	16 18	imbitrrdi	⊢ ( 𝑥 ∈ 𝒫 dom vol → ( 𝑥 ≼ ω → ∪ 𝑥 ∈ dom vol ) )
20	19	rgen	⊢ ∀ 𝑥 ∈ 𝒫 dom vol ( 𝑥 ≼ ω → ∪ 𝑥 ∈ dom vol )
21	4 6 20	3pm3.2i	⊢ ( ℝ ∈ dom vol ∧ ∀ 𝑥 ∈ dom vol ( ℝ ∖ 𝑥 ) ∈ dom vol ∧ ∀ 𝑥 ∈ 𝒫 dom vol ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 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 ∧ ∀ 𝑥 ∈ dom vol ( ℝ ∖ 𝑥 ) ∈ dom vol ∧ ∀ 𝑥 ∈ 𝒫 dom vol ( 𝑥 ≼ ω → ∪ 𝑥 ∈ dom vol ) ) ) ) )
26	24 25	ax-mp	⊢ ( dom vol ∈ ( sigAlgebra ‘ ℝ ) ↔ ( dom vol ⊆ 𝒫 ℝ ∧ ( ℝ ∈ dom vol ∧ ∀ 𝑥 ∈ dom vol ( ℝ ∖ 𝑥 ) ∈ dom vol ∧ ∀ 𝑥 ∈ 𝒫 dom vol ( 𝑥 ≼ ω → ∪ 𝑥 ∈ dom vol ) ) ) )
27	3 21 26	mpbir2an	⊢ dom vol ∈ ( sigAlgebra ‘ ℝ )