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	$$⊢\phi \to X\in \mathrm{Fin}$$
Assertion	rrnmbl	$$⊢\phi \to {ℝ}^X\in \mathrm{dom}\mathrm{voln}\left(X\right)$$

Proof

Step	Hyp	Ref	Expression
1		rrnmbl.1	$$⊢\phi \to X\in \mathrm{Fin}$$
2	1	ovnome	$$⊢\phi \to \mathrm{voln*}\left(X\right)\in \mathrm{OutMeas}$$
3		eqid	$$⊢\bigcup \mathrm{dom}\mathrm{voln*}\left(X\right)=\bigcup \mathrm{dom}\mathrm{voln*}\left(X\right)$$
4		eqid	$$⊢\mathrm{CaraGen}\left(\mathrm{voln*}\left(X\right)\right)=\mathrm{CaraGen}\left(\mathrm{voln*}\left(X\right)\right)$$
5	2 3 4	caragenunidm	$$⊢\phi \to \bigcup \mathrm{dom}\mathrm{voln*}\left(X\right)\in \mathrm{CaraGen}\left(\mathrm{voln*}\left(X\right)\right)$$
6	1	dmovn	$$⊢\phi \to \mathrm{dom}\mathrm{voln*}\left(X\right)=𝒫\left({ℝ}^X\right)$$
7	6	unieqd	$$⊢\phi \to \bigcup \mathrm{dom}\mathrm{voln*}\left(X\right)=\bigcup 𝒫\left({ℝ}^X\right)$$
8		unipw	$$⊢\bigcup 𝒫\left({ℝ}^X\right)={ℝ}^X$$
9	8	a1i	$$⊢\phi \to \bigcup 𝒫\left({ℝ}^X\right)={ℝ}^X$$
10	7 9	eqtr2d	$$⊢\phi \to {ℝ}^X=\bigcup \mathrm{dom}\mathrm{voln*}\left(X\right)$$
11	1	dmvon	$$⊢\phi \to \mathrm{dom}\mathrm{voln}\left(X\right)=\mathrm{CaraGen}\left(\mathrm{voln*}\left(X\right)\right)$$
12	10 11	eleq12d	$$⊢\phi \to \left({ℝ}^X\in \mathrm{dom}\mathrm{voln}\left(X\right)\leftrightarrow \bigcup \mathrm{dom}\mathrm{voln*}\left(X\right)\in \mathrm{CaraGen}\left(\mathrm{voln*}\left(X\right)\right)\right)$$
13	5 12	mpbird	$$⊢\phi \to {ℝ}^X\in \mathrm{dom}\mathrm{voln}\left(X\right)$$