Metamath Proof Explorer

Theorem 2ndcsb

Description: Having a countable subbase is a sufficient condition for second-countability. (Contributed by Jeff Hankins, 17-Jan-2010) (Proof shortened by Mario Carneiro, 21-Mar-2015)

Ref Expression
Assertion 2ndcsb 
|- ( J e. 2ndc <-> E. x ( x ~<_ _om /\ ( topGen ` ( fi ` x ) ) = J ) )

Proof

Step Hyp Ref Expression
1 is2ndc 
 |-  ( J e. 2ndc <-> E. x e. TopBases ( x ~<_ _om /\ ( topGen ` x ) = J ) )
2 df-rex 
 |-  ( E. x e. TopBases ( x ~<_ _om /\ ( topGen ` x ) = J ) <-> E. x ( x e. TopBases /\ ( x ~<_ _om /\ ( topGen ` x ) = J ) ) )
3 simprl 
 |-  ( ( x e. TopBases /\ ( x ~<_ _om /\ ( topGen ` x ) = J ) ) -> x ~<_ _om )
4 ssfii 
 |-  ( x e. TopBases -> x C_ ( fi ` x ) )
5 fvex 
 |-  ( topGen ` x ) e. _V
6 bastg 
 |-  ( x e. TopBases -> x C_ ( topGen ` x ) )
7 6 adantr 
 |-  ( ( x e. TopBases /\ ( x ~<_ _om /\ ( topGen ` x ) = J ) ) -> x C_ ( topGen ` x ) )
8 fiss 
 |-  ( ( ( topGen ` x ) e. _V /\ x C_ ( topGen ` x ) ) -> ( fi ` x ) C_ ( fi ` ( topGen ` x ) ) )
9 5 7 8 sylancr 
 |-  ( ( x e. TopBases /\ ( x ~<_ _om /\ ( topGen ` x ) = J ) ) -> ( fi ` x ) C_ ( fi ` ( topGen ` x ) ) )
10 tgcl 
 |-  ( x e. TopBases -> ( topGen ` x ) e. Top )
11 10 adantr 
 |-  ( ( x e. TopBases /\ ( x ~<_ _om /\ ( topGen ` x ) = J ) ) -> ( topGen ` x ) e. Top )
12 fitop 
 |-  ( ( topGen ` x ) e. Top -> ( fi ` ( topGen ` x ) ) = ( topGen ` x ) )
13 11 12 syl 
 |-  ( ( x e. TopBases /\ ( x ~<_ _om /\ ( topGen ` x ) = J ) ) -> ( fi ` ( topGen ` x ) ) = ( topGen ` x ) )
14 9 13 sseqtrd 
 |-  ( ( x e. TopBases /\ ( x ~<_ _om /\ ( topGen ` x ) = J ) ) -> ( fi ` x ) C_ ( topGen ` x ) )
15 2basgen 
 |-  ( ( x C_ ( fi ` x ) /\ ( fi ` x ) C_ ( topGen ` x ) ) -> ( topGen ` x ) = ( topGen ` ( fi ` x ) ) )
16 4 14 15 syl2an2r 
 |-  ( ( x e. TopBases /\ ( x ~<_ _om /\ ( topGen ` x ) = J ) ) -> ( topGen ` x ) = ( topGen ` ( fi ` x ) ) )
17 simprr 
 |-  ( ( x e. TopBases /\ ( x ~<_ _om /\ ( topGen ` x ) = J ) ) -> ( topGen ` x ) = J )
18 16 17 eqtr3d 
 |-  ( ( x e. TopBases /\ ( x ~<_ _om /\ ( topGen ` x ) = J ) ) -> ( topGen ` ( fi ` x ) ) = J )
19 3 18 jca 
 |-  ( ( x e. TopBases /\ ( x ~<_ _om /\ ( topGen ` x ) = J ) ) -> ( x ~<_ _om /\ ( topGen ` ( fi ` x ) ) = J ) )
20 19 eximi 
 |-  ( E. x ( x e. TopBases /\ ( x ~<_ _om /\ ( topGen ` x ) = J ) ) -> E. x ( x ~<_ _om /\ ( topGen ` ( fi ` x ) ) = J ) )
21 2 20 sylbi 
 |-  ( E. x e. TopBases ( x ~<_ _om /\ ( topGen ` x ) = J ) -> E. x ( x ~<_ _om /\ ( topGen ` ( fi ` x ) ) = J ) )
22 1 21 sylbi 
 |-  ( J e. 2ndc -> E. x ( x ~<_ _om /\ ( topGen ` ( fi ` x ) ) = J ) )
23 fibas 
 |-  ( fi ` x ) e. TopBases
24 simpl 
 |-  ( ( x ~<_ _om /\ ( topGen ` ( fi ` x ) ) = J ) -> x ~<_ _om )
25 fictb 
 |-  ( x e. _V -> ( x ~<_ _om <-> ( fi ` x ) ~<_ _om ) )
26 25 elv 
 |-  ( x ~<_ _om <-> ( fi ` x ) ~<_ _om )
27 24 26 sylib 
 |-  ( ( x ~<_ _om /\ ( topGen ` ( fi ` x ) ) = J ) -> ( fi ` x ) ~<_ _om )
28 simpr 
 |-  ( ( x ~<_ _om /\ ( topGen ` ( fi ` x ) ) = J ) -> ( topGen ` ( fi ` x ) ) = J )
29 27 28 jca 
 |-  ( ( x ~<_ _om /\ ( topGen ` ( fi ` x ) ) = J ) -> ( ( fi ` x ) ~<_ _om /\ ( topGen ` ( fi ` x ) ) = J ) )
30 breq1 
 |-  ( y = ( fi ` x ) -> ( y ~<_ _om <-> ( fi ` x ) ~<_ _om ) )
31 fveqeq2 
 |-  ( y = ( fi ` x ) -> ( ( topGen ` y ) = J <-> ( topGen ` ( fi ` x ) ) = J ) )
32 30 31 anbi12d 
 |-  ( y = ( fi ` x ) -> ( ( y ~<_ _om /\ ( topGen ` y ) = J ) <-> ( ( fi ` x ) ~<_ _om /\ ( topGen ` ( fi ` x ) ) = J ) ) )
33 32 rspcev 
 |-  ( ( ( fi ` x ) e. TopBases /\ ( ( fi ` x ) ~<_ _om /\ ( topGen ` ( fi ` x ) ) = J ) ) -> E. y e. TopBases ( y ~<_ _om /\ ( topGen ` y ) = J ) )
34 23 29 33 sylancr 
 |-  ( ( x ~<_ _om /\ ( topGen ` ( fi ` x ) ) = J ) -> E. y e. TopBases ( y ~<_ _om /\ ( topGen ` y ) = J ) )
35 is2ndc 
 |-  ( J e. 2ndc <-> E. y e. TopBases ( y ~<_ _om /\ ( topGen ` y ) = J ) )
36 34 35 sylibr 
 |-  ( ( x ~<_ _om /\ ( topGen ` ( fi ` x ) ) = J ) -> J e. 2ndc )
37 36 exlimiv 
 |-  ( E. x ( x ~<_ _om /\ ( topGen ` ( fi ` x ) ) = J ) -> J e. 2ndc )
38 22 37 impbii 
 |-  ( J e. 2ndc <-> E. x ( x ~<_ _om /\ ( topGen ` ( fi ` x ) ) = J ) )