# Metamath Proof Explorer

## Theorem cnmpt12f

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)$
cnmpt1t.b ${⊢}{\phi }\to \left({x}\in {X}⟼{B}\right)\in \left({J}\mathrm{Cn}{L}\right)$
cnmpt12f.f ${⊢}{\phi }\to {F}\in \left(\left({K}{×}_{t}{L}\right)\mathrm{Cn}{M}\right)$
Assertion cnmpt12f ${⊢}{\phi }\to \left({x}\in {X}⟼{A}{F}{B}\right)\in \left({J}\mathrm{Cn}{M}\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 cnmpt1t.b ${⊢}{\phi }\to \left({x}\in {X}⟼{B}\right)\in \left({J}\mathrm{Cn}{L}\right)$
4 cnmpt12f.f ${⊢}{\phi }\to {F}\in \left(\left({K}{×}_{t}{L}\right)\mathrm{Cn}{M}\right)$
5 df-ov ${⊢}{A}{F}{B}={F}\left(⟨{A},{B}⟩\right)$
6 5 mpteq2i ${⊢}\left({x}\in {X}⟼{A}{F}{B}\right)=\left({x}\in {X}⟼{F}\left(⟨{A},{B}⟩\right)\right)$
7 1 2 3 cnmpt1t ${⊢}{\phi }\to \left({x}\in {X}⟼⟨{A},{B}⟩\right)\in \left({J}\mathrm{Cn}\left({K}{×}_{t}{L}\right)\right)$
8 1 7 4 cnmpt11f ${⊢}{\phi }\to \left({x}\in {X}⟼{F}\left(⟨{A},{B}⟩\right)\right)\in \left({J}\mathrm{Cn}{M}\right)$
9 6 8 eqeltrid ${⊢}{\phi }\to \left({x}\in {X}⟼{A}{F}{B}\right)\in \left({J}\mathrm{Cn}{M}\right)$