Metamath Proof Explorer

Theorem hmeocnv

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

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

Proof

Step Hyp Ref Expression
1 hmeocnvcn 
 |-  ( F e. ( J Homeo K ) -> `' F e. ( K Cn J ) )
2 hmeocn 
 |-  ( F e. ( J Homeo K ) -> F e. ( J Cn K ) )
3 eqid 
 |-  U. J = U. J
4 eqid 
 |-  U. K = U. K
5 3 4 cnf 
 |-  ( F e. ( J Cn K ) -> F : U. J --> U. K )
6 frel 
 |-  ( F : U. J --> U. K -> Rel F )
7 2 5 6 3syl 
 |-  ( F e. ( J Homeo K ) -> Rel F )
8 dfrel2 
 |-  ( Rel F <-> `' `' F = F )
9 7 8 sylib 
 |-  ( F e. ( J Homeo K ) -> `' `' F = F )
10 9 2 eqeltrd 
 |-  ( F e. ( J Homeo K ) -> `' `' F e. ( J Cn K ) )
11 ishmeo 
 |-  ( `' F e. ( K Homeo J ) <-> ( `' F e. ( K Cn J ) /\ `' `' F e. ( J Cn K ) ) )
12 1 10 11 sylanbrc 
 |-  ( F e. ( J Homeo K ) -> `' F e. ( K Homeo J ) )