# Metamath Proof Explorer

## Theorem cnmpt1t

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)$
Assertion cnmpt1t ${⊢}{\phi }\to \left({x}\in {X}⟼⟨{A},{B}⟩\right)\in \left({J}\mathrm{Cn}\left({K}{×}_{t}{L}\right)\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 toponuni ${⊢}{J}\in \mathrm{TopOn}\left({X}\right)\to {X}=\bigcup {J}$
5 mpteq1 ${⊢}{X}=\bigcup {J}\to \left({x}\in {X}⟼⟨\left({x}\in {X}⟼{A}\right)\left({x}\right),\left({x}\in {X}⟼{B}\right)\left({x}\right)⟩\right)=\left({x}\in \bigcup {J}⟼⟨\left({x}\in {X}⟼{A}\right)\left({x}\right),\left({x}\in {X}⟼{B}\right)\left({x}\right)⟩\right)$
6 1 4 5 3syl ${⊢}{\phi }\to \left({x}\in {X}⟼⟨\left({x}\in {X}⟼{A}\right)\left({x}\right),\left({x}\in {X}⟼{B}\right)\left({x}\right)⟩\right)=\left({x}\in \bigcup {J}⟼⟨\left({x}\in {X}⟼{A}\right)\left({x}\right),\left({x}\in {X}⟼{B}\right)\left({x}\right)⟩\right)$
7 simpr ${⊢}\left({\phi }\wedge {x}\in {X}\right)\to {x}\in {X}$
8 cntop2 ${⊢}\left({x}\in {X}⟼{A}\right)\in \left({J}\mathrm{Cn}{K}\right)\to {K}\in \mathrm{Top}$
9 2 8 syl ${⊢}{\phi }\to {K}\in \mathrm{Top}$
10 toptopon2 ${⊢}{K}\in \mathrm{Top}↔{K}\in \mathrm{TopOn}\left(\bigcup {K}\right)$
11 9 10 sylib ${⊢}{\phi }\to {K}\in \mathrm{TopOn}\left(\bigcup {K}\right)$
12 cnf2 ${⊢}\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {K}\in \mathrm{TopOn}\left(\bigcup {K}\right)\wedge \left({x}\in {X}⟼{A}\right)\in \left({J}\mathrm{Cn}{K}\right)\right)\to \left({x}\in {X}⟼{A}\right):{X}⟶\bigcup {K}$
13 1 11 2 12 syl3anc ${⊢}{\phi }\to \left({x}\in {X}⟼{A}\right):{X}⟶\bigcup {K}$
14 13 fvmptelrn ${⊢}\left({\phi }\wedge {x}\in {X}\right)\to {A}\in \bigcup {K}$
15 eqid ${⊢}\left({x}\in {X}⟼{A}\right)=\left({x}\in {X}⟼{A}\right)$
16 15 fvmpt2 ${⊢}\left({x}\in {X}\wedge {A}\in \bigcup {K}\right)\to \left({x}\in {X}⟼{A}\right)\left({x}\right)={A}$
17 7 14 16 syl2anc ${⊢}\left({\phi }\wedge {x}\in {X}\right)\to \left({x}\in {X}⟼{A}\right)\left({x}\right)={A}$
18 cntop2 ${⊢}\left({x}\in {X}⟼{B}\right)\in \left({J}\mathrm{Cn}{L}\right)\to {L}\in \mathrm{Top}$
19 3 18 syl ${⊢}{\phi }\to {L}\in \mathrm{Top}$
20 toptopon2 ${⊢}{L}\in \mathrm{Top}↔{L}\in \mathrm{TopOn}\left(\bigcup {L}\right)$
21 19 20 sylib ${⊢}{\phi }\to {L}\in \mathrm{TopOn}\left(\bigcup {L}\right)$
22 cnf2 ${⊢}\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {L}\in \mathrm{TopOn}\left(\bigcup {L}\right)\wedge \left({x}\in {X}⟼{B}\right)\in \left({J}\mathrm{Cn}{L}\right)\right)\to \left({x}\in {X}⟼{B}\right):{X}⟶\bigcup {L}$
23 1 21 3 22 syl3anc ${⊢}{\phi }\to \left({x}\in {X}⟼{B}\right):{X}⟶\bigcup {L}$
24 23 fvmptelrn ${⊢}\left({\phi }\wedge {x}\in {X}\right)\to {B}\in \bigcup {L}$
25 eqid ${⊢}\left({x}\in {X}⟼{B}\right)=\left({x}\in {X}⟼{B}\right)$
26 25 fvmpt2 ${⊢}\left({x}\in {X}\wedge {B}\in \bigcup {L}\right)\to \left({x}\in {X}⟼{B}\right)\left({x}\right)={B}$
27 7 24 26 syl2anc ${⊢}\left({\phi }\wedge {x}\in {X}\right)\to \left({x}\in {X}⟼{B}\right)\left({x}\right)={B}$
28 17 27 opeq12d ${⊢}\left({\phi }\wedge {x}\in {X}\right)\to ⟨\left({x}\in {X}⟼{A}\right)\left({x}\right),\left({x}\in {X}⟼{B}\right)\left({x}\right)⟩=⟨{A},{B}⟩$
29 28 mpteq2dva ${⊢}{\phi }\to \left({x}\in {X}⟼⟨\left({x}\in {X}⟼{A}\right)\left({x}\right),\left({x}\in {X}⟼{B}\right)\left({x}\right)⟩\right)=\left({x}\in {X}⟼⟨{A},{B}⟩\right)$
30 6 29 eqtr3d ${⊢}{\phi }\to \left({x}\in \bigcup {J}⟼⟨\left({x}\in {X}⟼{A}\right)\left({x}\right),\left({x}\in {X}⟼{B}\right)\left({x}\right)⟩\right)=\left({x}\in {X}⟼⟨{A},{B}⟩\right)$
31 eqid ${⊢}\bigcup {J}=\bigcup {J}$
32 nfcv ${⊢}\underset{_}{Ⅎ}{y}\phantom{\rule{.4em}{0ex}}⟨\left({x}\in {X}⟼{A}\right)\left({x}\right),\left({x}\in {X}⟼{B}\right)\left({x}\right)⟩$
33 nffvmpt1 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\left({x}\in {X}⟼{A}\right)\left({y}\right)$
34 nffvmpt1 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\left({x}\in {X}⟼{B}\right)\left({y}\right)$
35 33 34 nfop ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}⟨\left({x}\in {X}⟼{A}\right)\left({y}\right),\left({x}\in {X}⟼{B}\right)\left({y}\right)⟩$
36 fveq2 ${⊢}{x}={y}\to \left({x}\in {X}⟼{A}\right)\left({x}\right)=\left({x}\in {X}⟼{A}\right)\left({y}\right)$
37 fveq2 ${⊢}{x}={y}\to \left({x}\in {X}⟼{B}\right)\left({x}\right)=\left({x}\in {X}⟼{B}\right)\left({y}\right)$
38 36 37 opeq12d ${⊢}{x}={y}\to ⟨\left({x}\in {X}⟼{A}\right)\left({x}\right),\left({x}\in {X}⟼{B}\right)\left({x}\right)⟩=⟨\left({x}\in {X}⟼{A}\right)\left({y}\right),\left({x}\in {X}⟼{B}\right)\left({y}\right)⟩$
39 32 35 38 cbvmpt ${⊢}\left({x}\in \bigcup {J}⟼⟨\left({x}\in {X}⟼{A}\right)\left({x}\right),\left({x}\in {X}⟼{B}\right)\left({x}\right)⟩\right)=\left({y}\in \bigcup {J}⟼⟨\left({x}\in {X}⟼{A}\right)\left({y}\right),\left({x}\in {X}⟼{B}\right)\left({y}\right)⟩\right)$
40 31 39 txcnmpt ${⊢}\left(\left({x}\in {X}⟼{A}\right)\in \left({J}\mathrm{Cn}{K}\right)\wedge \left({x}\in {X}⟼{B}\right)\in \left({J}\mathrm{Cn}{L}\right)\right)\to \left({x}\in \bigcup {J}⟼⟨\left({x}\in {X}⟼{A}\right)\left({x}\right),\left({x}\in {X}⟼{B}\right)\left({x}\right)⟩\right)\in \left({J}\mathrm{Cn}\left({K}{×}_{t}{L}\right)\right)$
41 2 3 40 syl2anc ${⊢}{\phi }\to \left({x}\in \bigcup {J}⟼⟨\left({x}\in {X}⟼{A}\right)\left({x}\right),\left({x}\in {X}⟼{B}\right)\left({x}\right)⟩\right)\in \left({J}\mathrm{Cn}\left({K}{×}_{t}{L}\right)\right)$
42 30 41 eqeltrrd ${⊢}{\phi }\to \left({x}\in {X}⟼⟨{A},{B}⟩\right)\in \left({J}\mathrm{Cn}\left({K}{×}_{t}{L}\right)\right)$