This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( 𝐽 ≃ { ∅ } ↔ 𝐽 = { ∅ } )