This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ) = { (/) } )