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 eqtrdi
 |-  ( 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 bitrdi
 |-  ( A e. V -> ( x e. ( { (/) } |`t A ) <-> x e. { (/) } ) )
13 12 eqrdv
 |-  ( A e. V -> ( { (/) } |`t A ) = { (/) } )