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	⊢ ( 𝐽 ∈ ( TopOn ‘ { 𝐴 } ) → 𝐽 = 𝒫 { 𝐴 } )

Proof

Step	Hyp	Ref	Expression
1		topgele	⊢ ( 𝐽 ∈ ( TopOn ‘ { 𝐴 } ) → ( { ∅ , { 𝐴 } } ⊆ 𝐽 ∧ 𝐽 ⊆ 𝒫 { 𝐴 } ) )
2	1	simprd	⊢ ( 𝐽 ∈ ( TopOn ‘ { 𝐴 } ) → 𝐽 ⊆ 𝒫 { 𝐴 } )
3		pwsn	⊢ 𝒫 { 𝐴 } = { ∅ , { 𝐴 } }
4	1	simpld	⊢ ( 𝐽 ∈ ( TopOn ‘ { 𝐴 } ) → { ∅ , { 𝐴 } } ⊆ 𝐽 )
5	3 4	eqsstrid	⊢ ( 𝐽 ∈ ( TopOn ‘ { 𝐴 } ) → 𝒫 { 𝐴 } ⊆ 𝐽 )
6	2 5	eqssd	⊢ ( 𝐽 ∈ ( TopOn ‘ { 𝐴 } ) → 𝐽 = 𝒫 { 𝐴 } )