# Metamath Proof Explorer

## Theorem cnmpt21

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 cnmpt21.j ${⊢}{\phi }\to {J}\in \mathrm{TopOn}\left({X}\right)$
cnmpt21.k ${⊢}{\phi }\to {K}\in \mathrm{TopOn}\left({Y}\right)$
cnmpt21.a ${⊢}{\phi }\to \left({x}\in {X},{y}\in {Y}⟼{A}\right)\in \left(\left({J}{×}_{t}{K}\right)\mathrm{Cn}{L}\right)$
cnmpt21.l ${⊢}{\phi }\to {L}\in \mathrm{TopOn}\left({Z}\right)$
cnmpt21.b ${⊢}{\phi }\to \left({z}\in {Z}⟼{B}\right)\in \left({L}\mathrm{Cn}{M}\right)$
cnmpt21.c ${⊢}{z}={A}\to {B}={C}$
Assertion cnmpt21 ${⊢}{\phi }\to \left({x}\in {X},{y}\in {Y}⟼{C}\right)\in \left(\left({J}{×}_{t}{K}\right)\mathrm{Cn}{M}\right)$

### Proof

Step Hyp Ref Expression
1 cnmpt21.j ${⊢}{\phi }\to {J}\in \mathrm{TopOn}\left({X}\right)$
2 cnmpt21.k ${⊢}{\phi }\to {K}\in \mathrm{TopOn}\left({Y}\right)$
3 cnmpt21.a ${⊢}{\phi }\to \left({x}\in {X},{y}\in {Y}⟼{A}\right)\in \left(\left({J}{×}_{t}{K}\right)\mathrm{Cn}{L}\right)$
4 cnmpt21.l ${⊢}{\phi }\to {L}\in \mathrm{TopOn}\left({Z}\right)$
5 cnmpt21.b ${⊢}{\phi }\to \left({z}\in {Z}⟼{B}\right)\in \left({L}\mathrm{Cn}{M}\right)$
6 cnmpt21.c ${⊢}{z}={A}\to {B}={C}$
7 df-ov ${⊢}{x}\left({x}\in {X},{y}\in {Y}⟼{A}\right){y}=\left({x}\in {X},{y}\in {Y}⟼{A}\right)\left(⟨{x},{y}⟩\right)$
8 simprl ${⊢}\left({\phi }\wedge \left({x}\in {X}\wedge {y}\in {Y}\right)\right)\to {x}\in {X}$
9 simprr ${⊢}\left({\phi }\wedge \left({x}\in {X}\wedge {y}\in {Y}\right)\right)\to {y}\in {Y}$
10 txtopon ${⊢}\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {K}\in \mathrm{TopOn}\left({Y}\right)\right)\to {J}{×}_{t}{K}\in \mathrm{TopOn}\left({X}×{Y}\right)$
11 1 2 10 syl2anc ${⊢}{\phi }\to {J}{×}_{t}{K}\in \mathrm{TopOn}\left({X}×{Y}\right)$
12 cnf2 ${⊢}\left({J}{×}_{t}{K}\in \mathrm{TopOn}\left({X}×{Y}\right)\wedge {L}\in \mathrm{TopOn}\left({Z}\right)\wedge \left({x}\in {X},{y}\in {Y}⟼{A}\right)\in \left(\left({J}{×}_{t}{K}\right)\mathrm{Cn}{L}\right)\right)\to \left({x}\in {X},{y}\in {Y}⟼{A}\right):{X}×{Y}⟶{Z}$
13 11 4 3 12 syl3anc ${⊢}{\phi }\to \left({x}\in {X},{y}\in {Y}⟼{A}\right):{X}×{Y}⟶{Z}$
14 eqid ${⊢}\left({x}\in {X},{y}\in {Y}⟼{A}\right)=\left({x}\in {X},{y}\in {Y}⟼{A}\right)$
15 14 fmpo ${⊢}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {Y}\phantom{\rule{.4em}{0ex}}{A}\in {Z}↔\left({x}\in {X},{y}\in {Y}⟼{A}\right):{X}×{Y}⟶{Z}$
16 13 15 sylibr ${⊢}{\phi }\to \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {Y}\phantom{\rule{.4em}{0ex}}{A}\in {Z}$
17 rsp2 ${⊢}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {Y}\phantom{\rule{.4em}{0ex}}{A}\in {Z}\to \left(\left({x}\in {X}\wedge {y}\in {Y}\right)\to {A}\in {Z}\right)$
18 16 17 syl ${⊢}{\phi }\to \left(\left({x}\in {X}\wedge {y}\in {Y}\right)\to {A}\in {Z}\right)$
19 18 imp ${⊢}\left({\phi }\wedge \left({x}\in {X}\wedge {y}\in {Y}\right)\right)\to {A}\in {Z}$
20 14 ovmpt4g ${⊢}\left({x}\in {X}\wedge {y}\in {Y}\wedge {A}\in {Z}\right)\to {x}\left({x}\in {X},{y}\in {Y}⟼{A}\right){y}={A}$
21 8 9 19 20 syl3anc ${⊢}\left({\phi }\wedge \left({x}\in {X}\wedge {y}\in {Y}\right)\right)\to {x}\left({x}\in {X},{y}\in {Y}⟼{A}\right){y}={A}$
22 7 21 syl5eqr ${⊢}\left({\phi }\wedge \left({x}\in {X}\wedge {y}\in {Y}\right)\right)\to \left({x}\in {X},{y}\in {Y}⟼{A}\right)\left(⟨{x},{y}⟩\right)={A}$
23 22 fveq2d ${⊢}\left({\phi }\wedge \left({x}\in {X}\wedge {y}\in {Y}\right)\right)\to \left({z}\in {Z}⟼{B}\right)\left(\left({x}\in {X},{y}\in {Y}⟼{A}\right)\left(⟨{x},{y}⟩\right)\right)=\left({z}\in {Z}⟼{B}\right)\left({A}\right)$
24 eqid ${⊢}\left({z}\in {Z}⟼{B}\right)=\left({z}\in {Z}⟼{B}\right)$
25 6 eleq1d ${⊢}{z}={A}\to \left({B}\in \bigcup {M}↔{C}\in \bigcup {M}\right)$
26 cntop2 ${⊢}\left({z}\in {Z}⟼{B}\right)\in \left({L}\mathrm{Cn}{M}\right)\to {M}\in \mathrm{Top}$
27 5 26 syl ${⊢}{\phi }\to {M}\in \mathrm{Top}$
28 toptopon2 ${⊢}{M}\in \mathrm{Top}↔{M}\in \mathrm{TopOn}\left(\bigcup {M}\right)$
29 27 28 sylib ${⊢}{\phi }\to {M}\in \mathrm{TopOn}\left(\bigcup {M}\right)$
30 cnf2 ${⊢}\left({L}\in \mathrm{TopOn}\left({Z}\right)\wedge {M}\in \mathrm{TopOn}\left(\bigcup {M}\right)\wedge \left({z}\in {Z}⟼{B}\right)\in \left({L}\mathrm{Cn}{M}\right)\right)\to \left({z}\in {Z}⟼{B}\right):{Z}⟶\bigcup {M}$
31 4 29 5 30 syl3anc ${⊢}{\phi }\to \left({z}\in {Z}⟼{B}\right):{Z}⟶\bigcup {M}$
32 24 fmpt ${⊢}\forall {z}\in {Z}\phantom{\rule{.4em}{0ex}}{B}\in \bigcup {M}↔\left({z}\in {Z}⟼{B}\right):{Z}⟶\bigcup {M}$
33 31 32 sylibr ${⊢}{\phi }\to \forall {z}\in {Z}\phantom{\rule{.4em}{0ex}}{B}\in \bigcup {M}$
34 33 adantr ${⊢}\left({\phi }\wedge \left({x}\in {X}\wedge {y}\in {Y}\right)\right)\to \forall {z}\in {Z}\phantom{\rule{.4em}{0ex}}{B}\in \bigcup {M}$
35 25 34 19 rspcdva ${⊢}\left({\phi }\wedge \left({x}\in {X}\wedge {y}\in {Y}\right)\right)\to {C}\in \bigcup {M}$
36 24 6 19 35 fvmptd3 ${⊢}\left({\phi }\wedge \left({x}\in {X}\wedge {y}\in {Y}\right)\right)\to \left({z}\in {Z}⟼{B}\right)\left({A}\right)={C}$
37 23 36 eqtrd ${⊢}\left({\phi }\wedge \left({x}\in {X}\wedge {y}\in {Y}\right)\right)\to \left({z}\in {Z}⟼{B}\right)\left(\left({x}\in {X},{y}\in {Y}⟼{A}\right)\left(⟨{x},{y}⟩\right)\right)={C}$
38 opelxpi ${⊢}\left({x}\in {X}\wedge {y}\in {Y}\right)\to ⟨{x},{y}⟩\in \left({X}×{Y}\right)$
39 fvco3 ${⊢}\left(\left({x}\in {X},{y}\in {Y}⟼{A}\right):{X}×{Y}⟶{Z}\wedge ⟨{x},{y}⟩\in \left({X}×{Y}\right)\right)\to \left(\left({z}\in {Z}⟼{B}\right)\circ \left({x}\in {X},{y}\in {Y}⟼{A}\right)\right)\left(⟨{x},{y}⟩\right)=\left({z}\in {Z}⟼{B}\right)\left(\left({x}\in {X},{y}\in {Y}⟼{A}\right)\left(⟨{x},{y}⟩\right)\right)$
40 13 38 39 syl2an ${⊢}\left({\phi }\wedge \left({x}\in {X}\wedge {y}\in {Y}\right)\right)\to \left(\left({z}\in {Z}⟼{B}\right)\circ \left({x}\in {X},{y}\in {Y}⟼{A}\right)\right)\left(⟨{x},{y}⟩\right)=\left({z}\in {Z}⟼{B}\right)\left(\left({x}\in {X},{y}\in {Y}⟼{A}\right)\left(⟨{x},{y}⟩\right)\right)$
41 df-ov ${⊢}{x}\left({x}\in {X},{y}\in {Y}⟼{C}\right){y}=\left({x}\in {X},{y}\in {Y}⟼{C}\right)\left(⟨{x},{y}⟩\right)$
42 eqid ${⊢}\left({x}\in {X},{y}\in {Y}⟼{C}\right)=\left({x}\in {X},{y}\in {Y}⟼{C}\right)$
43 42 ovmpt4g ${⊢}\left({x}\in {X}\wedge {y}\in {Y}\wedge {C}\in \bigcup {M}\right)\to {x}\left({x}\in {X},{y}\in {Y}⟼{C}\right){y}={C}$
44 8 9 35 43 syl3anc ${⊢}\left({\phi }\wedge \left({x}\in {X}\wedge {y}\in {Y}\right)\right)\to {x}\left({x}\in {X},{y}\in {Y}⟼{C}\right){y}={C}$
45 41 44 syl5eqr ${⊢}\left({\phi }\wedge \left({x}\in {X}\wedge {y}\in {Y}\right)\right)\to \left({x}\in {X},{y}\in {Y}⟼{C}\right)\left(⟨{x},{y}⟩\right)={C}$
46 37 40 45 3eqtr4d ${⊢}\left({\phi }\wedge \left({x}\in {X}\wedge {y}\in {Y}\right)\right)\to \left(\left({z}\in {Z}⟼{B}\right)\circ \left({x}\in {X},{y}\in {Y}⟼{A}\right)\right)\left(⟨{x},{y}⟩\right)=\left({x}\in {X},{y}\in {Y}⟼{C}\right)\left(⟨{x},{y}⟩\right)$
47 46 ralrimivva ${⊢}{\phi }\to \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {Y}\phantom{\rule{.4em}{0ex}}\left(\left({z}\in {Z}⟼{B}\right)\circ \left({x}\in {X},{y}\in {Y}⟼{A}\right)\right)\left(⟨{x},{y}⟩\right)=\left({x}\in {X},{y}\in {Y}⟼{C}\right)\left(⟨{x},{y}⟩\right)$
48 nfv ${⊢}Ⅎ{u}\phantom{\rule{.4em}{0ex}}\forall {y}\in {Y}\phantom{\rule{.4em}{0ex}}\left(\left({z}\in {Z}⟼{B}\right)\circ \left({x}\in {X},{y}\in {Y}⟼{A}\right)\right)\left(⟨{x},{y}⟩\right)=\left({x}\in {X},{y}\in {Y}⟼{C}\right)\left(⟨{x},{y}⟩\right)$
49 nfcv ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{Y}$
50 nfcv ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\left({z}\in {Z}⟼{B}\right)$
51 nfmpo1 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\left({x}\in {X},{y}\in {Y}⟼{A}\right)$
52 50 51 nfco ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\left(\left({z}\in {Z}⟼{B}\right)\circ \left({x}\in {X},{y}\in {Y}⟼{A}\right)\right)$
53 nfcv ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}⟨{u},{v}⟩$
54 52 53 nffv ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\left(\left({z}\in {Z}⟼{B}\right)\circ \left({x}\in {X},{y}\in {Y}⟼{A}\right)\right)\left(⟨{u},{v}⟩\right)$
55 nfmpo1 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\left({x}\in {X},{y}\in {Y}⟼{C}\right)$
56 55 53 nffv ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\left({x}\in {X},{y}\in {Y}⟼{C}\right)\left(⟨{u},{v}⟩\right)$
57 54 56 nfeq ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\left(\left({z}\in {Z}⟼{B}\right)\circ \left({x}\in {X},{y}\in {Y}⟼{A}\right)\right)\left(⟨{u},{v}⟩\right)=\left({x}\in {X},{y}\in {Y}⟼{C}\right)\left(⟨{u},{v}⟩\right)$
58 49 57 nfralw ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\forall {v}\in {Y}\phantom{\rule{.4em}{0ex}}\left(\left({z}\in {Z}⟼{B}\right)\circ \left({x}\in {X},{y}\in {Y}⟼{A}\right)\right)\left(⟨{u},{v}⟩\right)=\left({x}\in {X},{y}\in {Y}⟼{C}\right)\left(⟨{u},{v}⟩\right)$
59 nfv ${⊢}Ⅎ{v}\phantom{\rule{.4em}{0ex}}\left(\left({z}\in {Z}⟼{B}\right)\circ \left({x}\in {X},{y}\in {Y}⟼{A}\right)\right)\left(⟨{x},{y}⟩\right)=\left({x}\in {X},{y}\in {Y}⟼{C}\right)\left(⟨{x},{y}⟩\right)$
60 nfcv ${⊢}\underset{_}{Ⅎ}{y}\phantom{\rule{.4em}{0ex}}\left({z}\in {Z}⟼{B}\right)$
61 nfmpo2 ${⊢}\underset{_}{Ⅎ}{y}\phantom{\rule{.4em}{0ex}}\left({x}\in {X},{y}\in {Y}⟼{A}\right)$
62 60 61 nfco ${⊢}\underset{_}{Ⅎ}{y}\phantom{\rule{.4em}{0ex}}\left(\left({z}\in {Z}⟼{B}\right)\circ \left({x}\in {X},{y}\in {Y}⟼{A}\right)\right)$
63 nfcv ${⊢}\underset{_}{Ⅎ}{y}\phantom{\rule{.4em}{0ex}}⟨{x},{v}⟩$
64 62 63 nffv ${⊢}\underset{_}{Ⅎ}{y}\phantom{\rule{.4em}{0ex}}\left(\left({z}\in {Z}⟼{B}\right)\circ \left({x}\in {X},{y}\in {Y}⟼{A}\right)\right)\left(⟨{x},{v}⟩\right)$
65 nfmpo2 ${⊢}\underset{_}{Ⅎ}{y}\phantom{\rule{.4em}{0ex}}\left({x}\in {X},{y}\in {Y}⟼{C}\right)$
66 65 63 nffv ${⊢}\underset{_}{Ⅎ}{y}\phantom{\rule{.4em}{0ex}}\left({x}\in {X},{y}\in {Y}⟼{C}\right)\left(⟨{x},{v}⟩\right)$
67 64 66 nfeq ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}\left(\left({z}\in {Z}⟼{B}\right)\circ \left({x}\in {X},{y}\in {Y}⟼{A}\right)\right)\left(⟨{x},{v}⟩\right)=\left({x}\in {X},{y}\in {Y}⟼{C}\right)\left(⟨{x},{v}⟩\right)$
68 opeq2 ${⊢}{y}={v}\to ⟨{x},{y}⟩=⟨{x},{v}⟩$
69 68 fveq2d ${⊢}{y}={v}\to \left(\left({z}\in {Z}⟼{B}\right)\circ \left({x}\in {X},{y}\in {Y}⟼{A}\right)\right)\left(⟨{x},{y}⟩\right)=\left(\left({z}\in {Z}⟼{B}\right)\circ \left({x}\in {X},{y}\in {Y}⟼{A}\right)\right)\left(⟨{x},{v}⟩\right)$
70 68 fveq2d ${⊢}{y}={v}\to \left({x}\in {X},{y}\in {Y}⟼{C}\right)\left(⟨{x},{y}⟩\right)=\left({x}\in {X},{y}\in {Y}⟼{C}\right)\left(⟨{x},{v}⟩\right)$
71 69 70 eqeq12d ${⊢}{y}={v}\to \left(\left(\left({z}\in {Z}⟼{B}\right)\circ \left({x}\in {X},{y}\in {Y}⟼{A}\right)\right)\left(⟨{x},{y}⟩\right)=\left({x}\in {X},{y}\in {Y}⟼{C}\right)\left(⟨{x},{y}⟩\right)↔\left(\left({z}\in {Z}⟼{B}\right)\circ \left({x}\in {X},{y}\in {Y}⟼{A}\right)\right)\left(⟨{x},{v}⟩\right)=\left({x}\in {X},{y}\in {Y}⟼{C}\right)\left(⟨{x},{v}⟩\right)\right)$
72 59 67 71 cbvralw ${⊢}\forall {y}\in {Y}\phantom{\rule{.4em}{0ex}}\left(\left({z}\in {Z}⟼{B}\right)\circ \left({x}\in {X},{y}\in {Y}⟼{A}\right)\right)\left(⟨{x},{y}⟩\right)=\left({x}\in {X},{y}\in {Y}⟼{C}\right)\left(⟨{x},{y}⟩\right)↔\forall {v}\in {Y}\phantom{\rule{.4em}{0ex}}\left(\left({z}\in {Z}⟼{B}\right)\circ \left({x}\in {X},{y}\in {Y}⟼{A}\right)\right)\left(⟨{x},{v}⟩\right)=\left({x}\in {X},{y}\in {Y}⟼{C}\right)\left(⟨{x},{v}⟩\right)$
73 opeq1 ${⊢}{x}={u}\to ⟨{x},{v}⟩=⟨{u},{v}⟩$
74 73 fveq2d ${⊢}{x}={u}\to \left(\left({z}\in {Z}⟼{B}\right)\circ \left({x}\in {X},{y}\in {Y}⟼{A}\right)\right)\left(⟨{x},{v}⟩\right)=\left(\left({z}\in {Z}⟼{B}\right)\circ \left({x}\in {X},{y}\in {Y}⟼{A}\right)\right)\left(⟨{u},{v}⟩\right)$
75 73 fveq2d ${⊢}{x}={u}\to \left({x}\in {X},{y}\in {Y}⟼{C}\right)\left(⟨{x},{v}⟩\right)=\left({x}\in {X},{y}\in {Y}⟼{C}\right)\left(⟨{u},{v}⟩\right)$
76 74 75 eqeq12d ${⊢}{x}={u}\to \left(\left(\left({z}\in {Z}⟼{B}\right)\circ \left({x}\in {X},{y}\in {Y}⟼{A}\right)\right)\left(⟨{x},{v}⟩\right)=\left({x}\in {X},{y}\in {Y}⟼{C}\right)\left(⟨{x},{v}⟩\right)↔\left(\left({z}\in {Z}⟼{B}\right)\circ \left({x}\in {X},{y}\in {Y}⟼{A}\right)\right)\left(⟨{u},{v}⟩\right)=\left({x}\in {X},{y}\in {Y}⟼{C}\right)\left(⟨{u},{v}⟩\right)\right)$
77 76 ralbidv ${⊢}{x}={u}\to \left(\forall {v}\in {Y}\phantom{\rule{.4em}{0ex}}\left(\left({z}\in {Z}⟼{B}\right)\circ \left({x}\in {X},{y}\in {Y}⟼{A}\right)\right)\left(⟨{x},{v}⟩\right)=\left({x}\in {X},{y}\in {Y}⟼{C}\right)\left(⟨{x},{v}⟩\right)↔\forall {v}\in {Y}\phantom{\rule{.4em}{0ex}}\left(\left({z}\in {Z}⟼{B}\right)\circ \left({x}\in {X},{y}\in {Y}⟼{A}\right)\right)\left(⟨{u},{v}⟩\right)=\left({x}\in {X},{y}\in {Y}⟼{C}\right)\left(⟨{u},{v}⟩\right)\right)$
78 72 77 syl5bb ${⊢}{x}={u}\to \left(\forall {y}\in {Y}\phantom{\rule{.4em}{0ex}}\left(\left({z}\in {Z}⟼{B}\right)\circ \left({x}\in {X},{y}\in {Y}⟼{A}\right)\right)\left(⟨{x},{y}⟩\right)=\left({x}\in {X},{y}\in {Y}⟼{C}\right)\left(⟨{x},{y}⟩\right)↔\forall {v}\in {Y}\phantom{\rule{.4em}{0ex}}\left(\left({z}\in {Z}⟼{B}\right)\circ \left({x}\in {X},{y}\in {Y}⟼{A}\right)\right)\left(⟨{u},{v}⟩\right)=\left({x}\in {X},{y}\in {Y}⟼{C}\right)\left(⟨{u},{v}⟩\right)\right)$
79 48 58 78 cbvralw ${⊢}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {Y}\phantom{\rule{.4em}{0ex}}\left(\left({z}\in {Z}⟼{B}\right)\circ \left({x}\in {X},{y}\in {Y}⟼{A}\right)\right)\left(⟨{x},{y}⟩\right)=\left({x}\in {X},{y}\in {Y}⟼{C}\right)\left(⟨{x},{y}⟩\right)↔\forall {u}\in {X}\phantom{\rule{.4em}{0ex}}\forall {v}\in {Y}\phantom{\rule{.4em}{0ex}}\left(\left({z}\in {Z}⟼{B}\right)\circ \left({x}\in {X},{y}\in {Y}⟼{A}\right)\right)\left(⟨{u},{v}⟩\right)=\left({x}\in {X},{y}\in {Y}⟼{C}\right)\left(⟨{u},{v}⟩\right)$
80 47 79 sylib ${⊢}{\phi }\to \forall {u}\in {X}\phantom{\rule{.4em}{0ex}}\forall {v}\in {Y}\phantom{\rule{.4em}{0ex}}\left(\left({z}\in {Z}⟼{B}\right)\circ \left({x}\in {X},{y}\in {Y}⟼{A}\right)\right)\left(⟨{u},{v}⟩\right)=\left({x}\in {X},{y}\in {Y}⟼{C}\right)\left(⟨{u},{v}⟩\right)$
81 fveq2 ${⊢}{w}=⟨{u},{v}⟩\to \left(\left({z}\in {Z}⟼{B}\right)\circ \left({x}\in {X},{y}\in {Y}⟼{A}\right)\right)\left({w}\right)=\left(\left({z}\in {Z}⟼{B}\right)\circ \left({x}\in {X},{y}\in {Y}⟼{A}\right)\right)\left(⟨{u},{v}⟩\right)$
82 fveq2 ${⊢}{w}=⟨{u},{v}⟩\to \left({x}\in {X},{y}\in {Y}⟼{C}\right)\left({w}\right)=\left({x}\in {X},{y}\in {Y}⟼{C}\right)\left(⟨{u},{v}⟩\right)$
83 81 82 eqeq12d ${⊢}{w}=⟨{u},{v}⟩\to \left(\left(\left({z}\in {Z}⟼{B}\right)\circ \left({x}\in {X},{y}\in {Y}⟼{A}\right)\right)\left({w}\right)=\left({x}\in {X},{y}\in {Y}⟼{C}\right)\left({w}\right)↔\left(\left({z}\in {Z}⟼{B}\right)\circ \left({x}\in {X},{y}\in {Y}⟼{A}\right)\right)\left(⟨{u},{v}⟩\right)=\left({x}\in {X},{y}\in {Y}⟼{C}\right)\left(⟨{u},{v}⟩\right)\right)$
84 83 ralxp ${⊢}\forall {w}\in \left({X}×{Y}\right)\phantom{\rule{.4em}{0ex}}\left(\left({z}\in {Z}⟼{B}\right)\circ \left({x}\in {X},{y}\in {Y}⟼{A}\right)\right)\left({w}\right)=\left({x}\in {X},{y}\in {Y}⟼{C}\right)\left({w}\right)↔\forall {u}\in {X}\phantom{\rule{.4em}{0ex}}\forall {v}\in {Y}\phantom{\rule{.4em}{0ex}}\left(\left({z}\in {Z}⟼{B}\right)\circ \left({x}\in {X},{y}\in {Y}⟼{A}\right)\right)\left(⟨{u},{v}⟩\right)=\left({x}\in {X},{y}\in {Y}⟼{C}\right)\left(⟨{u},{v}⟩\right)$
85 80 84 sylibr ${⊢}{\phi }\to \forall {w}\in \left({X}×{Y}\right)\phantom{\rule{.4em}{0ex}}\left(\left({z}\in {Z}⟼{B}\right)\circ \left({x}\in {X},{y}\in {Y}⟼{A}\right)\right)\left({w}\right)=\left({x}\in {X},{y}\in {Y}⟼{C}\right)\left({w}\right)$
86 fco ${⊢}\left(\left({z}\in {Z}⟼{B}\right):{Z}⟶\bigcup {M}\wedge \left({x}\in {X},{y}\in {Y}⟼{A}\right):{X}×{Y}⟶{Z}\right)\to \left(\left({z}\in {Z}⟼{B}\right)\circ \left({x}\in {X},{y}\in {Y}⟼{A}\right)\right):{X}×{Y}⟶\bigcup {M}$
87 31 13 86 syl2anc ${⊢}{\phi }\to \left(\left({z}\in {Z}⟼{B}\right)\circ \left({x}\in {X},{y}\in {Y}⟼{A}\right)\right):{X}×{Y}⟶\bigcup {M}$
88 87 ffnd ${⊢}{\phi }\to \left(\left({z}\in {Z}⟼{B}\right)\circ \left({x}\in {X},{y}\in {Y}⟼{A}\right)\right)Fn\left({X}×{Y}\right)$
89 35 ralrimivva ${⊢}{\phi }\to \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {Y}\phantom{\rule{.4em}{0ex}}{C}\in \bigcup {M}$
90 42 fmpo ${⊢}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {Y}\phantom{\rule{.4em}{0ex}}{C}\in \bigcup {M}↔\left({x}\in {X},{y}\in {Y}⟼{C}\right):{X}×{Y}⟶\bigcup {M}$
91 89 90 sylib ${⊢}{\phi }\to \left({x}\in {X},{y}\in {Y}⟼{C}\right):{X}×{Y}⟶\bigcup {M}$
92 91 ffnd ${⊢}{\phi }\to \left({x}\in {X},{y}\in {Y}⟼{C}\right)Fn\left({X}×{Y}\right)$
93 eqfnfv ${⊢}\left(\left(\left({z}\in {Z}⟼{B}\right)\circ \left({x}\in {X},{y}\in {Y}⟼{A}\right)\right)Fn\left({X}×{Y}\right)\wedge \left({x}\in {X},{y}\in {Y}⟼{C}\right)Fn\left({X}×{Y}\right)\right)\to \left(\left({z}\in {Z}⟼{B}\right)\circ \left({x}\in {X},{y}\in {Y}⟼{A}\right)=\left({x}\in {X},{y}\in {Y}⟼{C}\right)↔\forall {w}\in \left({X}×{Y}\right)\phantom{\rule{.4em}{0ex}}\left(\left({z}\in {Z}⟼{B}\right)\circ \left({x}\in {X},{y}\in {Y}⟼{A}\right)\right)\left({w}\right)=\left({x}\in {X},{y}\in {Y}⟼{C}\right)\left({w}\right)\right)$
94 88 92 93 syl2anc ${⊢}{\phi }\to \left(\left({z}\in {Z}⟼{B}\right)\circ \left({x}\in {X},{y}\in {Y}⟼{A}\right)=\left({x}\in {X},{y}\in {Y}⟼{C}\right)↔\forall {w}\in \left({X}×{Y}\right)\phantom{\rule{.4em}{0ex}}\left(\left({z}\in {Z}⟼{B}\right)\circ \left({x}\in {X},{y}\in {Y}⟼{A}\right)\right)\left({w}\right)=\left({x}\in {X},{y}\in {Y}⟼{C}\right)\left({w}\right)\right)$
95 85 94 mpbird ${⊢}{\phi }\to \left({z}\in {Z}⟼{B}\right)\circ \left({x}\in {X},{y}\in {Y}⟼{A}\right)=\left({x}\in {X},{y}\in {Y}⟼{C}\right)$
96 cnco ${⊢}\left(\left({x}\in {X},{y}\in {Y}⟼{A}\right)\in \left(\left({J}{×}_{t}{K}\right)\mathrm{Cn}{L}\right)\wedge \left({z}\in {Z}⟼{B}\right)\in \left({L}\mathrm{Cn}{M}\right)\right)\to \left({z}\in {Z}⟼{B}\right)\circ \left({x}\in {X},{y}\in {Y}⟼{A}\right)\in \left(\left({J}{×}_{t}{K}\right)\mathrm{Cn}{M}\right)$
97 3 5 96 syl2anc ${⊢}{\phi }\to \left({z}\in {Z}⟼{B}\right)\circ \left({x}\in {X},{y}\in {Y}⟼{A}\right)\in \left(\left({J}{×}_{t}{K}\right)\mathrm{Cn}{M}\right)$
98 95 97 eqeltrrd ${⊢}{\phi }\to \left({x}\in {X},{y}\in {Y}⟼{C}\right)\in \left(\left({J}{×}_{t}{K}\right)\mathrm{Cn}{M}\right)$