Metamath Proof Explorer

Theorem resttop

Description: A subspace topology is a topology. Definition of subspace topology in Munkres p. 89. A is normally a subset of the base set of J . (Contributed by FL, 15-Apr-2007) (Revised by Mario Carneiro, 1-May-2015)

Ref Expression
Assertion resttop 
|- ( ( J e. Top /\ A e. V ) -> ( J |`t A ) e. Top )

Proof

Step Hyp Ref Expression
1 tgrest 
 |-  ( ( J e. Top /\ A e. V ) -> ( topGen ` ( J |`t A ) ) = ( ( topGen ` J ) |`t A ) )
2 tgtop 
 |-  ( J e. Top -> ( topGen ` J ) = J )
3 2 adantr 
 |-  ( ( J e. Top /\ A e. V ) -> ( topGen ` J ) = J )
4 3 oveq1d 
 |-  ( ( J e. Top /\ A e. V ) -> ( ( topGen ` J ) |`t A ) = ( J |`t A ) )
5 1 4 eqtrd 
 |-  ( ( J e. Top /\ A e. V ) -> ( topGen ` ( J |`t A ) ) = ( J |`t A ) )
6 topbas 
 |-  ( J e. Top -> J e. TopBases )
7 6 adantr 
 |-  ( ( J e. Top /\ A e. V ) -> J e. TopBases )
8 restbas 
 |-  ( J e. TopBases -> ( J |`t A ) e. TopBases )
9 tgcl 
 |-  ( ( J |`t A ) e. TopBases -> ( topGen ` ( J |`t A ) ) e. Top )
10 7 8 9 3syl 
 |-  ( ( J e. Top /\ A e. V ) -> ( topGen ` ( J |`t A ) ) e. Top )
11 5 10 eqeltrrd 
 |-  ( ( J e. Top /\ A e. V ) -> ( J |`t A ) e. Top )