Metamath Proof Explorer

Theorem hmeoco

Description: The composite of two homeomorphisms is a homeomorphism. (Contributed by FL, 9-Mar-2007) (Proof shortened by Mario Carneiro, 23-Aug-2015)

Ref Expression
Assertion hmeoco 
|- ( ( F e. ( J Homeo K ) /\ G e. ( K Homeo L ) ) -> ( G o. F ) e. ( J Homeo L ) )

Proof

Step Hyp Ref Expression
1 hmeocn 
 |-  ( F e. ( J Homeo K ) -> F e. ( J Cn K ) )
2 hmeocn 
 |-  ( G e. ( K Homeo L ) -> G e. ( K Cn L ) )
3 cnco 
 |-  ( ( F e. ( J Cn K ) /\ G e. ( K Cn L ) ) -> ( G o. F ) e. ( J Cn L ) )
4 1 2 3 syl2an 
 |-  ( ( F e. ( J Homeo K ) /\ G e. ( K Homeo L ) ) -> ( G o. F ) e. ( J Cn L ) )
5 cnvco 
 |-  `' ( G o. F ) = ( `' F o. `' G )
6 hmeocnvcn 
 |-  ( G e. ( K Homeo L ) -> `' G e. ( L Cn K ) )
7 hmeocnvcn 
 |-  ( F e. ( J Homeo K ) -> `' F e. ( K Cn J ) )
8 cnco 
 |-  ( ( `' G e. ( L Cn K ) /\ `' F e. ( K Cn J ) ) -> ( `' F o. `' G ) e. ( L Cn J ) )
9 6 7 8 syl2anr 
 |-  ( ( F e. ( J Homeo K ) /\ G e. ( K Homeo L ) ) -> ( `' F o. `' G ) e. ( L Cn J ) )
10 5 9 eqeltrid 
 |-  ( ( F e. ( J Homeo K ) /\ G e. ( K Homeo L ) ) -> `' ( G o. F ) e. ( L Cn J ) )
11 ishmeo 
 |-  ( ( G o. F ) e. ( J Homeo L ) <-> ( ( G o. F ) e. ( J Cn L ) /\ `' ( G o. F ) e. ( L Cn J ) ) )
12 4 10 11 sylanbrc 
 |-  ( ( F e. ( J Homeo K ) /\ G e. ( K Homeo L ) ) -> ( G o. F ) e. ( J Homeo L ) )