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