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 \in (J Homeo K) \land G \in (K Homeo L)) \to G \circ F \in (J Homeo L)$

Proof

Step	Hyp	Ref	Expression
1		hmeocn	$⊢ F \in (J Homeo K) \to F \in (J Cn K)$
2		hmeocn	$⊢ G \in (K Homeo L) \to G \in (K Cn L)$
3		cnco	$⊢ (F \in (J Cn K) \land G \in (K Cn L)) \to G \circ F \in (J Cn L)$
4	1 2 3	syl2an	$⊢ (F \in (J Homeo K) \land G \in (K Homeo L)) \to G \circ F \in (J Cn L)$
5		cnvco	$⊢ {(G \circ F)}^{-1} = F^{-1} \circ G^{-1}$
6		hmeocnvcn	$⊢ G \in (K Homeo L) \to G^{-1} \in (L Cn K)$
7		hmeocnvcn	$⊢ F \in (J Homeo K) \to F^{-1} \in (K Cn J)$
8		cnco	$⊢ (G^{-1} \in (L Cn K) \land F^{-1} \in (K Cn J)) \to F^{-1} \circ G^{-1} \in (L Cn J)$
9	6 7 8	syl2anr	$⊢ (F \in (J Homeo K) \land G \in (K Homeo L)) \to F^{-1} \circ G^{-1} \in (L Cn J)$
10	5 9	eqeltrid	$⊢ (F \in (J Homeo K) \land G \in (K Homeo L)) \to {(G \circ F)}^{-1} \in (L Cn J)$
11		ishmeo	$⊢ G \circ F \in (J Homeo L) \leftrightarrow (G \circ F \in (J Cn L) \land {(G \circ F)}^{-1} \in (L Cn J))$
12	4 10 11	sylanbrc	$⊢ (F \in (J Homeo K) \land G \in (K Homeo L)) \to G \circ F \in (J Homeo L)$