Theorem hmphtr

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

	Ref	Expression
Assertion	hmphtr	⊢ ( ( 𝐽 ≃ 𝐾 ∧ 𝐾 ≃ 𝐿 ) → 𝐽 ≃ 𝐿 )

Proof

Step	Hyp	Ref	Expression
1		hmph	⊢ ( 𝐽 ≃ 𝐾 ↔ ( 𝐽 Homeo 𝐾 ) ≠ ∅ )
2		hmph	⊢ ( 𝐾 ≃ 𝐿 ↔ ( 𝐾 Homeo 𝐿 ) ≠ ∅ )
3		n0	⊢ ( ( 𝐽 Homeo 𝐾 ) ≠ ∅ ↔ ∃ 𝑓 𝑓 ∈ ( 𝐽 Homeo 𝐾 ) )
4		n0	⊢ ( ( 𝐾 Homeo 𝐿 ) ≠ ∅ ↔ ∃ 𝑔 𝑔 ∈ ( 𝐾 Homeo 𝐿 ) )
5		exdistrv	⊢ ( ∃ 𝑓 ∃ 𝑔 ( 𝑓 ∈ ( 𝐽 Homeo 𝐾 ) ∧ 𝑔 ∈ ( 𝐾 Homeo 𝐿 ) ) ↔ ( ∃ 𝑓 𝑓 ∈ ( 𝐽 Homeo 𝐾 ) ∧ ∃ 𝑔 𝑔 ∈ ( 𝐾 Homeo 𝐿 ) ) )
6		hmeoco	⊢ ( ( 𝑓 ∈ ( 𝐽 Homeo 𝐾 ) ∧ 𝑔 ∈ ( 𝐾 Homeo 𝐿 ) ) → ( 𝑔 ∘ 𝑓 ) ∈ ( 𝐽 Homeo 𝐿 ) )
7		hmphi	⊢ ( ( 𝑔 ∘ 𝑓 ) ∈ ( 𝐽 Homeo 𝐿 ) → 𝐽 ≃ 𝐿 )
8	6 7	syl	⊢ ( ( 𝑓 ∈ ( 𝐽 Homeo 𝐾 ) ∧ 𝑔 ∈ ( 𝐾 Homeo 𝐿 ) ) → 𝐽 ≃ 𝐿 )
9	8	exlimivv	⊢ ( ∃ 𝑓 ∃ 𝑔 ( 𝑓 ∈ ( 𝐽 Homeo 𝐾 ) ∧ 𝑔 ∈ ( 𝐾 Homeo 𝐿 ) ) → 𝐽 ≃ 𝐿 )
10	5 9	sylbir	⊢ ( ( ∃ 𝑓 𝑓 ∈ ( 𝐽 Homeo 𝐾 ) ∧ ∃ 𝑔 𝑔 ∈ ( 𝐾 Homeo 𝐿 ) ) → 𝐽 ≃ 𝐿 )
11	3 4 10	syl2anb	⊢ ( ( ( 𝐽 Homeo 𝐾 ) ≠ ∅ ∧ ( 𝐾 Homeo 𝐿 ) ≠ ∅ ) → 𝐽 ≃ 𝐿 )
12	1 2 11	syl2anb	⊢ ( ( 𝐽 ≃ 𝐾 ∧ 𝐾 ≃ 𝐿 ) → 𝐽 ≃ 𝐿 )