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	|- ( ph -> X e. Fin )
	vonmblss2.y	|- ( ph -> Y e. dom ( voln ` X ) )
Assertion	vonmblss2	|- ( ph -> Y C_ ( RR ^m X ) )

Proof

Step	Hyp	Ref	Expression
1		vonmblss2.x	|- ( ph -> X e. Fin )
2		vonmblss2.y	|- ( ph -> Y e. dom ( voln ` X ) )
3	1	vonmblss	|- ( ph -> dom ( voln ` X ) C_ ~P ( RR ^m X ) )
4	3 2	sseldd	|- ( ph -> Y e. ~P ( RR ^m X ) )
5		elpwi	|- ( Y e. ~P ( RR ^m X ) -> Y C_ ( RR ^m X ) )
6	4 5	syl	|- ( ph -> Y C_ ( RR ^m X ) )