Description: "Is homeomorphic to" is symmetric. (Contributed by FL, 8Mar2007) (Proof shortened by Mario Carneiro, 30May2014)
Ref  Expression  

Assertion  hmphsym   ( J ~= K > K ~= J ) 
Step  Hyp  Ref  Expression 

1  hmph   ( J ~= K <> ( J Homeo K ) =/= (/) ) 

2  n0   ( ( J Homeo K ) =/= (/) <> E. f f e. ( J Homeo K ) ) 

3  1 2  bitri   ( J ~= K <> E. f f e. ( J Homeo K ) ) 
4  hmeocnv   ( f e. ( J Homeo K ) > `' f e. ( K Homeo J ) ) 

5  hmphi   ( `' f e. ( K Homeo J ) > K ~= J ) 

6  4 5  syl   ( f e. ( J Homeo K ) > K ~= J ) 
7  6  exlimiv   ( E. f f e. ( J Homeo K ) > K ~= J ) 
8  3 7  sylbi   ( J ~= K > K ~= J ) 