Theorem unidmvon

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

	Ref	Expression
Hypotheses	unidmvon.x	$$⊢\phi \to X\in \mathrm{Fin}$$
	unidmvon.s	$$⊢S=\mathrm{dom}\mathrm{voln}\left(X\right)$$
Assertion	unidmvon	$$⊢\phi \to \bigcup S={ℝ}^X$$

Proof

Step	Hyp	Ref	Expression
1		unidmvon.x	$$⊢\phi \to X\in \mathrm{Fin}$$
2		unidmvon.s	$$⊢S=\mathrm{dom}\mathrm{voln}\left(X\right)$$
3	2	a1i	$$⊢\phi \to S=\mathrm{dom}\mathrm{voln}\left(X\right)$$
4	1	dmvon	$$⊢\phi \to \mathrm{dom}\mathrm{voln}\left(X\right)=\mathrm{CaraGen}\left(\mathrm{voln*}\left(X\right)\right)$$
5	3 4	eqtrd	$$⊢\phi \to S=\mathrm{CaraGen}\left(\mathrm{voln*}\left(X\right)\right)$$
6	5	unieqd	$$⊢\phi \to \bigcup S=\bigcup \mathrm{CaraGen}\left(\mathrm{voln*}\left(X\right)\right)$$
7	1	ovnome	$$⊢\phi \to \mathrm{voln*}\left(X\right)\in \mathrm{OutMeas}$$
8		eqid	$$⊢\mathrm{CaraGen}\left(\mathrm{voln*}\left(X\right)\right)=\mathrm{CaraGen}\left(\mathrm{voln*}\left(X\right)\right)$$
9	7 8	caragenuni	$$⊢\phi \to \bigcup \mathrm{CaraGen}\left(\mathrm{voln*}\left(X\right)\right)=\bigcup \mathrm{dom}\mathrm{voln*}\left(X\right)$$
10	1	unidmovn	$$⊢\phi \to \bigcup \mathrm{dom}\mathrm{voln*}\left(X\right)={ℝ}^X$$
11	6 9 10	3eqtrd	$$⊢\phi \to \bigcup S={ℝ}^X$$