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	$$⊢\phi \to X\in \mathrm{Fin}$$
	vonmblss2.y	$$⊢\phi \to Y\in \mathrm{dom}\mathrm{voln}\left(X\right)$$
Assertion	vonmblss2	$$⊢\phi \to Y\subseteq {ℝ}^X$$

Proof

Step	Hyp	Ref	Expression
1		vonmblss2.x	$$⊢\phi \to X\in \mathrm{Fin}$$
2		vonmblss2.y	$$⊢\phi \to Y\in \mathrm{dom}\mathrm{voln}\left(X\right)$$
3	1	vonmblss	$$⊢\phi \to \mathrm{dom}\mathrm{voln}\left(X\right)\subseteq 𝒫\left({ℝ}^X\right)$$
4	3 2	sseldd	$$⊢\phi \to Y\in 𝒫\left({ℝ}^X\right)$$
5		elpwi	$$⊢Y\in 𝒫\left({ℝ}^X\right)\to Y\subseteq {ℝ}^X$$
6	4 5	syl	$$⊢\phi \to Y\subseteq {ℝ}^X$$