Theorem dmvolss

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

	Ref	Expression
Assertion	dmvolss	⊢ dom vol ⊆ 𝒫 ℝ

Proof

Step	Hyp	Ref	Expression
1		elex	⊢ ( 𝑥 ∈ dom vol → 𝑥 ∈ V )
2		mblss	⊢ ( 𝑥 ∈ dom vol → 𝑥 ⊆ ℝ )
3	1 2	elpwd	⊢ ( 𝑥 ∈ dom vol → 𝑥 ∈ 𝒫 ℝ )
4	3	rgen	⊢ ∀ 𝑥 ∈ dom vol 𝑥 ∈ 𝒫 ℝ
5		dfss3	⊢ ( dom vol ⊆ 𝒫 ℝ ↔ ∀ 𝑥 ∈ dom vol 𝑥 ∈ 𝒫 ℝ )
6	4 5	mpbir	⊢ dom vol ⊆ 𝒫 ℝ