Metamath Proof Explorer


Theorem brsiga

Description: The Borel Algebra on real numbers is a Borel sigma-algebra. (Contributed by Thierry Arnoux, 27-Dec-2016)

Ref Expression
Assertion brsiga 𝔅 𝛔 Top

Proof

Step Hyp Ref Expression
1 df-brsiga 𝔅 = 𝛔 topGen ran .
2 retop topGen ran . Top
3 df-sigagen 𝛔 = x V s sigAlgebra x | x s
4 3 funmpt2 Fun 𝛔
5 fvex topGen ran . V
6 sigagensiga topGen ran . V 𝛔 topGen ran . sigAlgebra topGen ran .
7 elrnsiga 𝛔 topGen ran . sigAlgebra topGen ran . 𝛔 topGen ran . ran sigAlgebra
8 5 6 7 mp2b 𝛔 topGen ran . ran sigAlgebra
9 0elsiga 𝛔 topGen ran . ran sigAlgebra 𝛔 topGen ran .
10 elfvdm 𝛔 topGen ran . topGen ran . dom 𝛔
11 8 9 10 mp2b topGen ran . dom 𝛔
12 funfvima Fun 𝛔 topGen ran . dom 𝛔 topGen ran . Top 𝛔 topGen ran . 𝛔 Top
13 4 11 12 mp2an topGen ran . Top 𝛔 topGen ran . 𝛔 Top
14 2 13 ax-mp 𝛔 topGen ran . 𝛔 Top
15 1 14 eqeltri 𝔅 𝛔 Top