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 
|- ( J ~= { (/) } <-> J = { (/) } )

Proof

Step Hyp Ref Expression
1 hmphen 
 |-  ( J ~= { (/) } -> J ~~ { (/) } )
2 df1o2 
 |-  1o = { (/) }
3 1 2 breqtrrdi 
 |-  ( J ~= { (/) } -> J ~~ 1o )
4 hmphtop1 
 |-  ( J ~= { (/) } -> J e. Top )
5 en1top 
 |-  ( J e. Top -> ( J ~~ 1o <-> J = { (/) } ) )
6 4 5 syl 
 |-  ( J ~= { (/) } -> ( J ~~ 1o <-> J = { (/) } ) )
7 3 6 mpbid 
 |-  ( J ~= { (/) } -> J = { (/) } )
8 id 
 |-  ( J = { (/) } -> J = { (/) } )
9 sn0top 
 |-  { (/) } e. Top
10 hmphref 
 |-  ( { (/) } e. Top -> { (/) } ~= { (/) } )
11 9 10 ax-mp 
 |-  { (/) } ~= { (/) }
12 8 11 eqbrtrdi 
 |-  ( J = { (/) } -> J ~= { (/) } )
13 7 12 impbii 
 |-  ( J ~= { (/) } <-> J = { (/) } )