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 𝐿 ) )