Theorem mblss

Description: A measurable set is a subset of the reals. (Contributed by Mario Carneiro, 17-Mar-2014)

	Ref	Expression
Assertion	mblss	$$⊢A\in \mathrm{dom}vol\to A\subseteq ℝ$$

Proof

Step	Hyp	Ref	Expression
1		ismbl	$$⊢A\in \mathrm{dom}vol\leftrightarrow \left(A\subseteq ℝ\wedge \forall x\in 𝒫ℝ\left({vol}^{*}\left(x\right)\in ℝ\to {vol}^{*}\left(x\right)={vol}^{*}\left(x\cap A\right)+{vol}^{*}\left(x\setminus A\right)\right)\right)$$
2	1	simplbi	$$⊢A\in \mathrm{dom}vol\to A\subseteq ℝ$$