# Metamath Proof Explorer

## Theorem cncfmpt1f

Description: Composition of continuous functions. -cn-> analogue of cnmpt11f . (Contributed by Mario Carneiro, 3-Sep-2014)

Ref Expression
Hypotheses cncfmpt1f.1 ${⊢}{\phi }\to {F}:ℂ\underset{cn}{⟶}ℂ$
cncfmpt1f.2 ${⊢}{\phi }\to \left({x}\in {X}⟼{A}\right):{X}\underset{cn}{⟶}ℂ$
Assertion cncfmpt1f ${⊢}{\phi }\to \left({x}\in {X}⟼{F}\left({A}\right)\right):{X}\underset{cn}{⟶}ℂ$

### Proof

Step Hyp Ref Expression
1 cncfmpt1f.1 ${⊢}{\phi }\to {F}:ℂ\underset{cn}{⟶}ℂ$
2 cncfmpt1f.2 ${⊢}{\phi }\to \left({x}\in {X}⟼{A}\right):{X}\underset{cn}{⟶}ℂ$
3 cncff ${⊢}\left({x}\in {X}⟼{A}\right):{X}\underset{cn}{⟶}ℂ\to \left({x}\in {X}⟼{A}\right):{X}⟶ℂ$
4 2 3 syl ${⊢}{\phi }\to \left({x}\in {X}⟼{A}\right):{X}⟶ℂ$
5 eqid ${⊢}\left({x}\in {X}⟼{A}\right)=\left({x}\in {X}⟼{A}\right)$
6 5 fmpt ${⊢}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}{A}\in ℂ↔\left({x}\in {X}⟼{A}\right):{X}⟶ℂ$
7 4 6 sylibr ${⊢}{\phi }\to \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}{A}\in ℂ$
8 eqidd ${⊢}{\phi }\to \left({x}\in {X}⟼{A}\right)=\left({x}\in {X}⟼{A}\right)$
9 cncff ${⊢}{F}:ℂ\underset{cn}{⟶}ℂ\to {F}:ℂ⟶ℂ$
10 1 9 syl ${⊢}{\phi }\to {F}:ℂ⟶ℂ$
11 10 feqmptd ${⊢}{\phi }\to {F}=\left({y}\in ℂ⟼{F}\left({y}\right)\right)$
12 fveq2 ${⊢}{y}={A}\to {F}\left({y}\right)={F}\left({A}\right)$
13 7 8 11 12 fmptcof ${⊢}{\phi }\to {F}\circ \left({x}\in {X}⟼{A}\right)=\left({x}\in {X}⟼{F}\left({A}\right)\right)$
14 2 1 cncfco ${⊢}{\phi }\to \left({F}\circ \left({x}\in {X}⟼{A}\right)\right):{X}\underset{cn}{⟶}ℂ$
15 13 14 eqeltrrd ${⊢}{\phi }\to \left({x}\in {X}⟼{F}\left({A}\right)\right):{X}\underset{cn}{⟶}ℂ$