Theorem unidmovn

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

	Ref	Expression
Hypothesis	unidmovn.1	|- ( ph -> X e. Fin )
Assertion	unidmovn	|- ( ph -> U. dom ( voln* ` X ) = ( RR ^m X ) )

Proof

Step	Hyp	Ref	Expression
1		unidmovn.1	|- ( ph -> X e. Fin )
2	1	dmovn	|- ( ph -> dom ( voln* ` X ) = ~P ( RR ^m X ) )
3	2	unieqd	|- ( ph -> U. dom ( voln* ` X ) = U. ~P ( RR ^m X ) )
4		unipw	|- U. ~P ( RR ^m X ) = ( RR ^m X )
5	4	a1i	|- ( ph -> U. ~P ( RR ^m X ) = ( RR ^m X ) )
6	3 5	eqtrd	|- ( ph -> U. dom ( voln* ` X ) = ( RR ^m X ) )