# Metamath Proof Explorer

## 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 ${⊢}\mathrm{dom}vol\in \mathrm{sigAlgebra}\left(ℝ\right)$

### Proof

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