Metamath Proof Explorer

Theorem 2ndci

Description: A countable basis generates a second-countable topology. (Contributed by Mario Carneiro, 21-Mar-2015)

Ref Expression
Assertion 2ndci 
|- ( ( B e. TopBases /\ B ~<_ _om ) -> ( topGen ` B ) e. 2ndc )

Proof

Step Hyp Ref Expression
1 simpl 
 |-  ( ( B e. TopBases /\ B ~<_ _om ) -> B e. TopBases )
2 simpr 
 |-  ( ( B e. TopBases /\ B ~<_ _om ) -> B ~<_ _om )
3 eqidd 
 |-  ( ( B e. TopBases /\ B ~<_ _om ) -> ( topGen ` B ) = ( topGen ` B ) )
4 breq1 
 |-  ( x = B -> ( x ~<_ _om <-> B ~<_ _om ) )
5 fveqeq2 
 |-  ( x = B -> ( ( topGen ` x ) = ( topGen ` B ) <-> ( topGen ` B ) = ( topGen ` B ) ) )
6 4 5 anbi12d 
 |-  ( x = B -> ( ( x ~<_ _om /\ ( topGen ` x ) = ( topGen ` B ) ) <-> ( B ~<_ _om /\ ( topGen ` B ) = ( topGen ` B ) ) ) )
7 6 rspcev 
 |-  ( ( B e. TopBases /\ ( B ~<_ _om /\ ( topGen ` B ) = ( topGen ` B ) ) ) -> E. x e. TopBases ( x ~<_ _om /\ ( topGen ` x ) = ( topGen ` B ) ) )
8 1 2 3 7 syl12anc 
 |-  ( ( B e. TopBases /\ B ~<_ _om ) -> E. x e. TopBases ( x ~<_ _om /\ ( topGen ` x ) = ( topGen ` B ) ) )
9 is2ndc 
 |-  ( ( topGen ` B ) e. 2ndc <-> E. x e. TopBases ( x ~<_ _om /\ ( topGen ` x ) = ( topGen ` B ) ) )
10 8 9 sylibr 
 |-  ( ( B e. TopBases /\ B ~<_ _om ) -> ( topGen ` B ) e. 2ndc )