# Metamath Proof Explorer

## Theorem cncfcompt2

Description: Composition of continuous functions. (Contributed by Glauco Siliprandi, 5-Apr-2020)

Ref Expression
Hypotheses cncfcompt2.xph ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\phi }$
cncfcompt2.ab ${⊢}{\phi }\to \left({x}\in {A}⟼{R}\right):{A}\underset{cn}{⟶}{B}$
cncfcompt2.cd ${⊢}{\phi }\to \left({y}\in {C}⟼{S}\right):{C}\underset{cn}{⟶}{E}$
cncfcompt2.bc ${⊢}{\phi }\to {B}\subseteq {C}$
cncfcompt2.st ${⊢}{y}={R}\to {S}={T}$
Assertion cncfcompt2 ${⊢}{\phi }\to \left({x}\in {A}⟼{T}\right):{A}\underset{cn}{⟶}{E}$

### Proof

Step Hyp Ref Expression
1 cncfcompt2.xph ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\phi }$
2 cncfcompt2.ab ${⊢}{\phi }\to \left({x}\in {A}⟼{R}\right):{A}\underset{cn}{⟶}{B}$
3 cncfcompt2.cd ${⊢}{\phi }\to \left({y}\in {C}⟼{S}\right):{C}\underset{cn}{⟶}{E}$
4 cncfcompt2.bc ${⊢}{\phi }\to {B}\subseteq {C}$
5 cncfcompt2.st ${⊢}{y}={R}\to {S}={T}$
6 4 adantr ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {B}\subseteq {C}$
7 cncff ${⊢}\left({x}\in {A}⟼{R}\right):{A}\underset{cn}{⟶}{B}\to \left({x}\in {A}⟼{R}\right):{A}⟶{B}$
8 2 7 syl ${⊢}{\phi }\to \left({x}\in {A}⟼{R}\right):{A}⟶{B}$
9 8 fvmptelrn ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {R}\in {B}$
10 6 9 sseldd ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {R}\in {C}$
11 10 ex ${⊢}{\phi }\to \left({x}\in {A}\to {R}\in {C}\right)$
12 1 11 ralrimi ${⊢}{\phi }\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{R}\in {C}$
13 eqidd ${⊢}{\phi }\to \left({x}\in {A}⟼{R}\right)=\left({x}\in {A}⟼{R}\right)$
14 eqidd ${⊢}{\phi }\to \left({y}\in {C}⟼{S}\right)=\left({y}\in {C}⟼{S}\right)$
15 12 13 14 5 fmptcof ${⊢}{\phi }\to \left({y}\in {C}⟼{S}\right)\circ \left({x}\in {A}⟼{R}\right)=\left({x}\in {A}⟼{T}\right)$
16 15 eqcomd ${⊢}{\phi }\to \left({x}\in {A}⟼{T}\right)=\left({y}\in {C}⟼{S}\right)\circ \left({x}\in {A}⟼{R}\right)$
17 cncfrss ${⊢}\left({y}\in {C}⟼{S}\right):{C}\underset{cn}{⟶}{E}\to {C}\subseteq ℂ$
18 3 17 syl ${⊢}{\phi }\to {C}\subseteq ℂ$
19 cncfss
20 4 18 19 syl2anc
21 20 2 sseldd ${⊢}{\phi }\to \left({x}\in {A}⟼{R}\right):{A}\underset{cn}{⟶}{C}$
22 21 3 cncfco ${⊢}{\phi }\to \left(\left({y}\in {C}⟼{S}\right)\circ \left({x}\in {A}⟼{R}\right)\right):{A}\underset{cn}{⟶}{E}$
23 16 22 eqeltrd ${⊢}{\phi }\to \left({x}\in {A}⟼{T}\right):{A}\underset{cn}{⟶}{E}$