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

Metamath Proof Explorer

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