Theorem unidmvol

Description: The union of the Lebesgue measurable sets is RR . (Contributed by Thierry Arnoux, 30-Jan-2017)

	Ref	Expression
Assertion	unidmvol	$$⊢\bigcup \mathrm{dom}vol=ℝ$$

Proof

Step	Hyp	Ref	Expression
1		unissb	$$⊢\bigcup \mathrm{dom}vol\subseteq ℝ\leftrightarrow \forall x\in \mathrm{dom}volx\subseteq ℝ$$
2		mblss	$$⊢x\in \mathrm{dom}vol\to x\subseteq ℝ$$
3	1 2	mprgbir	$$⊢\bigcup \mathrm{dom}vol\subseteq ℝ$$
4		rembl	$$⊢ℝ\in \mathrm{dom}vol$$
5		unissel	$$⊢\left(\bigcup \mathrm{dom}vol\subseteq ℝ\wedge ℝ\in \mathrm{dom}vol\right)\to \bigcup \mathrm{dom}vol=ℝ$$
6	3 4 5	mp2an	$$⊢\bigcup \mathrm{dom}vol=ℝ$$