Theorem topsn

Description: The only topology on a singleton is the discrete topology (which is also the indiscrete topology by pwsn ). (Contributed by FL, 5-Jan-2009) (Revised by Mario Carneiro, 16-Sep-2015)

	Ref	Expression
Assertion	topsn	|- ( J e. ( TopOn ` { A } ) -> J = ~P { A } )

Proof

Step	Hyp	Ref	Expression
1		topgele	|- ( J e. ( TopOn ` { A } ) -> ( { (/) , { A } } C_ J /\ J C_ ~P { A } ) )
2	1	simprd	|- ( J e. ( TopOn ` { A } ) -> J C_ ~P { A } )
3		pwsn	|- ~P { A } = { (/) , { A } }
4	1	simpld	|- ( J e. ( TopOn ` { A } ) -> { (/) , { A } } C_ J )
5	3 4	eqsstrid	|- ( J e. ( TopOn ` { A } ) -> ~P { A } C_ J )
6	2 5	eqssd	|- ( J e. ( TopOn ` { A } ) -> J = ~P { A } )