Theorem en1top

Description: { (/) } is the only topology with one element. (Contributed by FL, 18-Aug-2008)

	Ref	Expression
Assertion	en1top	$$⊢J\in \mathrm{Top}\to \left(J\approx 1_{𝑜}\leftrightarrow J=\left\{\varnothing \right\}\right)$$

Proof

Step	Hyp	Ref	Expression
1		0opn	$$⊢J\in \mathrm{Top}\to \varnothing \in J$$
2		en1eqsn	$$⊢\left(\varnothing \in J\wedge J\approx 1_{𝑜}\right)\to J=\left\{\varnothing \right\}$$
3	2	ex	$$⊢\varnothing \in J\to \left(J\approx 1_{𝑜}\to J=\left\{\varnothing \right\}\right)$$
4	1 3	syl	$$⊢J\in \mathrm{Top}\to \left(J\approx 1_{𝑜}\to J=\left\{\varnothing \right\}\right)$$
5		id	$$⊢J=\left\{\varnothing \right\}\to J=\left\{\varnothing \right\}$$
6		0ex	$$⊢\varnothing \in \mathrm{V}$$
7	6	ensn1	$$⊢\left\{\varnothing \right\}\approx 1_{𝑜}$$
8	5 7	eqbrtrdi	$$⊢J=\left\{\varnothing \right\}\to J\approx 1_{𝑜}$$
9	4 8	impbid1	$$⊢J\in \mathrm{Top}\to \left(J\approx 1_{𝑜}\leftrightarrow J=\left\{\varnothing \right\}\right)$$