Metamath Proof Explorer

Theorem tgtopon

Description: A basis generates a topology on U. B . (Contributed by Mario Carneiro, 14-Aug-2015)

Ref Expression
Assertion tgtopon 
|- ( B e. TopBases -> ( topGen ` B ) e. ( TopOn ` U. B ) )

Proof

Step Hyp Ref Expression
1 tgcl 
 |-  ( B e. TopBases -> ( topGen ` B ) e. Top )
2 unitg 
 |-  ( B e. TopBases -> U. ( topGen ` B ) = U. B )
3 2 eqcomd 
 |-  ( B e. TopBases -> U. B = U. ( topGen ` B ) )
4 istopon 
 |-  ( ( topGen ` B ) e. ( TopOn ` U. B ) <-> ( ( topGen ` B ) e. Top /\ U. B = U. ( topGen ` B ) ) )
5 1 3 4 sylanbrc 
 |-  ( B e. TopBases -> ( topGen ` B ) e. ( TopOn ` U. B ) )