Theorem hmph0

Description: A topology homeomorphic to the empty set is empty. (Contributed by FL, 18-Aug-2008) (Revised by Mario Carneiro, 10-Sep-2015)

	Ref	Expression
Assertion	hmph0	⊢ ( 𝐽 ≃ { ∅ } ↔ 𝐽 = { ∅ } )

Proof

Step	Hyp	Ref	Expression
1		hmphen	⊢ ( 𝐽 ≃ { ∅ } → 𝐽 ≈ { ∅ } )
2		df1o2	⊢ 1o = { ∅ }
3	1 2	breqtrrdi	⊢ ( 𝐽 ≃ { ∅ } → 𝐽 ≈ 1o )
4		hmphtop1	⊢ ( 𝐽 ≃ { ∅ } → 𝐽 ∈ Top )
5		en1top	⊢ ( 𝐽 ∈ Top → ( 𝐽 ≈ 1o ↔ 𝐽 = { ∅ } ) )
6	4 5	syl	⊢ ( 𝐽 ≃ { ∅ } → ( 𝐽 ≈ 1o ↔ 𝐽 = { ∅ } ) )
7	3 6	mpbid	⊢ ( 𝐽 ≃ { ∅ } → 𝐽 = { ∅ } )
8		id	⊢ ( 𝐽 = { ∅ } → 𝐽 = { ∅ } )
9		sn0top	⊢ { ∅ } ∈ Top
10		hmphref	⊢ ( { ∅ } ∈ Top → { ∅ } ≃ { ∅ } )
11	9 10	ax-mp	⊢ { ∅ } ≃ { ∅ }
12	8 11	eqbrtrdi	⊢ ( 𝐽 = { ∅ } → 𝐽 ≃ { ∅ } )
13	7 12	impbii	⊢ ( 𝐽 ≃ { ∅ } ↔ 𝐽 = { ∅ } )