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\in \mathrm{TopOn}\left(\left\{A\right\}\right)\to J=𝒫\left\{A\right\}$$

Proof

Step	Hyp	Ref	Expression
1		topgele	$$⊢J\in \mathrm{TopOn}\left(\left\{A\right\}\right)\to \left(\left\{\varnothing ,\left\{A\right\}\right\}\subseteq J\wedge J\subseteq 𝒫\left\{A\right\}\right)$$
2	1	simprd	$$⊢J\in \mathrm{TopOn}\left(\left\{A\right\}\right)\to J\subseteq 𝒫\left\{A\right\}$$
3		pwsn	$$⊢𝒫\left\{A\right\}=\left\{\varnothing ,\left\{A\right\}\right\}$$
4	1	simpld	$$⊢J\in \mathrm{TopOn}\left(\left\{A\right\}\right)\to \left\{\varnothing ,\left\{A\right\}\right\}\subseteq J$$
5	3 4	eqsstrid	$$⊢J\in \mathrm{TopOn}\left(\left\{A\right\}\right)\to 𝒫\left\{A\right\}\subseteq J$$
6	2 5	eqssd	$$⊢J\in \mathrm{TopOn}\left(\left\{A\right\}\right)\to J=𝒫\left\{A\right\}$$