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	⊢ ( 𝜑 → 𝑋 ∈ Fin )
Assertion	dmovn	⊢ ( 𝜑 → dom ( voln* ‘ 𝑋 ) = 𝒫 ( ℝ ↑m 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		dmovn.1	⊢ ( 𝜑 → 𝑋 ∈ Fin )
2	1	ovnf	⊢ ( 𝜑 → ( voln* ‘ 𝑋 ) : 𝒫 ( ℝ ↑m 𝑋 ) ⟶ ( 0 [,] +∞ ) )
3	2	fdmd	⊢ ( 𝜑 → dom ( voln* ‘ 𝑋 ) = 𝒫 ( ℝ ↑m 𝑋 ) )