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 ⊢ F ∈ J Cn K ∧ G ∈ K Cn L → G ∘ F ∈ J Cn L

Proof

Step Hyp Ref Expression
1 cntop1 ⊢ F ∈ J Cn K → J ∈ Top
2 cntop2 ⊢ G ∈ K Cn L → L ∈ Top
3 1 2 anim12i ⊢ F ∈ J Cn K ∧ G ∈ K Cn L → J ∈ Top ∧ L ∈ Top
4 eqid ⊢ ⋃ K = ⋃ K
5 eqid ⊢ ⋃ L = ⋃ L
6 4 5 cnf ⊢ G ∈ K Cn L → G : ⋃ K ⟶ ⋃ L
7 eqid ⊢ ⋃ J = ⋃ J
8 7 4 cnf ⊢ F ∈ J Cn K → F : ⋃ J ⟶ ⋃ K
9 fco ⊢ G : ⋃ K ⟶ ⋃ L ∧ F : ⋃ J ⟶ ⋃ K → G ∘ F : ⋃ J ⟶ ⋃ L
10 6 8 9 syl2anr ⊢ F ∈ J Cn K ∧ G ∈ K Cn L → G ∘ F : ⋃ J ⟶ ⋃ L
11 cnvco ⊢ G ∘ F -1 = F -1 ∘ G -1
12 11 imaeq1i ⊢ G ∘ F -1 x = F -1 ∘ G -1 x
13 imaco ⊢ F -1 ∘ G -1 x = F -1 G -1 x
14 12 13 eqtri ⊢ G ∘ F -1 x = F -1 G -1 x
15 simpll ⊢ F ∈ J Cn K ∧ G ∈ K Cn L ∧ x ∈ L → F ∈ J Cn K
16 cnima ⊢ G ∈ K Cn L ∧ x ∈ L → G -1 x ∈ K
17 16 adantll ⊢ F ∈ J Cn K ∧ G ∈ K Cn L ∧ x ∈ L → G -1 x ∈ K
18 cnima ⊢ F ∈ J Cn K ∧ G -1 x ∈ K → F -1 G -1 x ∈ J
19 15 17 18 syl2anc ⊢ F ∈ J Cn K ∧ G ∈ K Cn L ∧ x ∈ L → F -1 G -1 x ∈ J
20 14 19 eqeltrid ⊢ F ∈ J Cn K ∧ G ∈ K Cn L ∧ x ∈ L → G ∘ F -1 x ∈ J
21 20 ralrimiva ⊢ F ∈ J Cn K ∧ G ∈ K Cn L → ∀ x ∈ L G ∘ F -1 x ∈ J
22 10 21 jca ⊢ F ∈ J Cn K ∧ G ∈ K Cn L → G ∘ F : ⋃ J ⟶ ⋃ L ∧ ∀ x ∈ L G ∘ F -1 x ∈ J
23 7 5 iscn2 ⊢ G ∘ F ∈ J Cn L ↔ J ∈ Top ∧ L ∈ Top ∧ G ∘ F : ⋃ J ⟶ ⋃ L ∧ ∀ x ∈ L G ∘ F -1 x ∈ J
24 3 22 23 sylanbrc ⊢ F ∈ J Cn K ∧ G ∈ K Cn L → G ∘ F ∈ J Cn L