Theorem restsn2

Description: The subspace topology induced by a singleton. (Contributed by FL, 5-Jan-2009) (Revised by Mario Carneiro, 16-Sep-2015)

	Ref	Expression
Assertion	restsn2	|- ( ( J e. ( TopOn ` X ) /\ A e. X ) -> ( J |`t { A } ) = ~P { A } )

Proof

Step	Hyp	Ref	Expression
1		snssi	|- ( A e. X -> { A } C_ X )
2		resttopon	|- ( ( J e. ( TopOn ` X ) /\ { A } C_ X ) -> ( J |`t { A } ) e. ( TopOn ` { A } ) )
3	1 2	sylan2	|- ( ( J e. ( TopOn ` X ) /\ A e. X ) -> ( J |`t { A } ) e. ( TopOn ` { A } ) )
4		topsn	|- ( ( J |`t { A } ) e. ( TopOn ` { A } ) -> ( J |`t { A } ) = ~P { A } )
5	3 4	syl	|- ( ( J e. ( TopOn ` X ) /\ A e. X ) -> ( J |`t { A } ) = ~P { A } )