Theorem unidmovn

Description: Base set of the n-dimensional Lebesgue outer measure. (Contributed by Glauco Siliprandi, 24-Dec-2020)

	Ref	Expression
Hypothesis	unidmovn.1	$$⊢\phi \to X\in \mathrm{Fin}$$
Assertion	unidmovn	$$⊢\phi \to \bigcup \mathrm{dom}\mathrm{voln*}\left(X\right)={ℝ}^X$$

Proof

Step	Hyp	Ref	Expression
1		unidmovn.1	$$⊢\phi \to X\in \mathrm{Fin}$$
2	1	dmovn	$$⊢\phi \to \mathrm{dom}\mathrm{voln*}\left(X\right)=𝒫\left({ℝ}^X\right)$$
3	2	unieqd	$$⊢\phi \to \bigcup \mathrm{dom}\mathrm{voln*}\left(X\right)=\bigcup 𝒫\left({ℝ}^X\right)$$
4		unipw	$$⊢\bigcup 𝒫\left({ℝ}^X\right)={ℝ}^X$$
5	4	a1i	$$⊢\phi \to \bigcup 𝒫\left({ℝ}^X\right)={ℝ}^X$$
6	3 5	eqtrd	$$⊢\phi \to \bigcup \mathrm{dom}\mathrm{voln*}\left(X\right)={ℝ}^X$$