Metamath Proof Explorer

Theorem brsigarn

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

Ref Expression
Assertion brsigarn 
|- BrSiga e. ( sigAlgebra ` RR )

Proof

Step Hyp Ref Expression
1 fvex 
 |-  ( topGen ` ran (,) ) e. _V
2 sigagensiga 
 |-  ( ( topGen ` ran (,) ) e. _V -> ( sigaGen ` ( topGen ` ran (,) ) ) e. ( sigAlgebra ` U. ( topGen ` ran (,) ) ) )
3 1 2 ax-mp 
 |-  ( sigaGen ` ( topGen ` ran (,) ) ) e. ( sigAlgebra ` U. ( topGen ` ran (,) ) )
4 df-brsiga 
 |-  BrSiga = ( sigaGen ` ( topGen ` ran (,) ) )
5 uniretop 
 |-  RR = U. ( topGen ` ran (,) )
6 5 fveq2i 
 |-  ( sigAlgebra ` RR ) = ( sigAlgebra ` U. ( topGen ` ran (,) ) )
7 3 4 6 3eltr4i 
 |-  BrSiga e. ( sigAlgebra ` RR )