# Metamath Proof Explorer

## Theorem uncfcurf

Description: Cancellation of uncurry with curry. (Contributed by Mario Carneiro, 13-Jan-2017)

Ref Expression
Hypotheses uncfcurf.g ${⊢}{G}=⟨{C},{D}⟩{curry}_{F}{F}$
uncfcurf.c ${⊢}{\phi }\to {C}\in \mathrm{Cat}$
uncfcurf.d ${⊢}{\phi }\to {D}\in \mathrm{Cat}$
uncfcurf.f ${⊢}{\phi }\to {F}\in \left(\left({C}{×}_{c}{D}\right)\mathrm{Func}{E}\right)$
Assertion uncfcurf ${⊢}{\phi }\to ⟨“{C}{D}{E}”⟩{uncurry}_{F}{G}={F}$

### Proof

Step Hyp Ref Expression
1 uncfcurf.g ${⊢}{G}=⟨{C},{D}⟩{curry}_{F}{F}$
2 uncfcurf.c ${⊢}{\phi }\to {C}\in \mathrm{Cat}$
3 uncfcurf.d ${⊢}{\phi }\to {D}\in \mathrm{Cat}$
4 uncfcurf.f ${⊢}{\phi }\to {F}\in \left(\left({C}{×}_{c}{D}\right)\mathrm{Func}{E}\right)$
5 eqid ${⊢}⟨“{C}{D}{E}”⟩{uncurry}_{F}{G}=⟨“{C}{D}{E}”⟩{uncurry}_{F}{G}$
6 3 adantr ${⊢}\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{D}}\right)\right)\to {D}\in \mathrm{Cat}$
7 funcrcl ${⊢}{F}\in \left(\left({C}{×}_{c}{D}\right)\mathrm{Func}{E}\right)\to \left({C}{×}_{c}{D}\in \mathrm{Cat}\wedge {E}\in \mathrm{Cat}\right)$
8 4 7 syl ${⊢}{\phi }\to \left({C}{×}_{c}{D}\in \mathrm{Cat}\wedge {E}\in \mathrm{Cat}\right)$
9 8 simprd ${⊢}{\phi }\to {E}\in \mathrm{Cat}$
10 9 adantr ${⊢}\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{D}}\right)\right)\to {E}\in \mathrm{Cat}$
11 eqid ${⊢}{D}\mathrm{FuncCat}{E}={D}\mathrm{FuncCat}{E}$
12 1 11 2 3 4 curfcl ${⊢}{\phi }\to {G}\in \left({C}\mathrm{Func}\left({D}\mathrm{FuncCat}{E}\right)\right)$
13 12 adantr ${⊢}\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{D}}\right)\right)\to {G}\in \left({C}\mathrm{Func}\left({D}\mathrm{FuncCat}{E}\right)\right)$
14 eqid ${⊢}{\mathrm{Base}}_{{C}}={\mathrm{Base}}_{{C}}$
15 eqid ${⊢}{\mathrm{Base}}_{{D}}={\mathrm{Base}}_{{D}}$
16 simprl ${⊢}\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{D}}\right)\right)\to {x}\in {\mathrm{Base}}_{{C}}$
17 simprr ${⊢}\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{D}}\right)\right)\to {y}\in {\mathrm{Base}}_{{D}}$
18 5 6 10 13 14 15 16 17 uncf1 ${⊢}\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{D}}\right)\right)\to {x}{1}^{st}\left(⟨“{C}{D}{E}”⟩{uncurry}_{F}{G}\right){y}={1}^{st}\left({1}^{st}\left({G}\right)\left({x}\right)\right)\left({y}\right)$
19 2 adantr ${⊢}\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{D}}\right)\right)\to {C}\in \mathrm{Cat}$
20 4 adantr ${⊢}\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{D}}\right)\right)\to {F}\in \left(\left({C}{×}_{c}{D}\right)\mathrm{Func}{E}\right)$
21 eqid ${⊢}{1}^{st}\left({G}\right)\left({x}\right)={1}^{st}\left({G}\right)\left({x}\right)$
22 1 14 19 6 20 15 16 21 17 curf11 ${⊢}\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{D}}\right)\right)\to {1}^{st}\left({1}^{st}\left({G}\right)\left({x}\right)\right)\left({y}\right)={x}{1}^{st}\left({F}\right){y}$
23 18 22 eqtrd ${⊢}\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{D}}\right)\right)\to {x}{1}^{st}\left(⟨“{C}{D}{E}”⟩{uncurry}_{F}{G}\right){y}={x}{1}^{st}\left({F}\right){y}$
24 23 ralrimivva ${⊢}{\phi }\to \forall {x}\in {\mathrm{Base}}_{{C}}\phantom{\rule{.4em}{0ex}}\forall {y}\in {\mathrm{Base}}_{{D}}\phantom{\rule{.4em}{0ex}}{x}{1}^{st}\left(⟨“{C}{D}{E}”⟩{uncurry}_{F}{G}\right){y}={x}{1}^{st}\left({F}\right){y}$
25 eqid ${⊢}{C}{×}_{c}{D}={C}{×}_{c}{D}$
26 25 14 15 xpcbas ${⊢}{\mathrm{Base}}_{{C}}×{\mathrm{Base}}_{{D}}={\mathrm{Base}}_{\left({C}{×}_{c}{D}\right)}$
27 eqid ${⊢}{\mathrm{Base}}_{{E}}={\mathrm{Base}}_{{E}}$
28 relfunc ${⊢}\mathrm{Rel}\left(\left({C}{×}_{c}{D}\right)\mathrm{Func}{E}\right)$
29 5 3 9 12 uncfcl ${⊢}{\phi }\to ⟨“{C}{D}{E}”⟩{uncurry}_{F}{G}\in \left(\left({C}{×}_{c}{D}\right)\mathrm{Func}{E}\right)$
30 1st2ndbr ${⊢}\left(\mathrm{Rel}\left(\left({C}{×}_{c}{D}\right)\mathrm{Func}{E}\right)\wedge ⟨“{C}{D}{E}”⟩{uncurry}_{F}{G}\in \left(\left({C}{×}_{c}{D}\right)\mathrm{Func}{E}\right)\right)\to {1}^{st}\left(⟨“{C}{D}{E}”⟩{uncurry}_{F}{G}\right)\left(\left({C}{×}_{c}{D}\right)\mathrm{Func}{E}\right){2}^{nd}\left(⟨“{C}{D}{E}”⟩{uncurry}_{F}{G}\right)$
31 28 29 30 sylancr ${⊢}{\phi }\to {1}^{st}\left(⟨“{C}{D}{E}”⟩{uncurry}_{F}{G}\right)\left(\left({C}{×}_{c}{D}\right)\mathrm{Func}{E}\right){2}^{nd}\left(⟨“{C}{D}{E}”⟩{uncurry}_{F}{G}\right)$
32 26 27 31 funcf1 ${⊢}{\phi }\to {1}^{st}\left(⟨“{C}{D}{E}”⟩{uncurry}_{F}{G}\right):{\mathrm{Base}}_{{C}}×{\mathrm{Base}}_{{D}}⟶{\mathrm{Base}}_{{E}}$
33 32 ffnd ${⊢}{\phi }\to {1}^{st}\left(⟨“{C}{D}{E}”⟩{uncurry}_{F}{G}\right)Fn\left({\mathrm{Base}}_{{C}}×{\mathrm{Base}}_{{D}}\right)$
34 1st2ndbr ${⊢}\left(\mathrm{Rel}\left(\left({C}{×}_{c}{D}\right)\mathrm{Func}{E}\right)\wedge {F}\in \left(\left({C}{×}_{c}{D}\right)\mathrm{Func}{E}\right)\right)\to {1}^{st}\left({F}\right)\left(\left({C}{×}_{c}{D}\right)\mathrm{Func}{E}\right){2}^{nd}\left({F}\right)$
35 28 4 34 sylancr ${⊢}{\phi }\to {1}^{st}\left({F}\right)\left(\left({C}{×}_{c}{D}\right)\mathrm{Func}{E}\right){2}^{nd}\left({F}\right)$
36 26 27 35 funcf1 ${⊢}{\phi }\to {1}^{st}\left({F}\right):{\mathrm{Base}}_{{C}}×{\mathrm{Base}}_{{D}}⟶{\mathrm{Base}}_{{E}}$
37 36 ffnd ${⊢}{\phi }\to {1}^{st}\left({F}\right)Fn\left({\mathrm{Base}}_{{C}}×{\mathrm{Base}}_{{D}}\right)$
38 eqfnov2 ${⊢}\left({1}^{st}\left(⟨“{C}{D}{E}”⟩{uncurry}_{F}{G}\right)Fn\left({\mathrm{Base}}_{{C}}×{\mathrm{Base}}_{{D}}\right)\wedge {1}^{st}\left({F}\right)Fn\left({\mathrm{Base}}_{{C}}×{\mathrm{Base}}_{{D}}\right)\right)\to \left({1}^{st}\left(⟨“{C}{D}{E}”⟩{uncurry}_{F}{G}\right)={1}^{st}\left({F}\right)↔\forall {x}\in {\mathrm{Base}}_{{C}}\phantom{\rule{.4em}{0ex}}\forall {y}\in {\mathrm{Base}}_{{D}}\phantom{\rule{.4em}{0ex}}{x}{1}^{st}\left(⟨“{C}{D}{E}”⟩{uncurry}_{F}{G}\right){y}={x}{1}^{st}\left({F}\right){y}\right)$
39 33 37 38 syl2anc ${⊢}{\phi }\to \left({1}^{st}\left(⟨“{C}{D}{E}”⟩{uncurry}_{F}{G}\right)={1}^{st}\left({F}\right)↔\forall {x}\in {\mathrm{Base}}_{{C}}\phantom{\rule{.4em}{0ex}}\forall {y}\in {\mathrm{Base}}_{{D}}\phantom{\rule{.4em}{0ex}}{x}{1}^{st}\left(⟨“{C}{D}{E}”⟩{uncurry}_{F}{G}\right){y}={x}{1}^{st}\left({F}\right){y}\right)$
40 24 39 mpbird ${⊢}{\phi }\to {1}^{st}\left(⟨“{C}{D}{E}”⟩{uncurry}_{F}{G}\right)={1}^{st}\left({F}\right)$
41 3 ad3antrrr ${⊢}\left(\left(\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{D}}\right)\right)\wedge \left({z}\in {\mathrm{Base}}_{{C}}\wedge {w}\in {\mathrm{Base}}_{{D}}\right)\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}\right){z}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({D}\right){w}\right)\right)\right)\to {D}\in \mathrm{Cat}$
42 9 ad3antrrr ${⊢}\left(\left(\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{D}}\right)\right)\wedge \left({z}\in {\mathrm{Base}}_{{C}}\wedge {w}\in {\mathrm{Base}}_{{D}}\right)\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}\right){z}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({D}\right){w}\right)\right)\right)\to {E}\in \mathrm{Cat}$
43 12 ad3antrrr ${⊢}\left(\left(\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{D}}\right)\right)\wedge \left({z}\in {\mathrm{Base}}_{{C}}\wedge {w}\in {\mathrm{Base}}_{{D}}\right)\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}\right){z}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({D}\right){w}\right)\right)\right)\to {G}\in \left({C}\mathrm{Func}\left({D}\mathrm{FuncCat}{E}\right)\right)$
44 16 adantr ${⊢}\left(\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{D}}\right)\right)\wedge \left({z}\in {\mathrm{Base}}_{{C}}\wedge {w}\in {\mathrm{Base}}_{{D}}\right)\right)\to {x}\in {\mathrm{Base}}_{{C}}$
45 44 adantr ${⊢}\left(\left(\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{D}}\right)\right)\wedge \left({z}\in {\mathrm{Base}}_{{C}}\wedge {w}\in {\mathrm{Base}}_{{D}}\right)\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}\right){z}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({D}\right){w}\right)\right)\right)\to {x}\in {\mathrm{Base}}_{{C}}$
46 17 adantr ${⊢}\left(\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{D}}\right)\right)\wedge \left({z}\in {\mathrm{Base}}_{{C}}\wedge {w}\in {\mathrm{Base}}_{{D}}\right)\right)\to {y}\in {\mathrm{Base}}_{{D}}$
47 46 adantr ${⊢}\left(\left(\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{D}}\right)\right)\wedge \left({z}\in {\mathrm{Base}}_{{C}}\wedge {w}\in {\mathrm{Base}}_{{D}}\right)\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}\right){z}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({D}\right){w}\right)\right)\right)\to {y}\in {\mathrm{Base}}_{{D}}$
48 eqid ${⊢}\mathrm{Hom}\left({C}\right)=\mathrm{Hom}\left({C}\right)$
49 eqid ${⊢}\mathrm{Hom}\left({D}\right)=\mathrm{Hom}\left({D}\right)$
50 simprl ${⊢}\left(\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{D}}\right)\right)\wedge \left({z}\in {\mathrm{Base}}_{{C}}\wedge {w}\in {\mathrm{Base}}_{{D}}\right)\right)\to {z}\in {\mathrm{Base}}_{{C}}$
51 50 adantr ${⊢}\left(\left(\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{D}}\right)\right)\wedge \left({z}\in {\mathrm{Base}}_{{C}}\wedge {w}\in {\mathrm{Base}}_{{D}}\right)\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}\right){z}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({D}\right){w}\right)\right)\right)\to {z}\in {\mathrm{Base}}_{{C}}$
52 simprr ${⊢}\left(\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{D}}\right)\right)\wedge \left({z}\in {\mathrm{Base}}_{{C}}\wedge {w}\in {\mathrm{Base}}_{{D}}\right)\right)\to {w}\in {\mathrm{Base}}_{{D}}$
53 52 adantr ${⊢}\left(\left(\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{D}}\right)\right)\wedge \left({z}\in {\mathrm{Base}}_{{C}}\wedge {w}\in {\mathrm{Base}}_{{D}}\right)\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}\right){z}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({D}\right){w}\right)\right)\right)\to {w}\in {\mathrm{Base}}_{{D}}$
54 simprl ${⊢}\left(\left(\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{D}}\right)\right)\wedge \left({z}\in {\mathrm{Base}}_{{C}}\wedge {w}\in {\mathrm{Base}}_{{D}}\right)\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}\right){z}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({D}\right){w}\right)\right)\right)\to {f}\in \left({x}\mathrm{Hom}\left({C}\right){z}\right)$
55 simprr ${⊢}\left(\left(\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{D}}\right)\right)\wedge \left({z}\in {\mathrm{Base}}_{{C}}\wedge {w}\in {\mathrm{Base}}_{{D}}\right)\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}\right){z}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({D}\right){w}\right)\right)\right)\to {g}\in \left({y}\mathrm{Hom}\left({D}\right){w}\right)$
56 5 41 42 43 14 15 45 47 48 49 51 53 54 55 uncf2 ${⊢}\left(\left(\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{D}}\right)\right)\wedge \left({z}\in {\mathrm{Base}}_{{C}}\wedge {w}\in {\mathrm{Base}}_{{D}}\right)\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}\right){z}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({D}\right){w}\right)\right)\right)\to {f}\left(⟨{x},{y}⟩{2}^{nd}\left(⟨“{C}{D}{E}”⟩{uncurry}_{F}{G}\right)⟨{z},{w}⟩\right){g}=\left({x}{2}^{nd}\left({G}\right){z}\right)\left({f}\right)\left({w}\right)\left(⟨{1}^{st}\left({1}^{st}\left({G}\right)\left({x}\right)\right)\left({y}\right),{1}^{st}\left({1}^{st}\left({G}\right)\left({x}\right)\right)\left({w}\right)⟩\mathrm{comp}\left({E}\right){1}^{st}\left({1}^{st}\left({G}\right)\left({z}\right)\right)\left({w}\right)\right)\left({y}{2}^{nd}\left({1}^{st}\left({G}\right)\left({x}\right)\right){w}\right)\left({g}\right)$
57 2 ad3antrrr ${⊢}\left(\left(\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{D}}\right)\right)\wedge \left({z}\in {\mathrm{Base}}_{{C}}\wedge {w}\in {\mathrm{Base}}_{{D}}\right)\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}\right){z}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({D}\right){w}\right)\right)\right)\to {C}\in \mathrm{Cat}$
58 4 ad3antrrr ${⊢}\left(\left(\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{D}}\right)\right)\wedge \left({z}\in {\mathrm{Base}}_{{C}}\wedge {w}\in {\mathrm{Base}}_{{D}}\right)\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}\right){z}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({D}\right){w}\right)\right)\right)\to {F}\in \left(\left({C}{×}_{c}{D}\right)\mathrm{Func}{E}\right)$
59 1 14 57 41 58 15 45 21 47 curf11 ${⊢}\left(\left(\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{D}}\right)\right)\wedge \left({z}\in {\mathrm{Base}}_{{C}}\wedge {w}\in {\mathrm{Base}}_{{D}}\right)\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}\right){z}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({D}\right){w}\right)\right)\right)\to {1}^{st}\left({1}^{st}\left({G}\right)\left({x}\right)\right)\left({y}\right)={x}{1}^{st}\left({F}\right){y}$
60 df-ov ${⊢}{x}{1}^{st}\left({F}\right){y}={1}^{st}\left({F}\right)\left(⟨{x},{y}⟩\right)$
61 59 60 syl6eq ${⊢}\left(\left(\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{D}}\right)\right)\wedge \left({z}\in {\mathrm{Base}}_{{C}}\wedge {w}\in {\mathrm{Base}}_{{D}}\right)\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}\right){z}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({D}\right){w}\right)\right)\right)\to {1}^{st}\left({1}^{st}\left({G}\right)\left({x}\right)\right)\left({y}\right)={1}^{st}\left({F}\right)\left(⟨{x},{y}⟩\right)$
62 1 14 57 41 58 15 45 21 53 curf11 ${⊢}\left(\left(\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{D}}\right)\right)\wedge \left({z}\in {\mathrm{Base}}_{{C}}\wedge {w}\in {\mathrm{Base}}_{{D}}\right)\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}\right){z}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({D}\right){w}\right)\right)\right)\to {1}^{st}\left({1}^{st}\left({G}\right)\left({x}\right)\right)\left({w}\right)={x}{1}^{st}\left({F}\right){w}$
63 df-ov ${⊢}{x}{1}^{st}\left({F}\right){w}={1}^{st}\left({F}\right)\left(⟨{x},{w}⟩\right)$
64 62 63 syl6eq ${⊢}\left(\left(\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{D}}\right)\right)\wedge \left({z}\in {\mathrm{Base}}_{{C}}\wedge {w}\in {\mathrm{Base}}_{{D}}\right)\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}\right){z}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({D}\right){w}\right)\right)\right)\to {1}^{st}\left({1}^{st}\left({G}\right)\left({x}\right)\right)\left({w}\right)={1}^{st}\left({F}\right)\left(⟨{x},{w}⟩\right)$
65 61 64 opeq12d ${⊢}\left(\left(\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{D}}\right)\right)\wedge \left({z}\in {\mathrm{Base}}_{{C}}\wedge {w}\in {\mathrm{Base}}_{{D}}\right)\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}\right){z}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({D}\right){w}\right)\right)\right)\to ⟨{1}^{st}\left({1}^{st}\left({G}\right)\left({x}\right)\right)\left({y}\right),{1}^{st}\left({1}^{st}\left({G}\right)\left({x}\right)\right)\left({w}\right)⟩=⟨{1}^{st}\left({F}\right)\left(⟨{x},{y}⟩\right),{1}^{st}\left({F}\right)\left(⟨{x},{w}⟩\right)⟩$
66 eqid ${⊢}{1}^{st}\left({G}\right)\left({z}\right)={1}^{st}\left({G}\right)\left({z}\right)$
67 1 14 57 41 58 15 51 66 53 curf11 ${⊢}\left(\left(\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{D}}\right)\right)\wedge \left({z}\in {\mathrm{Base}}_{{C}}\wedge {w}\in {\mathrm{Base}}_{{D}}\right)\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}\right){z}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({D}\right){w}\right)\right)\right)\to {1}^{st}\left({1}^{st}\left({G}\right)\left({z}\right)\right)\left({w}\right)={z}{1}^{st}\left({F}\right){w}$
68 df-ov ${⊢}{z}{1}^{st}\left({F}\right){w}={1}^{st}\left({F}\right)\left(⟨{z},{w}⟩\right)$
69 67 68 syl6eq ${⊢}\left(\left(\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{D}}\right)\right)\wedge \left({z}\in {\mathrm{Base}}_{{C}}\wedge {w}\in {\mathrm{Base}}_{{D}}\right)\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}\right){z}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({D}\right){w}\right)\right)\right)\to {1}^{st}\left({1}^{st}\left({G}\right)\left({z}\right)\right)\left({w}\right)={1}^{st}\left({F}\right)\left(⟨{z},{w}⟩\right)$
70 65 69 oveq12d ${⊢}\left(\left(\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{D}}\right)\right)\wedge \left({z}\in {\mathrm{Base}}_{{C}}\wedge {w}\in {\mathrm{Base}}_{{D}}\right)\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}\right){z}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({D}\right){w}\right)\right)\right)\to ⟨{1}^{st}\left({1}^{st}\left({G}\right)\left({x}\right)\right)\left({y}\right),{1}^{st}\left({1}^{st}\left({G}\right)\left({x}\right)\right)\left({w}\right)⟩\mathrm{comp}\left({E}\right){1}^{st}\left({1}^{st}\left({G}\right)\left({z}\right)\right)\left({w}\right)=⟨{1}^{st}\left({F}\right)\left(⟨{x},{y}⟩\right),{1}^{st}\left({F}\right)\left(⟨{x},{w}⟩\right)⟩\mathrm{comp}\left({E}\right){1}^{st}\left({F}\right)\left(⟨{z},{w}⟩\right)$
71 eqid ${⊢}\mathrm{Id}\left({D}\right)=\mathrm{Id}\left({D}\right)$
72 eqid ${⊢}\left({x}{2}^{nd}\left({G}\right){z}\right)\left({f}\right)=\left({x}{2}^{nd}\left({G}\right){z}\right)\left({f}\right)$
73 1 14 57 41 58 15 48 71 45 51 54 72 53 curf2val ${⊢}\left(\left(\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{D}}\right)\right)\wedge \left({z}\in {\mathrm{Base}}_{{C}}\wedge {w}\in {\mathrm{Base}}_{{D}}\right)\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}\right){z}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({D}\right){w}\right)\right)\right)\to \left({x}{2}^{nd}\left({G}\right){z}\right)\left({f}\right)\left({w}\right)={f}\left(⟨{x},{w}⟩{2}^{nd}\left({F}\right)⟨{z},{w}⟩\right)\mathrm{Id}\left({D}\right)\left({w}\right)$
74 df-ov ${⊢}{f}\left(⟨{x},{w}⟩{2}^{nd}\left({F}\right)⟨{z},{w}⟩\right)\mathrm{Id}\left({D}\right)\left({w}\right)=\left(⟨{x},{w}⟩{2}^{nd}\left({F}\right)⟨{z},{w}⟩\right)\left(⟨{f},\mathrm{Id}\left({D}\right)\left({w}\right)⟩\right)$
75 73 74 syl6eq ${⊢}\left(\left(\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{D}}\right)\right)\wedge \left({z}\in {\mathrm{Base}}_{{C}}\wedge {w}\in {\mathrm{Base}}_{{D}}\right)\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}\right){z}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({D}\right){w}\right)\right)\right)\to \left({x}{2}^{nd}\left({G}\right){z}\right)\left({f}\right)\left({w}\right)=\left(⟨{x},{w}⟩{2}^{nd}\left({F}\right)⟨{z},{w}⟩\right)\left(⟨{f},\mathrm{Id}\left({D}\right)\left({w}\right)⟩\right)$
76 eqid ${⊢}\mathrm{Id}\left({C}\right)=\mathrm{Id}\left({C}\right)$
77 1 14 57 41 58 15 45 21 47 49 76 53 55 curf12 ${⊢}\left(\left(\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{D}}\right)\right)\wedge \left({z}\in {\mathrm{Base}}_{{C}}\wedge {w}\in {\mathrm{Base}}_{{D}}\right)\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}\right){z}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({D}\right){w}\right)\right)\right)\to \left({y}{2}^{nd}\left({1}^{st}\left({G}\right)\left({x}\right)\right){w}\right)\left({g}\right)=\mathrm{Id}\left({C}\right)\left({x}\right)\left(⟨{x},{y}⟩{2}^{nd}\left({F}\right)⟨{x},{w}⟩\right){g}$
78 df-ov ${⊢}\mathrm{Id}\left({C}\right)\left({x}\right)\left(⟨{x},{y}⟩{2}^{nd}\left({F}\right)⟨{x},{w}⟩\right){g}=\left(⟨{x},{y}⟩{2}^{nd}\left({F}\right)⟨{x},{w}⟩\right)\left(⟨\mathrm{Id}\left({C}\right)\left({x}\right),{g}⟩\right)$
79 77 78 syl6eq ${⊢}\left(\left(\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{D}}\right)\right)\wedge \left({z}\in {\mathrm{Base}}_{{C}}\wedge {w}\in {\mathrm{Base}}_{{D}}\right)\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}\right){z}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({D}\right){w}\right)\right)\right)\to \left({y}{2}^{nd}\left({1}^{st}\left({G}\right)\left({x}\right)\right){w}\right)\left({g}\right)=\left(⟨{x},{y}⟩{2}^{nd}\left({F}\right)⟨{x},{w}⟩\right)\left(⟨\mathrm{Id}\left({C}\right)\left({x}\right),{g}⟩\right)$
80 70 75 79 oveq123d ${⊢}\left(\left(\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{D}}\right)\right)\wedge \left({z}\in {\mathrm{Base}}_{{C}}\wedge {w}\in {\mathrm{Base}}_{{D}}\right)\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}\right){z}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({D}\right){w}\right)\right)\right)\to \left({x}{2}^{nd}\left({G}\right){z}\right)\left({f}\right)\left({w}\right)\left(⟨{1}^{st}\left({1}^{st}\left({G}\right)\left({x}\right)\right)\left({y}\right),{1}^{st}\left({1}^{st}\left({G}\right)\left({x}\right)\right)\left({w}\right)⟩\mathrm{comp}\left({E}\right){1}^{st}\left({1}^{st}\left({G}\right)\left({z}\right)\right)\left({w}\right)\right)\left({y}{2}^{nd}\left({1}^{st}\left({G}\right)\left({x}\right)\right){w}\right)\left({g}\right)=\left(⟨{x},{w}⟩{2}^{nd}\left({F}\right)⟨{z},{w}⟩\right)\left(⟨{f},\mathrm{Id}\left({D}\right)\left({w}\right)⟩\right)\left(⟨{1}^{st}\left({F}\right)\left(⟨{x},{y}⟩\right),{1}^{st}\left({F}\right)\left(⟨{x},{w}⟩\right)⟩\mathrm{comp}\left({E}\right){1}^{st}\left({F}\right)\left(⟨{z},{w}⟩\right)\right)\left(⟨{x},{y}⟩{2}^{nd}\left({F}\right)⟨{x},{w}⟩\right)\left(⟨\mathrm{Id}\left({C}\right)\left({x}\right),{g}⟩\right)$
81 eqid ${⊢}\mathrm{Hom}\left({C}{×}_{c}{D}\right)=\mathrm{Hom}\left({C}{×}_{c}{D}\right)$
82 eqid ${⊢}\mathrm{comp}\left({C}{×}_{c}{D}\right)=\mathrm{comp}\left({C}{×}_{c}{D}\right)$
83 eqid ${⊢}\mathrm{comp}\left({E}\right)=\mathrm{comp}\left({E}\right)$
84 35 ad2antrr ${⊢}\left(\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{D}}\right)\right)\wedge \left({z}\in {\mathrm{Base}}_{{C}}\wedge {w}\in {\mathrm{Base}}_{{D}}\right)\right)\to {1}^{st}\left({F}\right)\left(\left({C}{×}_{c}{D}\right)\mathrm{Func}{E}\right){2}^{nd}\left({F}\right)$
85 84 adantr ${⊢}\left(\left(\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{D}}\right)\right)\wedge \left({z}\in {\mathrm{Base}}_{{C}}\wedge {w}\in {\mathrm{Base}}_{{D}}\right)\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}\right){z}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({D}\right){w}\right)\right)\right)\to {1}^{st}\left({F}\right)\left(\left({C}{×}_{c}{D}\right)\mathrm{Func}{E}\right){2}^{nd}\left({F}\right)$
86 opelxpi ${⊢}\left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{D}}\right)\to ⟨{x},{y}⟩\in \left({\mathrm{Base}}_{{C}}×{\mathrm{Base}}_{{D}}\right)$
87 86 ad2antlr ${⊢}\left(\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{D}}\right)\right)\wedge \left({z}\in {\mathrm{Base}}_{{C}}\wedge {w}\in {\mathrm{Base}}_{{D}}\right)\right)\to ⟨{x},{y}⟩\in \left({\mathrm{Base}}_{{C}}×{\mathrm{Base}}_{{D}}\right)$
88 87 adantr ${⊢}\left(\left(\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{D}}\right)\right)\wedge \left({z}\in {\mathrm{Base}}_{{C}}\wedge {w}\in {\mathrm{Base}}_{{D}}\right)\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}\right){z}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({D}\right){w}\right)\right)\right)\to ⟨{x},{y}⟩\in \left({\mathrm{Base}}_{{C}}×{\mathrm{Base}}_{{D}}\right)$
89 45 53 opelxpd ${⊢}\left(\left(\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{D}}\right)\right)\wedge \left({z}\in {\mathrm{Base}}_{{C}}\wedge {w}\in {\mathrm{Base}}_{{D}}\right)\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}\right){z}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({D}\right){w}\right)\right)\right)\to ⟨{x},{w}⟩\in \left({\mathrm{Base}}_{{C}}×{\mathrm{Base}}_{{D}}\right)$
90 opelxpi ${⊢}\left({z}\in {\mathrm{Base}}_{{C}}\wedge {w}\in {\mathrm{Base}}_{{D}}\right)\to ⟨{z},{w}⟩\in \left({\mathrm{Base}}_{{C}}×{\mathrm{Base}}_{{D}}\right)$
91 90 adantl ${⊢}\left(\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{D}}\right)\right)\wedge \left({z}\in {\mathrm{Base}}_{{C}}\wedge {w}\in {\mathrm{Base}}_{{D}}\right)\right)\to ⟨{z},{w}⟩\in \left({\mathrm{Base}}_{{C}}×{\mathrm{Base}}_{{D}}\right)$
92 91 adantr ${⊢}\left(\left(\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{D}}\right)\right)\wedge \left({z}\in {\mathrm{Base}}_{{C}}\wedge {w}\in {\mathrm{Base}}_{{D}}\right)\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}\right){z}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({D}\right){w}\right)\right)\right)\to ⟨{z},{w}⟩\in \left({\mathrm{Base}}_{{C}}×{\mathrm{Base}}_{{D}}\right)$
93 14 48 76 57 45 catidcl ${⊢}\left(\left(\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{D}}\right)\right)\wedge \left({z}\in {\mathrm{Base}}_{{C}}\wedge {w}\in {\mathrm{Base}}_{{D}}\right)\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}\right){z}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({D}\right){w}\right)\right)\right)\to \mathrm{Id}\left({C}\right)\left({x}\right)\in \left({x}\mathrm{Hom}\left({C}\right){x}\right)$
94 93 55 opelxpd ${⊢}\left(\left(\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{D}}\right)\right)\wedge \left({z}\in {\mathrm{Base}}_{{C}}\wedge {w}\in {\mathrm{Base}}_{{D}}\right)\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}\right){z}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({D}\right){w}\right)\right)\right)\to ⟨\mathrm{Id}\left({C}\right)\left({x}\right),{g}⟩\in \left(\left({x}\mathrm{Hom}\left({C}\right){x}\right)×\left({y}\mathrm{Hom}\left({D}\right){w}\right)\right)$
95 25 14 15 48 49 45 47 45 53 81 xpchom2 ${⊢}\left(\left(\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{D}}\right)\right)\wedge \left({z}\in {\mathrm{Base}}_{{C}}\wedge {w}\in {\mathrm{Base}}_{{D}}\right)\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}\right){z}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({D}\right){w}\right)\right)\right)\to ⟨{x},{y}⟩\mathrm{Hom}\left({C}{×}_{c}{D}\right)⟨{x},{w}⟩=\left({x}\mathrm{Hom}\left({C}\right){x}\right)×\left({y}\mathrm{Hom}\left({D}\right){w}\right)$
96 94 95 eleqtrrd ${⊢}\left(\left(\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{D}}\right)\right)\wedge \left({z}\in {\mathrm{Base}}_{{C}}\wedge {w}\in {\mathrm{Base}}_{{D}}\right)\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}\right){z}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({D}\right){w}\right)\right)\right)\to ⟨\mathrm{Id}\left({C}\right)\left({x}\right),{g}⟩\in \left(⟨{x},{y}⟩\mathrm{Hom}\left({C}{×}_{c}{D}\right)⟨{x},{w}⟩\right)$
97 15 49 71 41 53 catidcl ${⊢}\left(\left(\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{D}}\right)\right)\wedge \left({z}\in {\mathrm{Base}}_{{C}}\wedge {w}\in {\mathrm{Base}}_{{D}}\right)\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}\right){z}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({D}\right){w}\right)\right)\right)\to \mathrm{Id}\left({D}\right)\left({w}\right)\in \left({w}\mathrm{Hom}\left({D}\right){w}\right)$
98 54 97 opelxpd ${⊢}\left(\left(\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{D}}\right)\right)\wedge \left({z}\in {\mathrm{Base}}_{{C}}\wedge {w}\in {\mathrm{Base}}_{{D}}\right)\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}\right){z}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({D}\right){w}\right)\right)\right)\to ⟨{f},\mathrm{Id}\left({D}\right)\left({w}\right)⟩\in \left(\left({x}\mathrm{Hom}\left({C}\right){z}\right)×\left({w}\mathrm{Hom}\left({D}\right){w}\right)\right)$
99 25 14 15 48 49 45 53 51 53 81 xpchom2 ${⊢}\left(\left(\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{D}}\right)\right)\wedge \left({z}\in {\mathrm{Base}}_{{C}}\wedge {w}\in {\mathrm{Base}}_{{D}}\right)\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}\right){z}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({D}\right){w}\right)\right)\right)\to ⟨{x},{w}⟩\mathrm{Hom}\left({C}{×}_{c}{D}\right)⟨{z},{w}⟩=\left({x}\mathrm{Hom}\left({C}\right){z}\right)×\left({w}\mathrm{Hom}\left({D}\right){w}\right)$
100 98 99 eleqtrrd ${⊢}\left(\left(\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{D}}\right)\right)\wedge \left({z}\in {\mathrm{Base}}_{{C}}\wedge {w}\in {\mathrm{Base}}_{{D}}\right)\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}\right){z}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({D}\right){w}\right)\right)\right)\to ⟨{f},\mathrm{Id}\left({D}\right)\left({w}\right)⟩\in \left(⟨{x},{w}⟩\mathrm{Hom}\left({C}{×}_{c}{D}\right)⟨{z},{w}⟩\right)$
101 26 81 82 83 85 88 89 92 96 100 funcco ${⊢}\left(\left(\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{D}}\right)\right)\wedge \left({z}\in {\mathrm{Base}}_{{C}}\wedge {w}\in {\mathrm{Base}}_{{D}}\right)\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}\right){z}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({D}\right){w}\right)\right)\right)\to \left(⟨{x},{y}⟩{2}^{nd}\left({F}\right)⟨{z},{w}⟩\right)\left(⟨{f},\mathrm{Id}\left({D}\right)\left({w}\right)⟩\left(⟨⟨{x},{y}⟩,⟨{x},{w}⟩⟩\mathrm{comp}\left({C}{×}_{c}{D}\right)⟨{z},{w}⟩\right)⟨\mathrm{Id}\left({C}\right)\left({x}\right),{g}⟩\right)=\left(⟨{x},{w}⟩{2}^{nd}\left({F}\right)⟨{z},{w}⟩\right)\left(⟨{f},\mathrm{Id}\left({D}\right)\left({w}\right)⟩\right)\left(⟨{1}^{st}\left({F}\right)\left(⟨{x},{y}⟩\right),{1}^{st}\left({F}\right)\left(⟨{x},{w}⟩\right)⟩\mathrm{comp}\left({E}\right){1}^{st}\left({F}\right)\left(⟨{z},{w}⟩\right)\right)\left(⟨{x},{y}⟩{2}^{nd}\left({F}\right)⟨{x},{w}⟩\right)\left(⟨\mathrm{Id}\left({C}\right)\left({x}\right),{g}⟩\right)$
102 eqid ${⊢}\mathrm{comp}\left({C}\right)=\mathrm{comp}\left({C}\right)$
103 eqid ${⊢}\mathrm{comp}\left({D}\right)=\mathrm{comp}\left({D}\right)$
104 25 14 15 48 49 45 47 45 53 102 103 82 51 53 93 55 54 97 xpcco2 ${⊢}\left(\left(\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{D}}\right)\right)\wedge \left({z}\in {\mathrm{Base}}_{{C}}\wedge {w}\in {\mathrm{Base}}_{{D}}\right)\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}\right){z}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({D}\right){w}\right)\right)\right)\to ⟨{f},\mathrm{Id}\left({D}\right)\left({w}\right)⟩\left(⟨⟨{x},{y}⟩,⟨{x},{w}⟩⟩\mathrm{comp}\left({C}{×}_{c}{D}\right)⟨{z},{w}⟩\right)⟨\mathrm{Id}\left({C}\right)\left({x}\right),{g}⟩=⟨{f}\left(⟨{x},{x}⟩\mathrm{comp}\left({C}\right){z}\right)\mathrm{Id}\left({C}\right)\left({x}\right),\mathrm{Id}\left({D}\right)\left({w}\right)\left(⟨{y},{w}⟩\mathrm{comp}\left({D}\right){w}\right){g}⟩$
105 104 fveq2d ${⊢}\left(\left(\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{D}}\right)\right)\wedge \left({z}\in {\mathrm{Base}}_{{C}}\wedge {w}\in {\mathrm{Base}}_{{D}}\right)\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}\right){z}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({D}\right){w}\right)\right)\right)\to \left(⟨{x},{y}⟩{2}^{nd}\left({F}\right)⟨{z},{w}⟩\right)\left(⟨{f},\mathrm{Id}\left({D}\right)\left({w}\right)⟩\left(⟨⟨{x},{y}⟩,⟨{x},{w}⟩⟩\mathrm{comp}\left({C}{×}_{c}{D}\right)⟨{z},{w}⟩\right)⟨\mathrm{Id}\left({C}\right)\left({x}\right),{g}⟩\right)=\left(⟨{x},{y}⟩{2}^{nd}\left({F}\right)⟨{z},{w}⟩\right)\left(⟨{f}\left(⟨{x},{x}⟩\mathrm{comp}\left({C}\right){z}\right)\mathrm{Id}\left({C}\right)\left({x}\right),\mathrm{Id}\left({D}\right)\left({w}\right)\left(⟨{y},{w}⟩\mathrm{comp}\left({D}\right){w}\right){g}⟩\right)$
106 df-ov ${⊢}\left({f}\left(⟨{x},{x}⟩\mathrm{comp}\left({C}\right){z}\right)\mathrm{Id}\left({C}\right)\left({x}\right)\right)\left(⟨{x},{y}⟩{2}^{nd}\left({F}\right)⟨{z},{w}⟩\right)\left(\mathrm{Id}\left({D}\right)\left({w}\right)\left(⟨{y},{w}⟩\mathrm{comp}\left({D}\right){w}\right){g}\right)=\left(⟨{x},{y}⟩{2}^{nd}\left({F}\right)⟨{z},{w}⟩\right)\left(⟨{f}\left(⟨{x},{x}⟩\mathrm{comp}\left({C}\right){z}\right)\mathrm{Id}\left({C}\right)\left({x}\right),\mathrm{Id}\left({D}\right)\left({w}\right)\left(⟨{y},{w}⟩\mathrm{comp}\left({D}\right){w}\right){g}⟩\right)$
107 105 106 syl6eqr ${⊢}\left(\left(\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{D}}\right)\right)\wedge \left({z}\in {\mathrm{Base}}_{{C}}\wedge {w}\in {\mathrm{Base}}_{{D}}\right)\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}\right){z}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({D}\right){w}\right)\right)\right)\to \left(⟨{x},{y}⟩{2}^{nd}\left({F}\right)⟨{z},{w}⟩\right)\left(⟨{f},\mathrm{Id}\left({D}\right)\left({w}\right)⟩\left(⟨⟨{x},{y}⟩,⟨{x},{w}⟩⟩\mathrm{comp}\left({C}{×}_{c}{D}\right)⟨{z},{w}⟩\right)⟨\mathrm{Id}\left({C}\right)\left({x}\right),{g}⟩\right)=\left({f}\left(⟨{x},{x}⟩\mathrm{comp}\left({C}\right){z}\right)\mathrm{Id}\left({C}\right)\left({x}\right)\right)\left(⟨{x},{y}⟩{2}^{nd}\left({F}\right)⟨{z},{w}⟩\right)\left(\mathrm{Id}\left({D}\right)\left({w}\right)\left(⟨{y},{w}⟩\mathrm{comp}\left({D}\right){w}\right){g}\right)$
108 14 48 76 57 45 102 51 54 catrid ${⊢}\left(\left(\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{D}}\right)\right)\wedge \left({z}\in {\mathrm{Base}}_{{C}}\wedge {w}\in {\mathrm{Base}}_{{D}}\right)\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}\right){z}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({D}\right){w}\right)\right)\right)\to {f}\left(⟨{x},{x}⟩\mathrm{comp}\left({C}\right){z}\right)\mathrm{Id}\left({C}\right)\left({x}\right)={f}$
109 15 49 71 41 47 103 53 55 catlid ${⊢}\left(\left(\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{D}}\right)\right)\wedge \left({z}\in {\mathrm{Base}}_{{C}}\wedge {w}\in {\mathrm{Base}}_{{D}}\right)\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}\right){z}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({D}\right){w}\right)\right)\right)\to \mathrm{Id}\left({D}\right)\left({w}\right)\left(⟨{y},{w}⟩\mathrm{comp}\left({D}\right){w}\right){g}={g}$
110 108 109 oveq12d ${⊢}\left(\left(\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{D}}\right)\right)\wedge \left({z}\in {\mathrm{Base}}_{{C}}\wedge {w}\in {\mathrm{Base}}_{{D}}\right)\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}\right){z}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({D}\right){w}\right)\right)\right)\to \left({f}\left(⟨{x},{x}⟩\mathrm{comp}\left({C}\right){z}\right)\mathrm{Id}\left({C}\right)\left({x}\right)\right)\left(⟨{x},{y}⟩{2}^{nd}\left({F}\right)⟨{z},{w}⟩\right)\left(\mathrm{Id}\left({D}\right)\left({w}\right)\left(⟨{y},{w}⟩\mathrm{comp}\left({D}\right){w}\right){g}\right)={f}\left(⟨{x},{y}⟩{2}^{nd}\left({F}\right)⟨{z},{w}⟩\right){g}$
111 107 110 eqtrd ${⊢}\left(\left(\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{D}}\right)\right)\wedge \left({z}\in {\mathrm{Base}}_{{C}}\wedge {w}\in {\mathrm{Base}}_{{D}}\right)\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}\right){z}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({D}\right){w}\right)\right)\right)\to \left(⟨{x},{y}⟩{2}^{nd}\left({F}\right)⟨{z},{w}⟩\right)\left(⟨{f},\mathrm{Id}\left({D}\right)\left({w}\right)⟩\left(⟨⟨{x},{y}⟩,⟨{x},{w}⟩⟩\mathrm{comp}\left({C}{×}_{c}{D}\right)⟨{z},{w}⟩\right)⟨\mathrm{Id}\left({C}\right)\left({x}\right),{g}⟩\right)={f}\left(⟨{x},{y}⟩{2}^{nd}\left({F}\right)⟨{z},{w}⟩\right){g}$
112 80 101 111 3eqtr2d ${⊢}\left(\left(\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{D}}\right)\right)\wedge \left({z}\in {\mathrm{Base}}_{{C}}\wedge {w}\in {\mathrm{Base}}_{{D}}\right)\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}\right){z}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({D}\right){w}\right)\right)\right)\to \left({x}{2}^{nd}\left({G}\right){z}\right)\left({f}\right)\left({w}\right)\left(⟨{1}^{st}\left({1}^{st}\left({G}\right)\left({x}\right)\right)\left({y}\right),{1}^{st}\left({1}^{st}\left({G}\right)\left({x}\right)\right)\left({w}\right)⟩\mathrm{comp}\left({E}\right){1}^{st}\left({1}^{st}\left({G}\right)\left({z}\right)\right)\left({w}\right)\right)\left({y}{2}^{nd}\left({1}^{st}\left({G}\right)\left({x}\right)\right){w}\right)\left({g}\right)={f}\left(⟨{x},{y}⟩{2}^{nd}\left({F}\right)⟨{z},{w}⟩\right){g}$
113 56 112 eqtrd ${⊢}\left(\left(\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{D}}\right)\right)\wedge \left({z}\in {\mathrm{Base}}_{{C}}\wedge {w}\in {\mathrm{Base}}_{{D}}\right)\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}\right){z}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({D}\right){w}\right)\right)\right)\to {f}\left(⟨{x},{y}⟩{2}^{nd}\left(⟨“{C}{D}{E}”⟩{uncurry}_{F}{G}\right)⟨{z},{w}⟩\right){g}={f}\left(⟨{x},{y}⟩{2}^{nd}\left({F}\right)⟨{z},{w}⟩\right){g}$
114 113 ralrimivva ${⊢}\left(\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{D}}\right)\right)\wedge \left({z}\in {\mathrm{Base}}_{{C}}\wedge {w}\in {\mathrm{Base}}_{{D}}\right)\right)\to \forall {f}\in \left({x}\mathrm{Hom}\left({C}\right){z}\right)\phantom{\rule{.4em}{0ex}}\forall {g}\in \left({y}\mathrm{Hom}\left({D}\right){w}\right)\phantom{\rule{.4em}{0ex}}{f}\left(⟨{x},{y}⟩{2}^{nd}\left(⟨“{C}{D}{E}”⟩{uncurry}_{F}{G}\right)⟨{z},{w}⟩\right){g}={f}\left(⟨{x},{y}⟩{2}^{nd}\left({F}\right)⟨{z},{w}⟩\right){g}$
115 eqid ${⊢}\mathrm{Hom}\left({E}\right)=\mathrm{Hom}\left({E}\right)$
116 31 ad2antrr ${⊢}\left(\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{D}}\right)\right)\wedge \left({z}\in {\mathrm{Base}}_{{C}}\wedge {w}\in {\mathrm{Base}}_{{D}}\right)\right)\to {1}^{st}\left(⟨“{C}{D}{E}”⟩{uncurry}_{F}{G}\right)\left(\left({C}{×}_{c}{D}\right)\mathrm{Func}{E}\right){2}^{nd}\left(⟨“{C}{D}{E}”⟩{uncurry}_{F}{G}\right)$
117 26 81 115 116 87 91 funcf2 ${⊢}\left(\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{D}}\right)\right)\wedge \left({z}\in {\mathrm{Base}}_{{C}}\wedge {w}\in {\mathrm{Base}}_{{D}}\right)\right)\to \left(⟨{x},{y}⟩{2}^{nd}\left(⟨“{C}{D}{E}”⟩{uncurry}_{F}{G}\right)⟨{z},{w}⟩\right):⟨{x},{y}⟩\mathrm{Hom}\left({C}{×}_{c}{D}\right)⟨{z},{w}⟩⟶{1}^{st}\left(⟨“{C}{D}{E}”⟩{uncurry}_{F}{G}\right)\left(⟨{x},{y}⟩\right)\mathrm{Hom}\left({E}\right){1}^{st}\left(⟨“{C}{D}{E}”⟩{uncurry}_{F}{G}\right)\left(⟨{z},{w}⟩\right)$
118 25 14 15 48 49 44 46 50 52 81 xpchom2 ${⊢}\left(\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{D}}\right)\right)\wedge \left({z}\in {\mathrm{Base}}_{{C}}\wedge {w}\in {\mathrm{Base}}_{{D}}\right)\right)\to ⟨{x},{y}⟩\mathrm{Hom}\left({C}{×}_{c}{D}\right)⟨{z},{w}⟩=\left({x}\mathrm{Hom}\left({C}\right){z}\right)×\left({y}\mathrm{Hom}\left({D}\right){w}\right)$
119 118 feq2d ${⊢}\left(\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{D}}\right)\right)\wedge \left({z}\in {\mathrm{Base}}_{{C}}\wedge {w}\in {\mathrm{Base}}_{{D}}\right)\right)\to \left(\left(⟨{x},{y}⟩{2}^{nd}\left(⟨“{C}{D}{E}”⟩{uncurry}_{F}{G}\right)⟨{z},{w}⟩\right):⟨{x},{y}⟩\mathrm{Hom}\left({C}{×}_{c}{D}\right)⟨{z},{w}⟩⟶{1}^{st}\left(⟨“{C}{D}{E}”⟩{uncurry}_{F}{G}\right)\left(⟨{x},{y}⟩\right)\mathrm{Hom}\left({E}\right){1}^{st}\left(⟨“{C}{D}{E}”⟩{uncurry}_{F}{G}\right)\left(⟨{z},{w}⟩\right)↔\left(⟨{x},{y}⟩{2}^{nd}\left(⟨“{C}{D}{E}”⟩{uncurry}_{F}{G}\right)⟨{z},{w}⟩\right):\left({x}\mathrm{Hom}\left({C}\right){z}\right)×\left({y}\mathrm{Hom}\left({D}\right){w}\right)⟶{1}^{st}\left(⟨“{C}{D}{E}”⟩{uncurry}_{F}{G}\right)\left(⟨{x},{y}⟩\right)\mathrm{Hom}\left({E}\right){1}^{st}\left(⟨“{C}{D}{E}”⟩{uncurry}_{F}{G}\right)\left(⟨{z},{w}⟩\right)\right)$
120 117 119 mpbid ${⊢}\left(\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{D}}\right)\right)\wedge \left({z}\in {\mathrm{Base}}_{{C}}\wedge {w}\in {\mathrm{Base}}_{{D}}\right)\right)\to \left(⟨{x},{y}⟩{2}^{nd}\left(⟨“{C}{D}{E}”⟩{uncurry}_{F}{G}\right)⟨{z},{w}⟩\right):\left({x}\mathrm{Hom}\left({C}\right){z}\right)×\left({y}\mathrm{Hom}\left({D}\right){w}\right)⟶{1}^{st}\left(⟨“{C}{D}{E}”⟩{uncurry}_{F}{G}\right)\left(⟨{x},{y}⟩\right)\mathrm{Hom}\left({E}\right){1}^{st}\left(⟨“{C}{D}{E}”⟩{uncurry}_{F}{G}\right)\left(⟨{z},{w}⟩\right)$
121 120 ffnd ${⊢}\left(\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{D}}\right)\right)\wedge \left({z}\in {\mathrm{Base}}_{{C}}\wedge {w}\in {\mathrm{Base}}_{{D}}\right)\right)\to \left(⟨{x},{y}⟩{2}^{nd}\left(⟨“{C}{D}{E}”⟩{uncurry}_{F}{G}\right)⟨{z},{w}⟩\right)Fn\left(\left({x}\mathrm{Hom}\left({C}\right){z}\right)×\left({y}\mathrm{Hom}\left({D}\right){w}\right)\right)$
122 26 81 115 84 87 91 funcf2 ${⊢}\left(\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{D}}\right)\right)\wedge \left({z}\in {\mathrm{Base}}_{{C}}\wedge {w}\in {\mathrm{Base}}_{{D}}\right)\right)\to \left(⟨{x},{y}⟩{2}^{nd}\left({F}\right)⟨{z},{w}⟩\right):⟨{x},{y}⟩\mathrm{Hom}\left({C}{×}_{c}{D}\right)⟨{z},{w}⟩⟶{1}^{st}\left({F}\right)\left(⟨{x},{y}⟩\right)\mathrm{Hom}\left({E}\right){1}^{st}\left({F}\right)\left(⟨{z},{w}⟩\right)$
123 118 feq2d ${⊢}\left(\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{D}}\right)\right)\wedge \left({z}\in {\mathrm{Base}}_{{C}}\wedge {w}\in {\mathrm{Base}}_{{D}}\right)\right)\to \left(\left(⟨{x},{y}⟩{2}^{nd}\left({F}\right)⟨{z},{w}⟩\right):⟨{x},{y}⟩\mathrm{Hom}\left({C}{×}_{c}{D}\right)⟨{z},{w}⟩⟶{1}^{st}\left({F}\right)\left(⟨{x},{y}⟩\right)\mathrm{Hom}\left({E}\right){1}^{st}\left({F}\right)\left(⟨{z},{w}⟩\right)↔\left(⟨{x},{y}⟩{2}^{nd}\left({F}\right)⟨{z},{w}⟩\right):\left({x}\mathrm{Hom}\left({C}\right){z}\right)×\left({y}\mathrm{Hom}\left({D}\right){w}\right)⟶{1}^{st}\left({F}\right)\left(⟨{x},{y}⟩\right)\mathrm{Hom}\left({E}\right){1}^{st}\left({F}\right)\left(⟨{z},{w}⟩\right)\right)$
124 122 123 mpbid ${⊢}\left(\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{D}}\right)\right)\wedge \left({z}\in {\mathrm{Base}}_{{C}}\wedge {w}\in {\mathrm{Base}}_{{D}}\right)\right)\to \left(⟨{x},{y}⟩{2}^{nd}\left({F}\right)⟨{z},{w}⟩\right):\left({x}\mathrm{Hom}\left({C}\right){z}\right)×\left({y}\mathrm{Hom}\left({D}\right){w}\right)⟶{1}^{st}\left({F}\right)\left(⟨{x},{y}⟩\right)\mathrm{Hom}\left({E}\right){1}^{st}\left({F}\right)\left(⟨{z},{w}⟩\right)$
125 124 ffnd ${⊢}\left(\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{D}}\right)\right)\wedge \left({z}\in {\mathrm{Base}}_{{C}}\wedge {w}\in {\mathrm{Base}}_{{D}}\right)\right)\to \left(⟨{x},{y}⟩{2}^{nd}\left({F}\right)⟨{z},{w}⟩\right)Fn\left(\left({x}\mathrm{Hom}\left({C}\right){z}\right)×\left({y}\mathrm{Hom}\left({D}\right){w}\right)\right)$
126 eqfnov2 ${⊢}\left(\left(⟨{x},{y}⟩{2}^{nd}\left(⟨“{C}{D}{E}”⟩{uncurry}_{F}{G}\right)⟨{z},{w}⟩\right)Fn\left(\left({x}\mathrm{Hom}\left({C}\right){z}\right)×\left({y}\mathrm{Hom}\left({D}\right){w}\right)\right)\wedge \left(⟨{x},{y}⟩{2}^{nd}\left({F}\right)⟨{z},{w}⟩\right)Fn\left(\left({x}\mathrm{Hom}\left({C}\right){z}\right)×\left({y}\mathrm{Hom}\left({D}\right){w}\right)\right)\right)\to \left(⟨{x},{y}⟩{2}^{nd}\left(⟨“{C}{D}{E}”⟩{uncurry}_{F}{G}\right)⟨{z},{w}⟩=⟨{x},{y}⟩{2}^{nd}\left({F}\right)⟨{z},{w}⟩↔\forall {f}\in \left({x}\mathrm{Hom}\left({C}\right){z}\right)\phantom{\rule{.4em}{0ex}}\forall {g}\in \left({y}\mathrm{Hom}\left({D}\right){w}\right)\phantom{\rule{.4em}{0ex}}{f}\left(⟨{x},{y}⟩{2}^{nd}\left(⟨“{C}{D}{E}”⟩{uncurry}_{F}{G}\right)⟨{z},{w}⟩\right){g}={f}\left(⟨{x},{y}⟩{2}^{nd}\left({F}\right)⟨{z},{w}⟩\right){g}\right)$
127 121 125 126 syl2anc ${⊢}\left(\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{D}}\right)\right)\wedge \left({z}\in {\mathrm{Base}}_{{C}}\wedge {w}\in {\mathrm{Base}}_{{D}}\right)\right)\to \left(⟨{x},{y}⟩{2}^{nd}\left(⟨“{C}{D}{E}”⟩{uncurry}_{F}{G}\right)⟨{z},{w}⟩=⟨{x},{y}⟩{2}^{nd}\left({F}\right)⟨{z},{w}⟩↔\forall {f}\in \left({x}\mathrm{Hom}\left({C}\right){z}\right)\phantom{\rule{.4em}{0ex}}\forall {g}\in \left({y}\mathrm{Hom}\left({D}\right){w}\right)\phantom{\rule{.4em}{0ex}}{f}\left(⟨{x},{y}⟩{2}^{nd}\left(⟨“{C}{D}{E}”⟩{uncurry}_{F}{G}\right)⟨{z},{w}⟩\right){g}={f}\left(⟨{x},{y}⟩{2}^{nd}\left({F}\right)⟨{z},{w}⟩\right){g}\right)$
128 114 127 mpbird ${⊢}\left(\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{D}}\right)\right)\wedge \left({z}\in {\mathrm{Base}}_{{C}}\wedge {w}\in {\mathrm{Base}}_{{D}}\right)\right)\to ⟨{x},{y}⟩{2}^{nd}\left(⟨“{C}{D}{E}”⟩{uncurry}_{F}{G}\right)⟨{z},{w}⟩=⟨{x},{y}⟩{2}^{nd}\left({F}\right)⟨{z},{w}⟩$
129 128 ralrimivva ${⊢}\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{D}}\right)\right)\to \forall {z}\in {\mathrm{Base}}_{{C}}\phantom{\rule{.4em}{0ex}}\forall {w}\in {\mathrm{Base}}_{{D}}\phantom{\rule{.4em}{0ex}}⟨{x},{y}⟩{2}^{nd}\left(⟨“{C}{D}{E}”⟩{uncurry}_{F}{G}\right)⟨{z},{w}⟩=⟨{x},{y}⟩{2}^{nd}\left({F}\right)⟨{z},{w}⟩$
130 129 ralrimivva ${⊢}{\phi }\to \forall {x}\in {\mathrm{Base}}_{{C}}\phantom{\rule{.4em}{0ex}}\forall {y}\in {\mathrm{Base}}_{{D}}\phantom{\rule{.4em}{0ex}}\forall {z}\in {\mathrm{Base}}_{{C}}\phantom{\rule{.4em}{0ex}}\forall {w}\in {\mathrm{Base}}_{{D}}\phantom{\rule{.4em}{0ex}}⟨{x},{y}⟩{2}^{nd}\left(⟨“{C}{D}{E}”⟩{uncurry}_{F}{G}\right)⟨{z},{w}⟩=⟨{x},{y}⟩{2}^{nd}\left({F}\right)⟨{z},{w}⟩$
131 oveq2 ${⊢}{v}=⟨{z},{w}⟩\to {u}{2}^{nd}\left(⟨“{C}{D}{E}”⟩{uncurry}_{F}{G}\right){v}={u}{2}^{nd}\left(⟨“{C}{D}{E}”⟩{uncurry}_{F}{G}\right)⟨{z},{w}⟩$
132 oveq2 ${⊢}{v}=⟨{z},{w}⟩\to {u}{2}^{nd}\left({F}\right){v}={u}{2}^{nd}\left({F}\right)⟨{z},{w}⟩$
133 131 132 eqeq12d ${⊢}{v}=⟨{z},{w}⟩\to \left({u}{2}^{nd}\left(⟨“{C}{D}{E}”⟩{uncurry}_{F}{G}\right){v}={u}{2}^{nd}\left({F}\right){v}↔{u}{2}^{nd}\left(⟨“{C}{D}{E}”⟩{uncurry}_{F}{G}\right)⟨{z},{w}⟩={u}{2}^{nd}\left({F}\right)⟨{z},{w}⟩\right)$
134 133 ralxp ${⊢}\forall {v}\in \left({\mathrm{Base}}_{{C}}×{\mathrm{Base}}_{{D}}\right)\phantom{\rule{.4em}{0ex}}{u}{2}^{nd}\left(⟨“{C}{D}{E}”⟩{uncurry}_{F}{G}\right){v}={u}{2}^{nd}\left({F}\right){v}↔\forall {z}\in {\mathrm{Base}}_{{C}}\phantom{\rule{.4em}{0ex}}\forall {w}\in {\mathrm{Base}}_{{D}}\phantom{\rule{.4em}{0ex}}{u}{2}^{nd}\left(⟨“{C}{D}{E}”⟩{uncurry}_{F}{G}\right)⟨{z},{w}⟩={u}{2}^{nd}\left({F}\right)⟨{z},{w}⟩$
135 oveq1 ${⊢}{u}=⟨{x},{y}⟩\to {u}{2}^{nd}\left(⟨“{C}{D}{E}”⟩{uncurry}_{F}{G}\right)⟨{z},{w}⟩=⟨{x},{y}⟩{2}^{nd}\left(⟨“{C}{D}{E}”⟩{uncurry}_{F}{G}\right)⟨{z},{w}⟩$
136 oveq1 ${⊢}{u}=⟨{x},{y}⟩\to {u}{2}^{nd}\left({F}\right)⟨{z},{w}⟩=⟨{x},{y}⟩{2}^{nd}\left({F}\right)⟨{z},{w}⟩$
137 135 136 eqeq12d ${⊢}{u}=⟨{x},{y}⟩\to \left({u}{2}^{nd}\left(⟨“{C}{D}{E}”⟩{uncurry}_{F}{G}\right)⟨{z},{w}⟩={u}{2}^{nd}\left({F}\right)⟨{z},{w}⟩↔⟨{x},{y}⟩{2}^{nd}\left(⟨“{C}{D}{E}”⟩{uncurry}_{F}{G}\right)⟨{z},{w}⟩=⟨{x},{y}⟩{2}^{nd}\left({F}\right)⟨{z},{w}⟩\right)$
138 137 2ralbidv ${⊢}{u}=⟨{x},{y}⟩\to \left(\forall {z}\in {\mathrm{Base}}_{{C}}\phantom{\rule{.4em}{0ex}}\forall {w}\in {\mathrm{Base}}_{{D}}\phantom{\rule{.4em}{0ex}}{u}{2}^{nd}\left(⟨“{C}{D}{E}”⟩{uncurry}_{F}{G}\right)⟨{z},{w}⟩={u}{2}^{nd}\left({F}\right)⟨{z},{w}⟩↔\forall {z}\in {\mathrm{Base}}_{{C}}\phantom{\rule{.4em}{0ex}}\forall {w}\in {\mathrm{Base}}_{{D}}\phantom{\rule{.4em}{0ex}}⟨{x},{y}⟩{2}^{nd}\left(⟨“{C}{D}{E}”⟩{uncurry}_{F}{G}\right)⟨{z},{w}⟩=⟨{x},{y}⟩{2}^{nd}\left({F}\right)⟨{z},{w}⟩\right)$
139 134 138 syl5bb ${⊢}{u}=⟨{x},{y}⟩\to \left(\forall {v}\in \left({\mathrm{Base}}_{{C}}×{\mathrm{Base}}_{{D}}\right)\phantom{\rule{.4em}{0ex}}{u}{2}^{nd}\left(⟨“{C}{D}{E}”⟩{uncurry}_{F}{G}\right){v}={u}{2}^{nd}\left({F}\right){v}↔\forall {z}\in {\mathrm{Base}}_{{C}}\phantom{\rule{.4em}{0ex}}\forall {w}\in {\mathrm{Base}}_{{D}}\phantom{\rule{.4em}{0ex}}⟨{x},{y}⟩{2}^{nd}\left(⟨“{C}{D}{E}”⟩{uncurry}_{F}{G}\right)⟨{z},{w}⟩=⟨{x},{y}⟩{2}^{nd}\left({F}\right)⟨{z},{w}⟩\right)$
140 139 ralxp ${⊢}\forall {u}\in \left({\mathrm{Base}}_{{C}}×{\mathrm{Base}}_{{D}}\right)\phantom{\rule{.4em}{0ex}}\forall {v}\in \left({\mathrm{Base}}_{{C}}×{\mathrm{Base}}_{{D}}\right)\phantom{\rule{.4em}{0ex}}{u}{2}^{nd}\left(⟨“{C}{D}{E}”⟩{uncurry}_{F}{G}\right){v}={u}{2}^{nd}\left({F}\right){v}↔\forall {x}\in {\mathrm{Base}}_{{C}}\phantom{\rule{.4em}{0ex}}\forall {y}\in {\mathrm{Base}}_{{D}}\phantom{\rule{.4em}{0ex}}\forall {z}\in {\mathrm{Base}}_{{C}}\phantom{\rule{.4em}{0ex}}\forall {w}\in {\mathrm{Base}}_{{D}}\phantom{\rule{.4em}{0ex}}⟨{x},{y}⟩{2}^{nd}\left(⟨“{C}{D}{E}”⟩{uncurry}_{F}{G}\right)⟨{z},{w}⟩=⟨{x},{y}⟩{2}^{nd}\left({F}\right)⟨{z},{w}⟩$
141 130 140 sylibr ${⊢}{\phi }\to \forall {u}\in \left({\mathrm{Base}}_{{C}}×{\mathrm{Base}}_{{D}}\right)\phantom{\rule{.4em}{0ex}}\forall {v}\in \left({\mathrm{Base}}_{{C}}×{\mathrm{Base}}_{{D}}\right)\phantom{\rule{.4em}{0ex}}{u}{2}^{nd}\left(⟨“{C}{D}{E}”⟩{uncurry}_{F}{G}\right){v}={u}{2}^{nd}\left({F}\right){v}$
142 26 31 funcfn2 ${⊢}{\phi }\to {2}^{nd}\left(⟨“{C}{D}{E}”⟩{uncurry}_{F}{G}\right)Fn\left(\left({\mathrm{Base}}_{{C}}×{\mathrm{Base}}_{{D}}\right)×\left({\mathrm{Base}}_{{C}}×{\mathrm{Base}}_{{D}}\right)\right)$
143 26 35 funcfn2 ${⊢}{\phi }\to {2}^{nd}\left({F}\right)Fn\left(\left({\mathrm{Base}}_{{C}}×{\mathrm{Base}}_{{D}}\right)×\left({\mathrm{Base}}_{{C}}×{\mathrm{Base}}_{{D}}\right)\right)$
144 eqfnov2 ${⊢}\left({2}^{nd}\left(⟨“{C}{D}{E}”⟩{uncurry}_{F}{G}\right)Fn\left(\left({\mathrm{Base}}_{{C}}×{\mathrm{Base}}_{{D}}\right)×\left({\mathrm{Base}}_{{C}}×{\mathrm{Base}}_{{D}}\right)\right)\wedge {2}^{nd}\left({F}\right)Fn\left(\left({\mathrm{Base}}_{{C}}×{\mathrm{Base}}_{{D}}\right)×\left({\mathrm{Base}}_{{C}}×{\mathrm{Base}}_{{D}}\right)\right)\right)\to \left({2}^{nd}\left(⟨“{C}{D}{E}”⟩{uncurry}_{F}{G}\right)={2}^{nd}\left({F}\right)↔\forall {u}\in \left({\mathrm{Base}}_{{C}}×{\mathrm{Base}}_{{D}}\right)\phantom{\rule{.4em}{0ex}}\forall {v}\in \left({\mathrm{Base}}_{{C}}×{\mathrm{Base}}_{{D}}\right)\phantom{\rule{.4em}{0ex}}{u}{2}^{nd}\left(⟨“{C}{D}{E}”⟩{uncurry}_{F}{G}\right){v}={u}{2}^{nd}\left({F}\right){v}\right)$
145 142 143 144 syl2anc ${⊢}{\phi }\to \left({2}^{nd}\left(⟨“{C}{D}{E}”⟩{uncurry}_{F}{G}\right)={2}^{nd}\left({F}\right)↔\forall {u}\in \left({\mathrm{Base}}_{{C}}×{\mathrm{Base}}_{{D}}\right)\phantom{\rule{.4em}{0ex}}\forall {v}\in \left({\mathrm{Base}}_{{C}}×{\mathrm{Base}}_{{D}}\right)\phantom{\rule{.4em}{0ex}}{u}{2}^{nd}\left(⟨“{C}{D}{E}”⟩{uncurry}_{F}{G}\right){v}={u}{2}^{nd}\left({F}\right){v}\right)$
146 141 145 mpbird ${⊢}{\phi }\to {2}^{nd}\left(⟨“{C}{D}{E}”⟩{uncurry}_{F}{G}\right)={2}^{nd}\left({F}\right)$
147 40 146 opeq12d ${⊢}{\phi }\to ⟨{1}^{st}\left(⟨“{C}{D}{E}”⟩{uncurry}_{F}{G}\right),{2}^{nd}\left(⟨“{C}{D}{E}”⟩{uncurry}_{F}{G}\right)⟩=⟨{1}^{st}\left({F}\right),{2}^{nd}\left({F}\right)⟩$
148 1st2nd ${⊢}\left(\mathrm{Rel}\left(\left({C}{×}_{c}{D}\right)\mathrm{Func}{E}\right)\wedge ⟨“{C}{D}{E}”⟩{uncurry}_{F}{G}\in \left(\left({C}{×}_{c}{D}\right)\mathrm{Func}{E}\right)\right)\to ⟨“{C}{D}{E}”⟩{uncurry}_{F}{G}=⟨{1}^{st}\left(⟨“{C}{D}{E}”⟩{uncurry}_{F}{G}\right),{2}^{nd}\left(⟨“{C}{D}{E}”⟩{uncurry}_{F}{G}\right)⟩$
149 28 29 148 sylancr ${⊢}{\phi }\to ⟨“{C}{D}{E}”⟩{uncurry}_{F}{G}=⟨{1}^{st}\left(⟨“{C}{D}{E}”⟩{uncurry}_{F}{G}\right),{2}^{nd}\left(⟨“{C}{D}{E}”⟩{uncurry}_{F}{G}\right)⟩$
150 1st2nd ${⊢}\left(\mathrm{Rel}\left(\left({C}{×}_{c}{D}\right)\mathrm{Func}{E}\right)\wedge {F}\in \left(\left({C}{×}_{c}{D}\right)\mathrm{Func}{E}\right)\right)\to {F}=⟨{1}^{st}\left({F}\right),{2}^{nd}\left({F}\right)⟩$
151 28 4 150 sylancr ${⊢}{\phi }\to {F}=⟨{1}^{st}\left({F}\right),{2}^{nd}\left({F}\right)⟩$
152 147 149 151 3eqtr4d ${⊢}{\phi }\to ⟨“{C}{D}{E}”⟩{uncurry}_{F}{G}={F}$