Theorem vonmblss

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

	Ref	Expression
Hypothesis	vonmblss.1	$$⊢\phi \to X\in \mathrm{Fin}$$
Assertion	vonmblss	$$⊢\phi \to \mathrm{dom}\mathrm{voln}\left(X\right)\subseteq 𝒫\left({ℝ}^X\right)$$

Proof

Step	Hyp	Ref	Expression
1		vonmblss.1	$$⊢\phi \to X\in \mathrm{Fin}$$
2	1	dmvon	$$⊢\phi \to \mathrm{dom}\mathrm{voln}\left(X\right)=\mathrm{CaraGen}\left(\mathrm{voln*}\left(X\right)\right)$$
3	1	ovnome	$$⊢\phi \to \mathrm{voln*}\left(X\right)\in \mathrm{OutMeas}$$
4		eqid	$$⊢\mathrm{CaraGen}\left(\mathrm{voln*}\left(X\right)\right)=\mathrm{CaraGen}\left(\mathrm{voln*}\left(X\right)\right)$$
5	4	caragenss	$$⊢\mathrm{voln*}\left(X\right)\in \mathrm{OutMeas}\to \mathrm{CaraGen}\left(\mathrm{voln*}\left(X\right)\right)\subseteq \mathrm{dom}\mathrm{voln*}\left(X\right)$$
6	3 5	syl	$$⊢\phi \to \mathrm{CaraGen}\left(\mathrm{voln*}\left(X\right)\right)\subseteq \mathrm{dom}\mathrm{voln*}\left(X\right)$$
7	1	dmovn	$$⊢\phi \to \mathrm{dom}\mathrm{voln*}\left(X\right)=𝒫\left({ℝ}^X\right)$$
8	6 7	sseqtrd	$$⊢\phi \to \mathrm{CaraGen}\left(\mathrm{voln*}\left(X\right)\right)\subseteq 𝒫\left({ℝ}^X\right)$$
9	2 8	eqsstrd	$$⊢\phi \to \mathrm{dom}\mathrm{voln}\left(X\right)\subseteq 𝒫\left({ℝ}^X\right)$$