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	$$⊢\phi \to X\in \mathrm{Fin}$$
Assertion	dmovn	$$⊢\phi \to \mathrm{dom}\mathrm{voln*}\left(X\right)=𝒫\left({ℝ}^X\right)$$

Proof

Step	Hyp	Ref	Expression
1		dmovn.1	$$⊢\phi \to X\in \mathrm{Fin}$$
2	1	ovnf	$$⊢\phi \to \mathrm{voln*}\left(X\right):𝒫\left({ℝ}^X\right)⟶\left[0,\mathrm{+\infty }\right]$$
3	2	fdmd	$$⊢\phi \to \mathrm{dom}\mathrm{voln*}\left(X\right)=𝒫\left({ℝ}^X\right)$$