Theorem vonmblss2

Description: n-dimensional Lebesgue measurable sets are subsets of the n-dimensional real Euclidean space. (Contributed by Glauco Siliprandi, 3-Mar-2021)

	Ref	Expression
Hypotheses	vonmblss2.x	⊢ ( 𝜑 → 𝑋 ∈ Fin )
	vonmblss2.y	⊢ ( 𝜑 → 𝑌 ∈ dom ( voln ‘ 𝑋 ) )
Assertion	vonmblss2	⊢ ( 𝜑 → 𝑌 ⊆ ( ℝ ↑m 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		vonmblss2.x	⊢ ( 𝜑 → 𝑋 ∈ Fin )
2		vonmblss2.y	⊢ ( 𝜑 → 𝑌 ∈ dom ( voln ‘ 𝑋 ) )
3	1	vonmblss	⊢ ( 𝜑 → dom ( voln ‘ 𝑋 ) ⊆ 𝒫 ( ℝ ↑m 𝑋 ) )
4	3 2	sseldd	⊢ ( 𝜑 → 𝑌 ∈ 𝒫 ( ℝ ↑m 𝑋 ) )
5		elpwi	⊢ ( 𝑌 ∈ 𝒫 ( ℝ ↑m 𝑋 ) → 𝑌 ⊆ ( ℝ ↑m 𝑋 ) )
6	4 5	syl	⊢ ( 𝜑 → 𝑌 ⊆ ( ℝ ↑m 𝑋 ) )