# Metamath Proof Explorer

## Theorem restsn

Description: The only subspace topology induced by the topology { (/) } . (Contributed by FL, 5-Jan-2009) (Revised by Mario Carneiro, 15-Dec-2013)

Ref Expression
Assertion restsn
`|- ( A e. V -> ( { (/) } |`t A ) = { (/) } )`

### Proof

Step Hyp Ref Expression
1 sn0top
` |-  { (/) } e. Top`
2 elrest
` |-  ( ( { (/) } e. Top /\ A e. V ) -> ( x e. ( { (/) } |`t A ) <-> E. y e. { (/) } x = ( y i^i A ) ) )`
3 1 2 mpan
` |-  ( A e. V -> ( x e. ( { (/) } |`t A ) <-> E. y e. { (/) } x = ( y i^i A ) ) )`
4 0ex
` |-  (/) e. _V`
5 ineq1
` |-  ( y = (/) -> ( y i^i A ) = ( (/) i^i A ) )`
6 0in
` |-  ( (/) i^i A ) = (/)`
7 5 6 syl6eq
` |-  ( y = (/) -> ( y i^i A ) = (/) )`
8 7 eqeq2d
` |-  ( y = (/) -> ( x = ( y i^i A ) <-> x = (/) ) )`
9 4 8 rexsn
` |-  ( E. y e. { (/) } x = ( y i^i A ) <-> x = (/) )`
10 velsn
` |-  ( x e. { (/) } <-> x = (/) )`
11 9 10 bitr4i
` |-  ( E. y e. { (/) } x = ( y i^i A ) <-> x e. { (/) } )`
12 3 11 syl6bb
` |-  ( A e. V -> ( x e. ( { (/) } |`t A ) <-> x e. { (/) } ) )`
13 12 eqrdv
` |-  ( A e. V -> ( { (/) } |`t A ) = { (/) } )`