Metamath Proof Explorer

Theorem hmphsym

Description: "Is homeomorphic to" is symmetric. (Contributed by FL, 8-Mar-2007) (Proof shortened by Mario Carneiro, 30-May-2014)

Ref Expression
Assertion hmphsym 
|- ( J ~= K -> K ~= J )

Proof

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 )