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