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

Metamath Proof Explorer

Theorem rest0

Description: The subspace topology induced by the topology J on the empty set. (Contributed by FL, 22-Dec-2008) (Revised by Mario Carneiro, 1-May-2015)

Ref Expression
Assertion rest0 
|- ( J e. Top -> ( J |`t (/) ) = { (/) } )

Proof

Step Hyp Ref Expression
1 0ex 
 |-  (/) e. _V
2 restval 
 |-  ( ( J e. Top /\ (/) e. _V ) -> ( J |`t (/) ) = ran ( x e. J |-> ( x i^i (/) ) ) )
3 1 2 mpan2 
 |-  ( J e. Top -> ( J |`t (/) ) = ran ( x e. J |-> ( x i^i (/) ) ) )
4 in0 
 |-  ( x i^i (/) ) = (/)
5 1 elsn2 
 |-  ( ( x i^i (/) ) e. { (/) } <-> ( x i^i (/) ) = (/) )
6 4 5 mpbir 
 |-  ( x i^i (/) ) e. { (/) }
7 6 a1i 
 |-  ( ( J e. Top /\ x e. J ) -> ( x i^i (/) ) e. { (/) } )
8 7 fmpttd 
 |-  ( J e. Top -> ( x e. J |-> ( x i^i (/) ) ) : J --> { (/) } )
9 8 frnd 
 |-  ( J e. Top -> ran ( x e. J |-> ( x i^i (/) ) ) C_ { (/) } )
10 3 9 eqsstrd 
 |-  ( J e. Top -> ( J |`t (/) ) C_ { (/) } )
11 resttop 
 |-  ( ( J e. Top /\ (/) e. _V ) -> ( J |`t (/) ) e. Top )
12 1 11 mpan2 
 |-  ( J e. Top -> ( J |`t (/) ) e. Top )
13 0opn 
 |-  ( ( J |`t (/) ) e. Top -> (/) e. ( J |`t (/) ) )
14 12 13 syl 
 |-  ( J e. Top -> (/) e. ( J |`t (/) ) )
15 14 snssd 
 |-  ( J e. Top -> { (/) } C_ ( J |`t (/) ) )
16 10 15 eqssd 
 |-  ( J e. Top -> ( J |`t (/) ) = { (/) } )