Theorem en1top

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

	Ref	Expression
Assertion	en1top	⊢ ( 𝐽 ∈ Top → ( 𝐽 ≈ 1o ↔ 𝐽 = { ∅ } ) )

Proof

Step	Hyp	Ref	Expression
1		0opn	⊢ ( 𝐽 ∈ Top → ∅ ∈ 𝐽 )
2		en1eqsn	⊢ ( ( ∅ ∈ 𝐽 ∧ 𝐽 ≈ 1o ) → 𝐽 = { ∅ } )
3	2	ex	⊢ ( ∅ ∈ 𝐽 → ( 𝐽 ≈ 1o → 𝐽 = { ∅ } ) )
4	1 3	syl	⊢ ( 𝐽 ∈ Top → ( 𝐽 ≈ 1o → 𝐽 = { ∅ } ) )
5		id	⊢ ( 𝐽 = { ∅ } → 𝐽 = { ∅ } )
6		0ex	⊢ ∅ ∈ V
7	6	ensn1	⊢ { ∅ } ≈ 1o
8	5 7	eqbrtrdi	⊢ ( 𝐽 = { ∅ } → 𝐽 ≈ 1o )
9	4 8	impbid1	⊢ ( 𝐽 ∈ Top → ( 𝐽 ≈ 1o ↔ 𝐽 = { ∅ } ) )