Metamath Proof Explorer


Theorem dmovn

Description: The domain of the Lebesgue outer measure is the power set of the n-dimensional Real numbers. Step (a)(i) of the proof of Proposition 115D (a) of Fremlin1 p. 30. (Contributed by Glauco Siliprandi, 24-Dec-2020)

Ref Expression
Hypothesis dmovn.1 φ X Fin
Assertion dmovn φ dom voln* X = 𝒫 X

Proof

Step Hyp Ref Expression
1 dmovn.1 φ X Fin
2 1 ovnf φ voln* X : 𝒫 X 0 +∞
3 2 fdmd φ dom voln* X = 𝒫 X