Metamath Proof Explorer

Theorem hmeocnvb

Description: The converse of a homeomorphism is a homeomorphism. (Contributed by FL, 5-Mar-2007) (Revised by Mario Carneiro, 23-Aug-2015)

Ref Expression
Assertion hmeocnvb 
|- ( Rel F -> ( `' F e. ( J Homeo K ) <-> F e. ( K Homeo J ) ) )

Proof

Step Hyp Ref Expression
1 hmeocnv 
 |-  ( `' F e. ( J Homeo K ) -> `' `' F e. ( K Homeo J ) )
2 dfrel2 
 |-  ( Rel F <-> `' `' F = F )
3 eleq1 
 |-  ( `' `' F = F -> ( `' `' F e. ( K Homeo J ) <-> F e. ( K Homeo J ) ) )
4 2 3 sylbi 
 |-  ( Rel F -> ( `' `' F e. ( K Homeo J ) <-> F e. ( K Homeo J ) ) )
5 1 4 syl5ib 
 |-  ( Rel F -> ( `' F e. ( J Homeo K ) -> F e. ( K Homeo J ) ) )
6 hmeocnv 
 |-  ( F e. ( K Homeo J ) -> `' F e. ( J Homeo K ) )
7 5 6 impbid1 
 |-  ( Rel F -> ( `' F e. ( J Homeo K ) <-> F e. ( K Homeo J ) ) )