Metamath Proof Explorer


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 φ X Fin
vonmblss2.y φ Y dom voln X
Assertion vonmblss2 φ Y X

Proof

Step Hyp Ref Expression
1 vonmblss2.x φ X Fin
2 vonmblss2.y φ Y dom voln X
3 1 vonmblss φ dom voln X 𝒫 X
4 3 2 sseldd φ Y 𝒫 X
5 elpwi Y 𝒫 X Y X
6 4 5 syl φ Y X