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