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 
|- BrSiga e. ( sigaGen " Top )

Proof

Step Hyp Ref Expression
1 df-brsiga 
 |-  BrSiga = ( sigaGen ` ( topGen ` ran (,) ) )
2 retop 
 |-  ( topGen ` ran (,) ) e. Top
3 df-sigagen 
 |-  sigaGen = ( x e. _V |-> |^| { s e. ( sigAlgebra ` U. x ) | x C_ s } )
4 3 funmpt2 
 |-  Fun sigaGen
5 fvex 
 |-  ( topGen ` ran (,) ) e. _V
6 sigagensiga 
 |-  ( ( topGen ` ran (,) ) e. _V -> ( sigaGen ` ( topGen ` ran (,) ) ) e. ( sigAlgebra ` U. ( topGen ` ran (,) ) ) )
7 elrnsiga 
 |-  ( ( sigaGen ` ( topGen ` ran (,) ) ) e. ( sigAlgebra ` U. ( topGen ` ran (,) ) ) -> ( sigaGen ` ( topGen ` ran (,) ) ) e. U. ran sigAlgebra )
8 5 6 7 mp2b 
 |-  ( sigaGen ` ( topGen ` ran (,) ) ) e. U. ran sigAlgebra
9 0elsiga 
 |-  ( ( sigaGen ` ( topGen ` ran (,) ) ) e. U. ran sigAlgebra -> (/) e. ( sigaGen ` ( topGen ` ran (,) ) ) )
10 elfvdm 
 |-  ( (/) e. ( sigaGen ` ( topGen ` ran (,) ) ) -> ( topGen ` ran (,) ) e. dom sigaGen )
11 8 9 10 mp2b 
 |-  ( topGen ` ran (,) ) e. dom sigaGen
12 funfvima 
 |-  ( ( Fun sigaGen /\ ( topGen ` ran (,) ) e. dom sigaGen ) -> ( ( topGen ` ran (,) ) e. Top -> ( sigaGen ` ( topGen ` ran (,) ) ) e. ( sigaGen " Top ) ) )
13 4 11 12 mp2an 
 |-  ( ( topGen ` ran (,) ) e. Top -> ( sigaGen ` ( topGen ` ran (,) ) ) e. ( sigaGen " Top ) )
14 2 13 ax-mp 
 |-  ( sigaGen ` ( topGen ` ran (,) ) ) e. ( sigaGen " Top )
15 1 14 eqeltri 
 |-  BrSiga e. ( sigaGen " Top )