Metamath Proof Explorer

Theorem hmeocn

Description: A homeomorphism is continuous. (Contributed by Mario Carneiro, 22-Aug-2015)

Ref Expression
Assertion hmeocn 
|- ( F e. ( J Homeo K ) -> F e. ( J Cn K ) )

Proof

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