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

Metamath Proof Explorer

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 ⊢ ( ( 𝐽 ≃ 𝐾 ∧ 𝐾 ≃ 𝐿 ) → 𝐽 ≃ 𝐿 )