# 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 )`
` |-  ( ( 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 )`
` |-  ( ( J e. Top /\ A e. V ) -> J e. TopBases )`
` |-  ( J e. TopBases -> ( J |`t A ) e. TopBases )`
` |-  ( ( J |`t A ) e. TopBases -> ( topGen ` ( J |`t A ) ) e. Top )`
` |-  ( ( J e. Top /\ A e. V ) -> ( topGen ` ( J |`t A ) ) e. Top )`
` |-  ( ( J e. Top /\ A e. V ) -> ( J |`t A ) e. Top )`