hmphtr

Description: "Is homeomorphic to" is transitive. (Contributed by FL, 9-Mar-2007) (Revised by Mario Carneiro, 23-Aug-2015)

		Ref	Expression
	Assertion	hmphtr	$⊢ (J ≃ K \land K ≃ L) \to J ≃ L$

Step	Hyp	Ref	Expression
1		hmph	$⊢ J ≃ K \leftrightarrow J Homeo K \neq \emptyset$
2		hmph	$⊢ K ≃ L \leftrightarrow K Homeo L \neq \emptyset$
3		n0	$⊢ J Homeo K \neq \emptyset \leftrightarrow \exists f f \in (J Homeo K)$
4		n0	$⊢ K Homeo L \neq \emptyset \leftrightarrow \exists g g \in (K Homeo L)$
5		exdistrv	$⊢ \exists f \exists g (f \in (J Homeo K) \land g \in (K Homeo L)) \leftrightarrow (\exists f f \in (J Homeo K) \land \exists g g \in (K Homeo L))$
6		hmeoco	$⊢ (f \in (J Homeo K) \land g \in (K Homeo L)) \to g \circ f \in (J Homeo L)$
7		hmphi	$⊢ g \circ f \in (J Homeo L) \to J ≃ L$
8	6 7	syl	$⊢ (f \in (J Homeo K) \land g \in (K Homeo L)) \to J ≃ L$
9	8	exlimivv	$⊢ \exists f \exists g (f \in (J Homeo K) \land g \in (K Homeo L)) \to J ≃ L$
10	5 9	sylbir	$⊢ (\exists f f \in (J Homeo K) \land \exists g g \in (K Homeo L)) \to J ≃ L$
11	3 4 10	syl2anb	$⊢ (J Homeo K \neq \emptyset \land K Homeo L \neq \emptyset) \to J ≃ L$
12	1 2 11	syl2anb	$⊢ (J ≃ K \land K ≃ L) \to J ≃ L$

Metamath Proof Explorer