Metamath Proof Explorer

Theorem unibrsiga

Description: The union of the Borel Algebra is the set of real numbers. (Contributed by Thierry Arnoux, 21-Jan-2017)

Ref Expression
Assertion unibrsiga 
|- U. BrSiga = RR

Proof

Step Hyp Ref Expression
1 retop 
 |-  ( topGen ` ran (,) ) e. Top
2 unisg 
 |-  ( ( topGen ` ran (,) ) e. Top -> U. ( sigaGen ` ( topGen ` ran (,) ) ) = U. ( topGen ` ran (,) ) )
3 1 2 ax-mp 
 |-  U. ( sigaGen ` ( topGen ` ran (,) ) ) = U. ( topGen ` ran (,) )
4 df-brsiga 
 |-  BrSiga = ( sigaGen ` ( topGen ` ran (,) ) )
5 4 unieqi 
 |-  U. BrSiga = U. ( sigaGen ` ( topGen ` ran (,) ) )
6 uniretop 
 |-  RR = U. ( topGen ` ran (,) )
7 3 5 6 3eqtr4i 
 |-  U. BrSiga = RR