Metamath Proof Explorer


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 } )