Theorem dmvolss

Description: Lebesgue measurable sets are subsets of Real numbers. (Contributed by Glauco Siliprandi, 3-Mar-2021)

	Ref	Expression
Assertion	dmvolss	$$⊢\mathrm{dom}vol\subseteq 𝒫ℝ$$

Proof

Step	Hyp	Ref	Expression
1		elex	$$⊢x\in \mathrm{dom}vol\to x\in \mathrm{V}$$
2		mblss	$$⊢x\in \mathrm{dom}vol\to x\subseteq ℝ$$
3	1 2	elpwd	$$⊢x\in \mathrm{dom}vol\to x\in 𝒫ℝ$$
4	3	rgen	$$⊢\forall x\in \mathrm{dom}volx\in 𝒫ℝ$$
5		dfss3	$$⊢\mathrm{dom}vol\subseteq 𝒫ℝ\leftrightarrow \forall x\in \mathrm{dom}volx\in 𝒫ℝ$$
6	4 5	mpbir	$$⊢\mathrm{dom}vol\subseteq 𝒫ℝ$$