# Metamath Proof Explorer

## Theorem cnmpt11f

Description: The composition of continuous functions is continuous. (Contributed by Mario Carneiro, 5-May-2014) (Revised by Mario Carneiro, 22-Aug-2015)

Ref Expression
Hypotheses cnmptid.j ${⊢}{\phi }\to {J}\in \mathrm{TopOn}\left({X}\right)$
cnmpt11.a ${⊢}{\phi }\to \left({x}\in {X}⟼{A}\right)\in \left({J}\mathrm{Cn}{K}\right)$
cnmpt11f.f ${⊢}{\phi }\to {F}\in \left({K}\mathrm{Cn}{L}\right)$
Assertion cnmpt11f ${⊢}{\phi }\to \left({x}\in {X}⟼{F}\left({A}\right)\right)\in \left({J}\mathrm{Cn}{L}\right)$

### Proof

Step Hyp Ref Expression
1 cnmptid.j ${⊢}{\phi }\to {J}\in \mathrm{TopOn}\left({X}\right)$
2 cnmpt11.a ${⊢}{\phi }\to \left({x}\in {X}⟼{A}\right)\in \left({J}\mathrm{Cn}{K}\right)$
3 cnmpt11f.f ${⊢}{\phi }\to {F}\in \left({K}\mathrm{Cn}{L}\right)$
4 cntop2 ${⊢}\left({x}\in {X}⟼{A}\right)\in \left({J}\mathrm{Cn}{K}\right)\to {K}\in \mathrm{Top}$
5 2 4 syl ${⊢}{\phi }\to {K}\in \mathrm{Top}$
6 toptopon2 ${⊢}{K}\in \mathrm{Top}↔{K}\in \mathrm{TopOn}\left(\bigcup {K}\right)$
7 5 6 sylib ${⊢}{\phi }\to {K}\in \mathrm{TopOn}\left(\bigcup {K}\right)$
8 eqid ${⊢}\bigcup {K}=\bigcup {K}$
9 eqid ${⊢}\bigcup {L}=\bigcup {L}$
10 8 9 cnf ${⊢}{F}\in \left({K}\mathrm{Cn}{L}\right)\to {F}:\bigcup {K}⟶\bigcup {L}$
11 3 10 syl ${⊢}{\phi }\to {F}:\bigcup {K}⟶\bigcup {L}$
12 11 feqmptd ${⊢}{\phi }\to {F}=\left({y}\in \bigcup {K}⟼{F}\left({y}\right)\right)$
13 12 3 eqeltrrd ${⊢}{\phi }\to \left({y}\in \bigcup {K}⟼{F}\left({y}\right)\right)\in \left({K}\mathrm{Cn}{L}\right)$
14 fveq2 ${⊢}{y}={A}\to {F}\left({y}\right)={F}\left({A}\right)$
15 1 2 7 13 14 cnmpt11 ${⊢}{\phi }\to \left({x}\in {X}⟼{F}\left({A}\right)\right)\in \left({J}\mathrm{Cn}{L}\right)$