Metamath Proof Explorer

Theorem hmpher

Description: "Is homeomorphic to" is an equivalence relation. (Contributed by FL, 22-Mar-2007) (Revised by Mario Carneiro, 23-Aug-2015)

Ref Expression
Assertion hmpher 
|- ~= Er Top

Proof

Step Hyp Ref Expression
1 df-hmph 
 |-  ~= = ( `' Homeo " ( _V \ 1o ) )
2 cnvimass 
 |-  ( `' Homeo " ( _V \ 1o ) ) C_ dom Homeo
3 hmeofn 
 |-  Homeo Fn ( Top X. Top )
4 3 fndmi 
 |-  dom Homeo = ( Top X. Top )
5 2 4 sseqtri 
 |-  ( `' Homeo " ( _V \ 1o ) ) C_ ( Top X. Top )
6 1 5 eqsstri 
 |-  ~= C_ ( Top X. Top )
7 relxp 
 |-  Rel ( Top X. Top )
8 relss 
 |-  ( ~= C_ ( Top X. Top ) -> ( Rel ( Top X. Top ) -> Rel ~= ) )
9 6 7 8 mp2 
 |-  Rel ~=
10 hmphsym 
 |-  ( x ~= y -> y ~= x )
11 hmphtr 
 |-  ( ( x ~= y /\ y ~= z ) -> x ~= z )
12 hmphref 
 |-  ( x e. Top -> x ~= x )
13 hmphtop1 
 |-  ( x ~= x -> x e. Top )
14 12 13 impbii 
 |-  ( x e. Top <-> x ~= x )
15 9 10 11 14 iseri 
 |-  ~= Er Top