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	|- ( ph -> X e. Fin )
Assertion	vonmblss	|- ( ph -> dom ( voln ` X ) C_ ~P ( RR ^m X ) )

Proof

Step	Hyp	Ref	Expression
1		vonmblss.1	|- ( ph -> X e. Fin )
2	1	dmvon	|- ( ph -> dom ( voln ` X ) = ( CaraGen ` ( voln* ` X ) ) )
3	1	ovnome	|- ( ph -> ( voln* ` X ) e. OutMeas )
4		eqid	|- ( CaraGen ` ( voln* ` X ) ) = ( CaraGen ` ( voln* ` X ) )
5	4	caragenss	|- ( ( voln* ` X ) e. OutMeas -> ( CaraGen ` ( voln* ` X ) ) C_ dom ( voln* ` X ) )
6	3 5	syl	|- ( ph -> ( CaraGen ` ( voln* ` X ) ) C_ dom ( voln* ` X ) )
7	1	dmovn	|- ( ph -> dom ( voln* ` X ) = ~P ( RR ^m X ) )
8	6 7	sseqtrd	|- ( ph -> ( CaraGen ` ( voln* ` X ) ) C_ ~P ( RR ^m X ) )
9	2 8	eqsstrd	|- ( ph -> dom ( voln ` X ) C_ ~P ( RR ^m X ) )