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∈JCnK∧G∈KCnL→G∘F∈JCnL

Proof

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