Theorem cnco

Description: The composition of two continuous functions is a continuous function. (Contributed by FL, 8-Dec-2006) (Revised by Mario Carneiro, 21-Aug-2015)

	Ref	Expression
Assertion	cnco	⊢ ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝐺 ∈ ( 𝐾 Cn 𝐿 ) ) → ( 𝐺 ∘ 𝐹 ) ∈ ( 𝐽 Cn 𝐿 ) )

Proof

Step	Hyp	Ref	Expression
1		cntop1	⊢ ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) → 𝐽 ∈ Top )
2		cntop2	⊢ ( 𝐺 ∈ ( 𝐾 Cn 𝐿 ) → 𝐿 ∈ Top )
3	1 2	anim12i	⊢ ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝐺 ∈ ( 𝐾 Cn 𝐿 ) ) → ( 𝐽 ∈ Top ∧ 𝐿 ∈ Top ) )
4		eqid	⊢ ∪ 𝐾 = ∪ 𝐾
5		eqid	⊢ ∪ 𝐿 = ∪ 𝐿
6	4 5	cnf	⊢ ( 𝐺 ∈ ( 𝐾 Cn 𝐿 ) → 𝐺 : ∪ 𝐾 ⟶ ∪ 𝐿 )
7		eqid	⊢ ∪ 𝐽 = ∪ 𝐽
8	7 4	cnf	⊢ ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) → 𝐹 : ∪ 𝐽 ⟶ ∪ 𝐾 )
9		fco	⊢ ( ( 𝐺 : ∪ 𝐾 ⟶ ∪ 𝐿 ∧ 𝐹 : ∪ 𝐽 ⟶ ∪ 𝐾 ) → ( 𝐺 ∘ 𝐹 ) : ∪ 𝐽 ⟶ ∪ 𝐿 )
10	6 8 9	syl2anr	⊢ ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝐺 ∈ ( 𝐾 Cn 𝐿 ) ) → ( 𝐺 ∘ 𝐹 ) : ∪ 𝐽 ⟶ ∪ 𝐿 )
11		cnvco	⊢ ◡ ( 𝐺 ∘ 𝐹 ) = ( ◡ 𝐹 ∘ ◡ 𝐺 )
12	11	imaeq1i	⊢ ( ◡ ( 𝐺 ∘ 𝐹 ) “ 𝑥 ) = ( ( ◡ 𝐹 ∘ ◡ 𝐺 ) “ 𝑥 )
13		imaco	⊢ ( ( ◡ 𝐹 ∘ ◡ 𝐺 ) “ 𝑥 ) = ( ◡ 𝐹 “ ( ◡ 𝐺 “ 𝑥 ) )
14	12 13	eqtri	⊢ ( ◡ ( 𝐺 ∘ 𝐹 ) “ 𝑥 ) = ( ◡ 𝐹 “ ( ◡ 𝐺 “ 𝑥 ) )
15		simpll	⊢ ( ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝐺 ∈ ( 𝐾 Cn 𝐿 ) ) ∧ 𝑥 ∈ 𝐿 ) → 𝐹 ∈ ( 𝐽 Cn 𝐾 ) )
16		cnima	⊢ ( ( 𝐺 ∈ ( 𝐾 Cn 𝐿 ) ∧ 𝑥 ∈ 𝐿 ) → ( ◡ 𝐺 “ 𝑥 ) ∈ 𝐾 )
17	16	adantll	⊢ ( ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝐺 ∈ ( 𝐾 Cn 𝐿 ) ) ∧ 𝑥 ∈ 𝐿 ) → ( ◡ 𝐺 “ 𝑥 ) ∈ 𝐾 )
18		cnima	⊢ ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ ( ◡ 𝐺 “ 𝑥 ) ∈ 𝐾 ) → ( ◡ 𝐹 “ ( ◡ 𝐺 “ 𝑥 ) ) ∈ 𝐽 )
19	15 17 18	syl2anc	⊢ ( ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝐺 ∈ ( 𝐾 Cn 𝐿 ) ) ∧ 𝑥 ∈ 𝐿 ) → ( ◡ 𝐹 “ ( ◡ 𝐺 “ 𝑥 ) ) ∈ 𝐽 )
20	14 19	eqeltrid	⊢ ( ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝐺 ∈ ( 𝐾 Cn 𝐿 ) ) ∧ 𝑥 ∈ 𝐿 ) → ( ◡ ( 𝐺 ∘ 𝐹 ) “ 𝑥 ) ∈ 𝐽 )
21	20	ralrimiva	⊢ ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝐺 ∈ ( 𝐾 Cn 𝐿 ) ) → ∀ 𝑥 ∈ 𝐿 ( ◡ ( 𝐺 ∘ 𝐹 ) “ 𝑥 ) ∈ 𝐽 )
22	10 21	jca	⊢ ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝐺 ∈ ( 𝐾 Cn 𝐿 ) ) → ( ( 𝐺 ∘ 𝐹 ) : ∪ 𝐽 ⟶ ∪ 𝐿 ∧ ∀ 𝑥 ∈ 𝐿 ( ◡ ( 𝐺 ∘ 𝐹 ) “ 𝑥 ) ∈ 𝐽 ) )
23	7 5	iscn2	⊢ ( ( 𝐺 ∘ 𝐹 ) ∈ ( 𝐽 Cn 𝐿 ) ↔ ( ( 𝐽 ∈ Top ∧ 𝐿 ∈ Top ) ∧ ( ( 𝐺 ∘ 𝐹 ) : ∪ 𝐽 ⟶ ∪ 𝐿 ∧ ∀ 𝑥 ∈ 𝐿 ( ◡ ( 𝐺 ∘ 𝐹 ) “ 𝑥 ) ∈ 𝐽 ) ) )
24	3 22 23	sylanbrc	⊢ ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝐺 ∈ ( 𝐾 Cn 𝐿 ) ) → ( 𝐺 ∘ 𝐹 ) ∈ ( 𝐽 Cn 𝐿 ) )