en1top

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

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

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

Metamath Proof Explorer