Metamath Proof Explorer

Theorem hmeocnvcn

Description: The converse of a homeomorphism is continuous. (Contributed by Mario Carneiro, 22-Aug-2015)

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

Proof

Step Hyp Ref Expression
1 ishmeo 
 |-  ( F e. ( J Homeo K ) <-> ( F e. ( J Cn K ) /\ `' F e. ( K Cn J ) ) )
2 1 simprbi 
 |-  ( F e. ( J Homeo K ) -> `' F e. ( K Cn J ) )