Metamath Proof Explorer


Theorem borelmbl

Description: All Borel subsets of the n-dimensional Real numbers are Lebesgue measurable. This is Proposition 115G (b) of Fremlin1 p. 32. See also Definition 111G (d) of Fremlin1 p. 13. (Contributed by Glauco Siliprandi, 3-Jan-2021)

Ref Expression
Hypotheses borelmbl.x φ X Fin
borelmbl.s S = dom voln X
borelmbl.b B = SalGen TopOpen X
Assertion borelmbl φ B S

Proof

Step Hyp Ref Expression
1 borelmbl.x φ X Fin
2 borelmbl.s S = dom voln X
3 borelmbl.b B = SalGen TopOpen X
4 fvexd φ TopOpen X V
5 1 2 dmovnsal φ S SAlg
6 1 adantr φ y TopOpen X X Fin
7 simpr φ y TopOpen X y TopOpen X
8 6 2 7 opnvonmbl φ y TopOpen X y S
9 8 ssd φ TopOpen X S
10 eqid dom voln X = dom voln X
11 1 10 unidmvon φ dom voln X = X
12 2 unieqi S = dom voln X
13 12 a1i φ S = dom voln X
14 rrxunitopnfi X Fin TopOpen X = X
15 1 14 syl φ TopOpen X = X
16 11 13 15 3eqtr4d φ S = TopOpen X
17 4 3 5 9 16 salgenss φ B S