Theorem rrnmbl

Description: The set of n-dimensional Real numbers is Lebesgue measurable. (Contributed by Glauco Siliprandi, 24-Dec-2020)

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

Proof

Step	Hyp	Ref	Expression
1		rrnmbl.1	|- ( ph -> X e. Fin )
2	1	ovnome	|- ( ph -> ( voln* ` X ) e. OutMeas )
3		eqid	|- U. dom ( voln* ` X ) = U. dom ( voln* ` X )
4		eqid	|- ( CaraGen ` ( voln* ` X ) ) = ( CaraGen ` ( voln* ` X ) )
5	2 3 4	caragenunidm	|- ( ph -> U. dom ( voln* ` X ) e. ( CaraGen ` ( voln* ` X ) ) )
6	1	dmovn	|- ( ph -> dom ( voln* ` X ) = ~P ( RR ^m X ) )
7	6	unieqd	|- ( ph -> U. dom ( voln* ` X ) = U. ~P ( RR ^m X ) )
8		unipw	|- U. ~P ( RR ^m X ) = ( RR ^m X )
9	8	a1i	|- ( ph -> U. ~P ( RR ^m X ) = ( RR ^m X ) )
10	7 9	eqtr2d	|- ( ph -> ( RR ^m X ) = U. dom ( voln* ` X ) )
11	1	dmvon	|- ( ph -> dom ( voln ` X ) = ( CaraGen ` ( voln* ` X ) ) )
12	10 11	eleq12d	|- ( ph -> ( ( RR ^m X ) e. dom ( voln ` X ) <-> U. dom ( voln* ` X ) e. ( CaraGen ` ( voln* ` X ) ) ) )
13	5 12	mpbird	|- ( ph -> ( RR ^m X ) e. dom ( voln ` X ) )