Metamath Proof Explorer

Theorem 2ndcrest

Description: A subspace of a second-countable space is second-countable. (Contributed by Mario Carneiro, 21-Mar-2015)

Ref Expression
Assertion 2ndcrest 
|- ( ( J e. 2ndc /\ A e. V ) -> ( J |`t A ) e. 2ndc )

Proof

Step Hyp Ref Expression
1 is2ndc 
 |-  ( J e. 2ndc <-> E. x e. TopBases ( x ~<_ _om /\ ( topGen ` x ) = J ) )
2 simplr 
 |-  ( ( ( A e. V /\ x e. TopBases ) /\ x ~<_ _om ) -> x e. TopBases )
3 simpll 
 |-  ( ( ( A e. V /\ x e. TopBases ) /\ x ~<_ _om ) -> A e. V )
4 tgrest 
 |-  ( ( x e. TopBases /\ A e. V ) -> ( topGen ` ( x |`t A ) ) = ( ( topGen ` x ) |`t A ) )
5 2 3 4 syl2anc 
 |-  ( ( ( A e. V /\ x e. TopBases ) /\ x ~<_ _om ) -> ( topGen ` ( x |`t A ) ) = ( ( topGen ` x ) |`t A ) )
6 restbas 
 |-  ( x e. TopBases -> ( x |`t A ) e. TopBases )
7 6 ad2antlr 
 |-  ( ( ( A e. V /\ x e. TopBases ) /\ x ~<_ _om ) -> ( x |`t A ) e. TopBases )
8 restval 
 |-  ( ( x e. TopBases /\ A e. V ) -> ( x |`t A ) = ran ( y e. x |-> ( y i^i A ) ) )
9 2 3 8 syl2anc 
 |-  ( ( ( A e. V /\ x e. TopBases ) /\ x ~<_ _om ) -> ( x |`t A ) = ran ( y e. x |-> ( y i^i A ) ) )
10 1stcrestlem 
 |-  ( x ~<_ _om -> ran ( y e. x |-> ( y i^i A ) ) ~<_ _om )
11 10 adantl 
 |-  ( ( ( A e. V /\ x e. TopBases ) /\ x ~<_ _om ) -> ran ( y e. x |-> ( y i^i A ) ) ~<_ _om )
12 9 11 eqbrtrd 
 |-  ( ( ( A e. V /\ x e. TopBases ) /\ x ~<_ _om ) -> ( x |`t A ) ~<_ _om )
13 2ndci 
 |-  ( ( ( x |`t A ) e. TopBases /\ ( x |`t A ) ~<_ _om ) -> ( topGen ` ( x |`t A ) ) e. 2ndc )
14 7 12 13 syl2anc 
 |-  ( ( ( A e. V /\ x e. TopBases ) /\ x ~<_ _om ) -> ( topGen ` ( x |`t A ) ) e. 2ndc )
15 5 14 eqeltrrd 
 |-  ( ( ( A e. V /\ x e. TopBases ) /\ x ~<_ _om ) -> ( ( topGen ` x ) |`t A ) e. 2ndc )
16 oveq1 
 |-  ( ( topGen ` x ) = J -> ( ( topGen ` x ) |`t A ) = ( J |`t A ) )
17 16 eleq1d 
 |-  ( ( topGen ` x ) = J -> ( ( ( topGen ` x ) |`t A ) e. 2ndc <-> ( J |`t A ) e. 2ndc ) )
18 15 17 syl5ibcom 
 |-  ( ( ( A e. V /\ x e. TopBases ) /\ x ~<_ _om ) -> ( ( topGen ` x ) = J -> ( J |`t A ) e. 2ndc ) )
19 18 expimpd 
 |-  ( ( A e. V /\ x e. TopBases ) -> ( ( x ~<_ _om /\ ( topGen ` x ) = J ) -> ( J |`t A ) e. 2ndc ) )
20 19 rexlimdva 
 |-  ( A e. V -> ( E. x e. TopBases ( x ~<_ _om /\ ( topGen ` x ) = J ) -> ( J |`t A ) e. 2ndc ) )
21 1 20 syl5bi 
 |-  ( A e. V -> ( J e. 2ndc -> ( J |`t A ) e. 2ndc ) )
22 21 impcom 
 |-  ( ( J e. 2ndc /\ A e. V ) -> ( J |`t A ) e. 2ndc )