# 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 ) )`