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 )