Theorem unidmvon

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

	Ref	Expression
Hypotheses	unidmvon.x	|- ( ph -> X e. Fin )
	unidmvon.s	|- S = dom ( voln ` X )
Assertion	unidmvon	|- ( ph -> U. S = ( RR ^m X ) )

Proof

Step	Hyp	Ref	Expression
1		unidmvon.x	|- ( ph -> X e. Fin )
2		unidmvon.s	|- S = dom ( voln ` X )
3	2	a1i	|- ( ph -> S = dom ( voln ` X ) )
4	1	dmvon	|- ( ph -> dom ( voln ` X ) = ( CaraGen ` ( voln* ` X ) ) )
5	3 4	eqtrd	|- ( ph -> S = ( CaraGen ` ( voln* ` X ) ) )
6	5	unieqd	|- ( ph -> U. S = U. ( CaraGen ` ( voln* ` X ) ) )
7	1	ovnome	|- ( ph -> ( voln* ` X ) e. OutMeas )
8		eqid	|- ( CaraGen ` ( voln* ` X ) ) = ( CaraGen ` ( voln* ` X ) )
9	7 8	caragenuni	|- ( ph -> U. ( CaraGen ` ( voln* ` X ) ) = U. dom ( voln* ` X ) )
10	1	unidmovn	|- ( ph -> U. dom ( voln* ` X ) = ( RR ^m X ) )
11	6 9 10	3eqtrd	|- ( ph -> U. S = ( RR ^m X ) )