This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ∈ J Homeo K ∧ G ∈ K Homeo L → G ∘ F ∈ J Homeo L

Proof

Step Hyp Ref Expression
1 hmeocn ⊢ F ∈ J Homeo K → F ∈ J Cn K
2 hmeocn ⊢ G ∈ K Homeo L → G ∈ K Cn L
3 cnco ⊢ F ∈ J Cn K ∧ G ∈ K Cn L → G ∘ F ∈ J Cn L
4 1 2 3 syl2an ⊢ F ∈ J Homeo K ∧ G ∈ K Homeo L → G ∘ F ∈ J Cn L
5 cnvco ⊢ G ∘ F -1 = F -1 ∘ G -1
6 hmeocnvcn ⊢ G ∈ K Homeo L → G -1 ∈ L Cn K
7 hmeocnvcn ⊢ F ∈ J Homeo K → F -1 ∈ K Cn J
8 cnco ⊢ G -1 ∈ L Cn K ∧ F -1 ∈ K Cn J → F -1 ∘ G -1 ∈ L Cn J
9 6 7 8 syl2anr ⊢ F ∈ J Homeo K ∧ G ∈ K Homeo L → F -1 ∘ G -1 ∈ L Cn J
10 5 9 eqeltrid ⊢ F ∈ J Homeo K ∧ G ∈ K Homeo L → G ∘ F -1 ∈ L Cn J
11 ishmeo ⊢ G ∘ F ∈ J Homeo L ↔ G ∘ F ∈ J Cn L ∧ G ∘ F -1 ∈ L Cn J
12 4 10 11 sylanbrc ⊢ F ∈ J Homeo K ∧ G ∈ K Homeo L → G ∘ F ∈ J Homeo L