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

Proof

Step Hyp Ref Expression
1 dmovn.1
 |-  ( ph -> X e. Fin )
2 1 ovnf
 |-  ( ph -> ( voln* ` X ) : ~P ( RR ^m X ) --> ( 0 [,] +oo ) )
3 2 fdmd
 |-  ( ph -> dom ( voln* ` X ) = ~P ( RR ^m X ) )