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 ( ( 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) ∧ 𝐺 ∈ ( 𝐾 Homeo 𝐿 ) ) → ( 𝐺 ∘ 𝐹 ) ∈ ( 𝐽 Homeo 𝐿 ) )

Proof

Step Hyp Ref Expression
1 hmeocn ⊢ ( 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) → 𝐹 ∈ ( 𝐽 Cn 𝐾 ) )
2 hmeocn ⊢ ( 𝐺 ∈ ( 𝐾 Homeo 𝐿 ) → 𝐺 ∈ ( 𝐾 Cn 𝐿 ) )
3 cnco ⊢ ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝐺 ∈ ( 𝐾 Cn 𝐿 ) ) → ( 𝐺 ∘ 𝐹 ) ∈ ( 𝐽 Cn 𝐿 ) )
4 1 2 3 syl2an ⊢ ( ( 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) ∧ 𝐺 ∈ ( 𝐾 Homeo 𝐿 ) ) → ( 𝐺 ∘ 𝐹 ) ∈ ( 𝐽 Cn 𝐿 ) )
5 cnvco ⊢ ◡ ( 𝐺 ∘ 𝐹 ) = ( ◡ 𝐹 ∘ ◡ 𝐺 )
6 hmeocnvcn ⊢ ( 𝐺 ∈ ( 𝐾 Homeo 𝐿 ) → ◡ 𝐺 ∈ ( 𝐿 Cn 𝐾 ) )
7 hmeocnvcn ⊢ ( 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) → ◡ 𝐹 ∈ ( 𝐾 Cn 𝐽 ) )
8 cnco ⊢ ( ( ◡ 𝐺 ∈ ( 𝐿 Cn 𝐾 ) ∧ ◡ 𝐹 ∈ ( 𝐾 Cn 𝐽 ) ) → ( ◡ 𝐹 ∘ ◡ 𝐺 ) ∈ ( 𝐿 Cn 𝐽 ) )
9 6 7 8 syl2anr ⊢ ( ( 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) ∧ 𝐺 ∈ ( 𝐾 Homeo 𝐿 ) ) → ( ◡ 𝐹 ∘ ◡ 𝐺 ) ∈ ( 𝐿 Cn 𝐽 ) )
10 5 9 eqeltrid ⊢ ( ( 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) ∧ 𝐺 ∈ ( 𝐾 Homeo 𝐿 ) ) → ◡ ( 𝐺 ∘ 𝐹 ) ∈ ( 𝐿 Cn 𝐽 ) )
11 ishmeo ⊢ ( ( 𝐺 ∘ 𝐹 ) ∈ ( 𝐽 Homeo 𝐿 ) ↔ ( ( 𝐺 ∘ 𝐹 ) ∈ ( 𝐽 Cn 𝐿 ) ∧ ◡ ( 𝐺 ∘ 𝐹 ) ∈ ( 𝐿 Cn 𝐽 ) ) )
12 4 10 11 sylanbrc ⊢ ( ( 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) ∧ 𝐺 ∈ ( 𝐾 Homeo 𝐿 ) ) → ( 𝐺 ∘ 𝐹 ) ∈ ( 𝐽 Homeo 𝐿 ) )