Metamath Proof Explorer


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 φ X Fin
Assertion rrnmbl φ X dom voln X

Proof

Step Hyp Ref Expression
1 rrnmbl.1 φ X Fin
2 1 ovnome φ voln* X OutMeas
3 eqid dom voln* X = dom voln* X
4 eqid CaraGen voln* X = CaraGen voln* X
5 2 3 4 caragenunidm φ dom voln* X CaraGen voln* X
6 1 dmovn φ dom voln* X = 𝒫 X
7 6 unieqd φ dom voln* X = 𝒫 X
8 unipw 𝒫 X = X
9 8 a1i φ 𝒫 X = X
10 7 9 eqtr2d φ X = dom voln* X
11 1 dmvon φ dom voln X = CaraGen voln* X
12 10 11 eleq12d φ X dom voln X dom voln* X CaraGen voln* X
13 5 12 mpbird φ X dom voln X