# Metamath Proof Explorer

## Theorem uncf2

Description: Value of the uncurry functor on a morphism. (Contributed by Mario Carneiro, 13-Jan-2017)

Ref Expression
Hypotheses uncfval.g ${⊢}{F}=⟨“{C}{D}{E}”⟩{uncurry}_{F}{G}$
uncfval.c ${⊢}{\phi }\to {D}\in \mathrm{Cat}$
uncfval.d ${⊢}{\phi }\to {E}\in \mathrm{Cat}$
uncfval.f ${⊢}{\phi }\to {G}\in \left({C}\mathrm{Func}\left({D}\mathrm{FuncCat}{E}\right)\right)$
uncf1.a ${⊢}{A}={\mathrm{Base}}_{{C}}$
uncf1.b ${⊢}{B}={\mathrm{Base}}_{{D}}$
uncf1.x ${⊢}{\phi }\to {X}\in {A}$
uncf1.y ${⊢}{\phi }\to {Y}\in {B}$
uncf2.h ${⊢}{H}=\mathrm{Hom}\left({C}\right)$
uncf2.j ${⊢}{J}=\mathrm{Hom}\left({D}\right)$
uncf2.z ${⊢}{\phi }\to {Z}\in {A}$
uncf2.w ${⊢}{\phi }\to {W}\in {B}$
uncf2.r ${⊢}{\phi }\to {R}\in \left({X}{H}{Z}\right)$
uncf2.s ${⊢}{\phi }\to {S}\in \left({Y}{J}{W}\right)$
Assertion uncf2 ${⊢}{\phi }\to {R}\left(⟨{X},{Y}⟩{2}^{nd}\left({F}\right)⟨{Z},{W}⟩\right){S}=\left({X}{2}^{nd}\left({G}\right){Z}\right)\left({R}\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({S}\right)$

### Proof

Step Hyp Ref Expression
1 uncfval.g ${⊢}{F}=⟨“{C}{D}{E}”⟩{uncurry}_{F}{G}$
2 uncfval.c ${⊢}{\phi }\to {D}\in \mathrm{Cat}$
3 uncfval.d ${⊢}{\phi }\to {E}\in \mathrm{Cat}$
4 uncfval.f ${⊢}{\phi }\to {G}\in \left({C}\mathrm{Func}\left({D}\mathrm{FuncCat}{E}\right)\right)$
5 uncf1.a ${⊢}{A}={\mathrm{Base}}_{{C}}$
6 uncf1.b ${⊢}{B}={\mathrm{Base}}_{{D}}$
7 uncf1.x ${⊢}{\phi }\to {X}\in {A}$
8 uncf1.y ${⊢}{\phi }\to {Y}\in {B}$
9 uncf2.h ${⊢}{H}=\mathrm{Hom}\left({C}\right)$
10 uncf2.j ${⊢}{J}=\mathrm{Hom}\left({D}\right)$
11 uncf2.z ${⊢}{\phi }\to {Z}\in {A}$
12 uncf2.w ${⊢}{\phi }\to {W}\in {B}$
13 uncf2.r ${⊢}{\phi }\to {R}\in \left({X}{H}{Z}\right)$
14 uncf2.s ${⊢}{\phi }\to {S}\in \left({Y}{J}{W}\right)$
15 1 2 3 4 uncfval ${⊢}{\phi }\to {F}=\left({D}{eval}_{F}{E}\right){\circ }_{\mathrm{func}}\left(\left({G}{\circ }_{\mathrm{func}}\left({C}{{1}^{st}}_{F}{D}\right)\right){⟨,⟩}_{F}\left({C}{{2}^{nd}}_{F}{D}\right)\right)$
16 15 fveq2d ${⊢}{\phi }\to {2}^{nd}\left({F}\right)={2}^{nd}\left(\left({D}{eval}_{F}{E}\right){\circ }_{\mathrm{func}}\left(\left({G}{\circ }_{\mathrm{func}}\left({C}{{1}^{st}}_{F}{D}\right)\right){⟨,⟩}_{F}\left({C}{{2}^{nd}}_{F}{D}\right)\right)\right)$
17 16 oveqd ${⊢}{\phi }\to ⟨{X},{Y}⟩{2}^{nd}\left({F}\right)⟨{Z},{W}⟩=⟨{X},{Y}⟩{2}^{nd}\left(\left({D}{eval}_{F}{E}\right){\circ }_{\mathrm{func}}\left(\left({G}{\circ }_{\mathrm{func}}\left({C}{{1}^{st}}_{F}{D}\right)\right){⟨,⟩}_{F}\left({C}{{2}^{nd}}_{F}{D}\right)\right)\right)⟨{Z},{W}⟩$
18 17 oveqd ${⊢}{\phi }\to {R}\left(⟨{X},{Y}⟩{2}^{nd}\left({F}\right)⟨{Z},{W}⟩\right){S}={R}\left(⟨{X},{Y}⟩{2}^{nd}\left(\left({D}{eval}_{F}{E}\right){\circ }_{\mathrm{func}}\left(\left({G}{\circ }_{\mathrm{func}}\left({C}{{1}^{st}}_{F}{D}\right)\right){⟨,⟩}_{F}\left({C}{{2}^{nd}}_{F}{D}\right)\right)\right)⟨{Z},{W}⟩\right){S}$
19 df-ov ${⊢}{R}\left(⟨{X},{Y}⟩{2}^{nd}\left(\left({D}{eval}_{F}{E}\right){\circ }_{\mathrm{func}}\left(\left({G}{\circ }_{\mathrm{func}}\left({C}{{1}^{st}}_{F}{D}\right)\right){⟨,⟩}_{F}\left({C}{{2}^{nd}}_{F}{D}\right)\right)\right)⟨{Z},{W}⟩\right){S}=\left(⟨{X},{Y}⟩{2}^{nd}\left(\left({D}{eval}_{F}{E}\right){\circ }_{\mathrm{func}}\left(\left({G}{\circ }_{\mathrm{func}}\left({C}{{1}^{st}}_{F}{D}\right)\right){⟨,⟩}_{F}\left({C}{{2}^{nd}}_{F}{D}\right)\right)\right)⟨{Z},{W}⟩\right)\left(⟨{R},{S}⟩\right)$
20 eqid ${⊢}{C}{×}_{c}{D}={C}{×}_{c}{D}$
21 20 5 6 xpcbas ${⊢}{A}×{B}={\mathrm{Base}}_{\left({C}{×}_{c}{D}\right)}$
22 eqid ${⊢}\left({G}{\circ }_{\mathrm{func}}\left({C}{{1}^{st}}_{F}{D}\right)\right){⟨,⟩}_{F}\left({C}{{2}^{nd}}_{F}{D}\right)=\left({G}{\circ }_{\mathrm{func}}\left({C}{{1}^{st}}_{F}{D}\right)\right){⟨,⟩}_{F}\left({C}{{2}^{nd}}_{F}{D}\right)$
23 eqid ${⊢}\left({D}\mathrm{FuncCat}{E}\right){×}_{c}{D}=\left({D}\mathrm{FuncCat}{E}\right){×}_{c}{D}$
24 funcrcl ${⊢}{G}\in \left({C}\mathrm{Func}\left({D}\mathrm{FuncCat}{E}\right)\right)\to \left({C}\in \mathrm{Cat}\wedge {D}\mathrm{FuncCat}{E}\in \mathrm{Cat}\right)$
25 4 24 syl ${⊢}{\phi }\to \left({C}\in \mathrm{Cat}\wedge {D}\mathrm{FuncCat}{E}\in \mathrm{Cat}\right)$
26 25 simpld ${⊢}{\phi }\to {C}\in \mathrm{Cat}$
27 eqid ${⊢}{C}{{1}^{st}}_{F}{D}={C}{{1}^{st}}_{F}{D}$
28 20 26 2 27 1stfcl ${⊢}{\phi }\to {C}{{1}^{st}}_{F}{D}\in \left(\left({C}{×}_{c}{D}\right)\mathrm{Func}{C}\right)$
29 28 4 cofucl ${⊢}{\phi }\to {G}{\circ }_{\mathrm{func}}\left({C}{{1}^{st}}_{F}{D}\right)\in \left(\left({C}{×}_{c}{D}\right)\mathrm{Func}\left({D}\mathrm{FuncCat}{E}\right)\right)$
30 eqid ${⊢}{C}{{2}^{nd}}_{F}{D}={C}{{2}^{nd}}_{F}{D}$
31 20 26 2 30 2ndfcl ${⊢}{\phi }\to {C}{{2}^{nd}}_{F}{D}\in \left(\left({C}{×}_{c}{D}\right)\mathrm{Func}{D}\right)$
32 22 23 29 31 prfcl ${⊢}{\phi }\to \left({G}{\circ }_{\mathrm{func}}\left({C}{{1}^{st}}_{F}{D}\right)\right){⟨,⟩}_{F}\left({C}{{2}^{nd}}_{F}{D}\right)\in \left(\left({C}{×}_{c}{D}\right)\mathrm{Func}\left(\left({D}\mathrm{FuncCat}{E}\right){×}_{c}{D}\right)\right)$
33 eqid ${⊢}{D}{eval}_{F}{E}={D}{eval}_{F}{E}$
34 eqid ${⊢}{D}\mathrm{FuncCat}{E}={D}\mathrm{FuncCat}{E}$
35 33 34 2 3 evlfcl ${⊢}{\phi }\to {D}{eval}_{F}{E}\in \left(\left(\left({D}\mathrm{FuncCat}{E}\right){×}_{c}{D}\right)\mathrm{Func}{E}\right)$
36 7 8 opelxpd ${⊢}{\phi }\to ⟨{X},{Y}⟩\in \left({A}×{B}\right)$
37 11 12 opelxpd ${⊢}{\phi }\to ⟨{Z},{W}⟩\in \left({A}×{B}\right)$
38 eqid ${⊢}\mathrm{Hom}\left({C}{×}_{c}{D}\right)=\mathrm{Hom}\left({C}{×}_{c}{D}\right)$
39 13 14 opelxpd ${⊢}{\phi }\to ⟨{R},{S}⟩\in \left(\left({X}{H}{Z}\right)×\left({Y}{J}{W}\right)\right)$
40 20 5 6 9 10 7 8 11 12 38 xpchom2 ${⊢}{\phi }\to ⟨{X},{Y}⟩\mathrm{Hom}\left({C}{×}_{c}{D}\right)⟨{Z},{W}⟩=\left({X}{H}{Z}\right)×\left({Y}{J}{W}\right)$
41 39 40 eleqtrrd ${⊢}{\phi }\to ⟨{R},{S}⟩\in \left(⟨{X},{Y}⟩\mathrm{Hom}\left({C}{×}_{c}{D}\right)⟨{Z},{W}⟩\right)$
42 21 32 35 36 37 38 41 cofu2 ${⊢}{\phi }\to \left(⟨{X},{Y}⟩{2}^{nd}\left(\left({D}{eval}_{F}{E}\right){\circ }_{\mathrm{func}}\left(\left({G}{\circ }_{\mathrm{func}}\left({C}{{1}^{st}}_{F}{D}\right)\right){⟨,⟩}_{F}\left({C}{{2}^{nd}}_{F}{D}\right)\right)\right)⟨{Z},{W}⟩\right)\left(⟨{R},{S}⟩\right)=\left({1}^{st}\left(\left({G}{\circ }_{\mathrm{func}}\left({C}{{1}^{st}}_{F}{D}\right)\right){⟨,⟩}_{F}\left({C}{{2}^{nd}}_{F}{D}\right)\right)\left(⟨{X},{Y}⟩\right){2}^{nd}\left({D}{eval}_{F}{E}\right){1}^{st}\left(\left({G}{\circ }_{\mathrm{func}}\left({C}{{1}^{st}}_{F}{D}\right)\right){⟨,⟩}_{F}\left({C}{{2}^{nd}}_{F}{D}\right)\right)\left(⟨{Z},{W}⟩\right)\right)\left(\left(⟨{X},{Y}⟩{2}^{nd}\left(\left({G}{\circ }_{\mathrm{func}}\left({C}{{1}^{st}}_{F}{D}\right)\right){⟨,⟩}_{F}\left({C}{{2}^{nd}}_{F}{D}\right)\right)⟨{Z},{W}⟩\right)\left(⟨{R},{S}⟩\right)\right)$
43 19 42 syl5eq ${⊢}{\phi }\to {R}\left(⟨{X},{Y}⟩{2}^{nd}\left(\left({D}{eval}_{F}{E}\right){\circ }_{\mathrm{func}}\left(\left({G}{\circ }_{\mathrm{func}}\left({C}{{1}^{st}}_{F}{D}\right)\right){⟨,⟩}_{F}\left({C}{{2}^{nd}}_{F}{D}\right)\right)\right)⟨{Z},{W}⟩\right){S}=\left({1}^{st}\left(\left({G}{\circ }_{\mathrm{func}}\left({C}{{1}^{st}}_{F}{D}\right)\right){⟨,⟩}_{F}\left({C}{{2}^{nd}}_{F}{D}\right)\right)\left(⟨{X},{Y}⟩\right){2}^{nd}\left({D}{eval}_{F}{E}\right){1}^{st}\left(\left({G}{\circ }_{\mathrm{func}}\left({C}{{1}^{st}}_{F}{D}\right)\right){⟨,⟩}_{F}\left({C}{{2}^{nd}}_{F}{D}\right)\right)\left(⟨{Z},{W}⟩\right)\right)\left(\left(⟨{X},{Y}⟩{2}^{nd}\left(\left({G}{\circ }_{\mathrm{func}}\left({C}{{1}^{st}}_{F}{D}\right)\right){⟨,⟩}_{F}\left({C}{{2}^{nd}}_{F}{D}\right)\right)⟨{Z},{W}⟩\right)\left(⟨{R},{S}⟩\right)\right)$
44 18 43 eqtrd ${⊢}{\phi }\to {R}\left(⟨{X},{Y}⟩{2}^{nd}\left({F}\right)⟨{Z},{W}⟩\right){S}=\left({1}^{st}\left(\left({G}{\circ }_{\mathrm{func}}\left({C}{{1}^{st}}_{F}{D}\right)\right){⟨,⟩}_{F}\left({C}{{2}^{nd}}_{F}{D}\right)\right)\left(⟨{X},{Y}⟩\right){2}^{nd}\left({D}{eval}_{F}{E}\right){1}^{st}\left(\left({G}{\circ }_{\mathrm{func}}\left({C}{{1}^{st}}_{F}{D}\right)\right){⟨,⟩}_{F}\left({C}{{2}^{nd}}_{F}{D}\right)\right)\left(⟨{Z},{W}⟩\right)\right)\left(\left(⟨{X},{Y}⟩{2}^{nd}\left(\left({G}{\circ }_{\mathrm{func}}\left({C}{{1}^{st}}_{F}{D}\right)\right){⟨,⟩}_{F}\left({C}{{2}^{nd}}_{F}{D}\right)\right)⟨{Z},{W}⟩\right)\left(⟨{R},{S}⟩\right)\right)$
45 22 21 38 29 31 36 prf1 ${⊢}{\phi }\to {1}^{st}\left(\left({G}{\circ }_{\mathrm{func}}\left({C}{{1}^{st}}_{F}{D}\right)\right){⟨,⟩}_{F}\left({C}{{2}^{nd}}_{F}{D}\right)\right)\left(⟨{X},{Y}⟩\right)=⟨{1}^{st}\left({G}{\circ }_{\mathrm{func}}\left({C}{{1}^{st}}_{F}{D}\right)\right)\left(⟨{X},{Y}⟩\right),{1}^{st}\left({C}{{2}^{nd}}_{F}{D}\right)\left(⟨{X},{Y}⟩\right)⟩$
46 21 28 4 36 cofu1 ${⊢}{\phi }\to {1}^{st}\left({G}{\circ }_{\mathrm{func}}\left({C}{{1}^{st}}_{F}{D}\right)\right)\left(⟨{X},{Y}⟩\right)={1}^{st}\left({G}\right)\left({1}^{st}\left({C}{{1}^{st}}_{F}{D}\right)\left(⟨{X},{Y}⟩\right)\right)$
47 20 21 38 26 2 27 36 1stf1 ${⊢}{\phi }\to {1}^{st}\left({C}{{1}^{st}}_{F}{D}\right)\left(⟨{X},{Y}⟩\right)={1}^{st}\left(⟨{X},{Y}⟩\right)$
48 op1stg ${⊢}\left({X}\in {A}\wedge {Y}\in {B}\right)\to {1}^{st}\left(⟨{X},{Y}⟩\right)={X}$
49 7 8 48 syl2anc ${⊢}{\phi }\to {1}^{st}\left(⟨{X},{Y}⟩\right)={X}$
50 47 49 eqtrd ${⊢}{\phi }\to {1}^{st}\left({C}{{1}^{st}}_{F}{D}\right)\left(⟨{X},{Y}⟩\right)={X}$
51 50 fveq2d ${⊢}{\phi }\to {1}^{st}\left({G}\right)\left({1}^{st}\left({C}{{1}^{st}}_{F}{D}\right)\left(⟨{X},{Y}⟩\right)\right)={1}^{st}\left({G}\right)\left({X}\right)$
52 46 51 eqtrd ${⊢}{\phi }\to {1}^{st}\left({G}{\circ }_{\mathrm{func}}\left({C}{{1}^{st}}_{F}{D}\right)\right)\left(⟨{X},{Y}⟩\right)={1}^{st}\left({G}\right)\left({X}\right)$
53 20 21 38 26 2 30 36 2ndf1 ${⊢}{\phi }\to {1}^{st}\left({C}{{2}^{nd}}_{F}{D}\right)\left(⟨{X},{Y}⟩\right)={2}^{nd}\left(⟨{X},{Y}⟩\right)$
54 op2ndg ${⊢}\left({X}\in {A}\wedge {Y}\in {B}\right)\to {2}^{nd}\left(⟨{X},{Y}⟩\right)={Y}$
55 7 8 54 syl2anc ${⊢}{\phi }\to {2}^{nd}\left(⟨{X},{Y}⟩\right)={Y}$
56 53 55 eqtrd ${⊢}{\phi }\to {1}^{st}\left({C}{{2}^{nd}}_{F}{D}\right)\left(⟨{X},{Y}⟩\right)={Y}$
57 52 56 opeq12d ${⊢}{\phi }\to ⟨{1}^{st}\left({G}{\circ }_{\mathrm{func}}\left({C}{{1}^{st}}_{F}{D}\right)\right)\left(⟨{X},{Y}⟩\right),{1}^{st}\left({C}{{2}^{nd}}_{F}{D}\right)\left(⟨{X},{Y}⟩\right)⟩=⟨{1}^{st}\left({G}\right)\left({X}\right),{Y}⟩$
58 45 57 eqtrd ${⊢}{\phi }\to {1}^{st}\left(\left({G}{\circ }_{\mathrm{func}}\left({C}{{1}^{st}}_{F}{D}\right)\right){⟨,⟩}_{F}\left({C}{{2}^{nd}}_{F}{D}\right)\right)\left(⟨{X},{Y}⟩\right)=⟨{1}^{st}\left({G}\right)\left({X}\right),{Y}⟩$
59 22 21 38 29 31 37 prf1 ${⊢}{\phi }\to {1}^{st}\left(\left({G}{\circ }_{\mathrm{func}}\left({C}{{1}^{st}}_{F}{D}\right)\right){⟨,⟩}_{F}\left({C}{{2}^{nd}}_{F}{D}\right)\right)\left(⟨{Z},{W}⟩\right)=⟨{1}^{st}\left({G}{\circ }_{\mathrm{func}}\left({C}{{1}^{st}}_{F}{D}\right)\right)\left(⟨{Z},{W}⟩\right),{1}^{st}\left({C}{{2}^{nd}}_{F}{D}\right)\left(⟨{Z},{W}⟩\right)⟩$
60 21 28 4 37 cofu1 ${⊢}{\phi }\to {1}^{st}\left({G}{\circ }_{\mathrm{func}}\left({C}{{1}^{st}}_{F}{D}\right)\right)\left(⟨{Z},{W}⟩\right)={1}^{st}\left({G}\right)\left({1}^{st}\left({C}{{1}^{st}}_{F}{D}\right)\left(⟨{Z},{W}⟩\right)\right)$
61 20 21 38 26 2 27 37 1stf1 ${⊢}{\phi }\to {1}^{st}\left({C}{{1}^{st}}_{F}{D}\right)\left(⟨{Z},{W}⟩\right)={1}^{st}\left(⟨{Z},{W}⟩\right)$
62 op1stg ${⊢}\left({Z}\in {A}\wedge {W}\in {B}\right)\to {1}^{st}\left(⟨{Z},{W}⟩\right)={Z}$
63 11 12 62 syl2anc ${⊢}{\phi }\to {1}^{st}\left(⟨{Z},{W}⟩\right)={Z}$
64 61 63 eqtrd ${⊢}{\phi }\to {1}^{st}\left({C}{{1}^{st}}_{F}{D}\right)\left(⟨{Z},{W}⟩\right)={Z}$
65 64 fveq2d ${⊢}{\phi }\to {1}^{st}\left({G}\right)\left({1}^{st}\left({C}{{1}^{st}}_{F}{D}\right)\left(⟨{Z},{W}⟩\right)\right)={1}^{st}\left({G}\right)\left({Z}\right)$
66 60 65 eqtrd ${⊢}{\phi }\to {1}^{st}\left({G}{\circ }_{\mathrm{func}}\left({C}{{1}^{st}}_{F}{D}\right)\right)\left(⟨{Z},{W}⟩\right)={1}^{st}\left({G}\right)\left({Z}\right)$
67 20 21 38 26 2 30 37 2ndf1 ${⊢}{\phi }\to {1}^{st}\left({C}{{2}^{nd}}_{F}{D}\right)\left(⟨{Z},{W}⟩\right)={2}^{nd}\left(⟨{Z},{W}⟩\right)$
68 op2ndg ${⊢}\left({Z}\in {A}\wedge {W}\in {B}\right)\to {2}^{nd}\left(⟨{Z},{W}⟩\right)={W}$
69 11 12 68 syl2anc ${⊢}{\phi }\to {2}^{nd}\left(⟨{Z},{W}⟩\right)={W}$
70 67 69 eqtrd ${⊢}{\phi }\to {1}^{st}\left({C}{{2}^{nd}}_{F}{D}\right)\left(⟨{Z},{W}⟩\right)={W}$
71 66 70 opeq12d ${⊢}{\phi }\to ⟨{1}^{st}\left({G}{\circ }_{\mathrm{func}}\left({C}{{1}^{st}}_{F}{D}\right)\right)\left(⟨{Z},{W}⟩\right),{1}^{st}\left({C}{{2}^{nd}}_{F}{D}\right)\left(⟨{Z},{W}⟩\right)⟩=⟨{1}^{st}\left({G}\right)\left({Z}\right),{W}⟩$
72 59 71 eqtrd ${⊢}{\phi }\to {1}^{st}\left(\left({G}{\circ }_{\mathrm{func}}\left({C}{{1}^{st}}_{F}{D}\right)\right){⟨,⟩}_{F}\left({C}{{2}^{nd}}_{F}{D}\right)\right)\left(⟨{Z},{W}⟩\right)=⟨{1}^{st}\left({G}\right)\left({Z}\right),{W}⟩$
73 58 72 oveq12d ${⊢}{\phi }\to {1}^{st}\left(\left({G}{\circ }_{\mathrm{func}}\left({C}{{1}^{st}}_{F}{D}\right)\right){⟨,⟩}_{F}\left({C}{{2}^{nd}}_{F}{D}\right)\right)\left(⟨{X},{Y}⟩\right){2}^{nd}\left({D}{eval}_{F}{E}\right){1}^{st}\left(\left({G}{\circ }_{\mathrm{func}}\left({C}{{1}^{st}}_{F}{D}\right)\right){⟨,⟩}_{F}\left({C}{{2}^{nd}}_{F}{D}\right)\right)\left(⟨{Z},{W}⟩\right)=⟨{1}^{st}\left({G}\right)\left({X}\right),{Y}⟩{2}^{nd}\left({D}{eval}_{F}{E}\right)⟨{1}^{st}\left({G}\right)\left({Z}\right),{W}⟩$
74 22 21 38 29 31 36 37 41 prf2 ${⊢}{\phi }\to \left(⟨{X},{Y}⟩{2}^{nd}\left(\left({G}{\circ }_{\mathrm{func}}\left({C}{{1}^{st}}_{F}{D}\right)\right){⟨,⟩}_{F}\left({C}{{2}^{nd}}_{F}{D}\right)\right)⟨{Z},{W}⟩\right)\left(⟨{R},{S}⟩\right)=⟨\left(⟨{X},{Y}⟩{2}^{nd}\left({G}{\circ }_{\mathrm{func}}\left({C}{{1}^{st}}_{F}{D}\right)\right)⟨{Z},{W}⟩\right)\left(⟨{R},{S}⟩\right),\left(⟨{X},{Y}⟩{2}^{nd}\left({C}{{2}^{nd}}_{F}{D}\right)⟨{Z},{W}⟩\right)\left(⟨{R},{S}⟩\right)⟩$
75 21 28 4 36 37 38 41 cofu2 ${⊢}{\phi }\to \left(⟨{X},{Y}⟩{2}^{nd}\left({G}{\circ }_{\mathrm{func}}\left({C}{{1}^{st}}_{F}{D}\right)\right)⟨{Z},{W}⟩\right)\left(⟨{R},{S}⟩\right)=\left({1}^{st}\left({C}{{1}^{st}}_{F}{D}\right)\left(⟨{X},{Y}⟩\right){2}^{nd}\left({G}\right){1}^{st}\left({C}{{1}^{st}}_{F}{D}\right)\left(⟨{Z},{W}⟩\right)\right)\left(\left(⟨{X},{Y}⟩{2}^{nd}\left({C}{{1}^{st}}_{F}{D}\right)⟨{Z},{W}⟩\right)\left(⟨{R},{S}⟩\right)\right)$
76 50 64 oveq12d ${⊢}{\phi }\to {1}^{st}\left({C}{{1}^{st}}_{F}{D}\right)\left(⟨{X},{Y}⟩\right){2}^{nd}\left({G}\right){1}^{st}\left({C}{{1}^{st}}_{F}{D}\right)\left(⟨{Z},{W}⟩\right)={X}{2}^{nd}\left({G}\right){Z}$
77 20 21 38 26 2 27 36 37 1stf2 ${⊢}{\phi }\to ⟨{X},{Y}⟩{2}^{nd}\left({C}{{1}^{st}}_{F}{D}\right)⟨{Z},{W}⟩={{1}^{st}↾}_{\left(⟨{X},{Y}⟩\mathrm{Hom}\left({C}{×}_{c}{D}\right)⟨{Z},{W}⟩\right)}$
78 77 fveq1d ${⊢}{\phi }\to \left(⟨{X},{Y}⟩{2}^{nd}\left({C}{{1}^{st}}_{F}{D}\right)⟨{Z},{W}⟩\right)\left(⟨{R},{S}⟩\right)=\left({{1}^{st}↾}_{\left(⟨{X},{Y}⟩\mathrm{Hom}\left({C}{×}_{c}{D}\right)⟨{Z},{W}⟩\right)}\right)\left(⟨{R},{S}⟩\right)$
79 41 fvresd ${⊢}{\phi }\to \left({{1}^{st}↾}_{\left(⟨{X},{Y}⟩\mathrm{Hom}\left({C}{×}_{c}{D}\right)⟨{Z},{W}⟩\right)}\right)\left(⟨{R},{S}⟩\right)={1}^{st}\left(⟨{R},{S}⟩\right)$
80 op1stg ${⊢}\left({R}\in \left({X}{H}{Z}\right)\wedge {S}\in \left({Y}{J}{W}\right)\right)\to {1}^{st}\left(⟨{R},{S}⟩\right)={R}$
81 13 14 80 syl2anc ${⊢}{\phi }\to {1}^{st}\left(⟨{R},{S}⟩\right)={R}$
82 78 79 81 3eqtrd ${⊢}{\phi }\to \left(⟨{X},{Y}⟩{2}^{nd}\left({C}{{1}^{st}}_{F}{D}\right)⟨{Z},{W}⟩\right)\left(⟨{R},{S}⟩\right)={R}$
83 76 82 fveq12d ${⊢}{\phi }\to \left({1}^{st}\left({C}{{1}^{st}}_{F}{D}\right)\left(⟨{X},{Y}⟩\right){2}^{nd}\left({G}\right){1}^{st}\left({C}{{1}^{st}}_{F}{D}\right)\left(⟨{Z},{W}⟩\right)\right)\left(\left(⟨{X},{Y}⟩{2}^{nd}\left({C}{{1}^{st}}_{F}{D}\right)⟨{Z},{W}⟩\right)\left(⟨{R},{S}⟩\right)\right)=\left({X}{2}^{nd}\left({G}\right){Z}\right)\left({R}\right)$
84 75 83 eqtrd ${⊢}{\phi }\to \left(⟨{X},{Y}⟩{2}^{nd}\left({G}{\circ }_{\mathrm{func}}\left({C}{{1}^{st}}_{F}{D}\right)\right)⟨{Z},{W}⟩\right)\left(⟨{R},{S}⟩\right)=\left({X}{2}^{nd}\left({G}\right){Z}\right)\left({R}\right)$
85 20 21 38 26 2 30 36 37 2ndf2 ${⊢}{\phi }\to ⟨{X},{Y}⟩{2}^{nd}\left({C}{{2}^{nd}}_{F}{D}\right)⟨{Z},{W}⟩={{2}^{nd}↾}_{\left(⟨{X},{Y}⟩\mathrm{Hom}\left({C}{×}_{c}{D}\right)⟨{Z},{W}⟩\right)}$
86 85 fveq1d ${⊢}{\phi }\to \left(⟨{X},{Y}⟩{2}^{nd}\left({C}{{2}^{nd}}_{F}{D}\right)⟨{Z},{W}⟩\right)\left(⟨{R},{S}⟩\right)=\left({{2}^{nd}↾}_{\left(⟨{X},{Y}⟩\mathrm{Hom}\left({C}{×}_{c}{D}\right)⟨{Z},{W}⟩\right)}\right)\left(⟨{R},{S}⟩\right)$
87 41 fvresd ${⊢}{\phi }\to \left({{2}^{nd}↾}_{\left(⟨{X},{Y}⟩\mathrm{Hom}\left({C}{×}_{c}{D}\right)⟨{Z},{W}⟩\right)}\right)\left(⟨{R},{S}⟩\right)={2}^{nd}\left(⟨{R},{S}⟩\right)$
88 op2ndg ${⊢}\left({R}\in \left({X}{H}{Z}\right)\wedge {S}\in \left({Y}{J}{W}\right)\right)\to {2}^{nd}\left(⟨{R},{S}⟩\right)={S}$
89 13 14 88 syl2anc ${⊢}{\phi }\to {2}^{nd}\left(⟨{R},{S}⟩\right)={S}$
90 86 87 89 3eqtrd ${⊢}{\phi }\to \left(⟨{X},{Y}⟩{2}^{nd}\left({C}{{2}^{nd}}_{F}{D}\right)⟨{Z},{W}⟩\right)\left(⟨{R},{S}⟩\right)={S}$
91 84 90 opeq12d ${⊢}{\phi }\to ⟨\left(⟨{X},{Y}⟩{2}^{nd}\left({G}{\circ }_{\mathrm{func}}\left({C}{{1}^{st}}_{F}{D}\right)\right)⟨{Z},{W}⟩\right)\left(⟨{R},{S}⟩\right),\left(⟨{X},{Y}⟩{2}^{nd}\left({C}{{2}^{nd}}_{F}{D}\right)⟨{Z},{W}⟩\right)\left(⟨{R},{S}⟩\right)⟩=⟨\left({X}{2}^{nd}\left({G}\right){Z}\right)\left({R}\right),{S}⟩$
92 74 91 eqtrd ${⊢}{\phi }\to \left(⟨{X},{Y}⟩{2}^{nd}\left(\left({G}{\circ }_{\mathrm{func}}\left({C}{{1}^{st}}_{F}{D}\right)\right){⟨,⟩}_{F}\left({C}{{2}^{nd}}_{F}{D}\right)\right)⟨{Z},{W}⟩\right)\left(⟨{R},{S}⟩\right)=⟨\left({X}{2}^{nd}\left({G}\right){Z}\right)\left({R}\right),{S}⟩$
93 73 92 fveq12d ${⊢}{\phi }\to \left({1}^{st}\left(\left({G}{\circ }_{\mathrm{func}}\left({C}{{1}^{st}}_{F}{D}\right)\right){⟨,⟩}_{F}\left({C}{{2}^{nd}}_{F}{D}\right)\right)\left(⟨{X},{Y}⟩\right){2}^{nd}\left({D}{eval}_{F}{E}\right){1}^{st}\left(\left({G}{\circ }_{\mathrm{func}}\left({C}{{1}^{st}}_{F}{D}\right)\right){⟨,⟩}_{F}\left({C}{{2}^{nd}}_{F}{D}\right)\right)\left(⟨{Z},{W}⟩\right)\right)\left(\left(⟨{X},{Y}⟩{2}^{nd}\left(\left({G}{\circ }_{\mathrm{func}}\left({C}{{1}^{st}}_{F}{D}\right)\right){⟨,⟩}_{F}\left({C}{{2}^{nd}}_{F}{D}\right)\right)⟨{Z},{W}⟩\right)\left(⟨{R},{S}⟩\right)\right)=\left(⟨{1}^{st}\left({G}\right)\left({X}\right),{Y}⟩{2}^{nd}\left({D}{eval}_{F}{E}\right)⟨{1}^{st}\left({G}\right)\left({Z}\right),{W}⟩\right)\left(⟨\left({X}{2}^{nd}\left({G}\right){Z}\right)\left({R}\right),{S}⟩\right)$
94 df-ov ${⊢}\left({X}{2}^{nd}\left({G}\right){Z}\right)\left({R}\right)\left(⟨{1}^{st}\left({G}\right)\left({X}\right),{Y}⟩{2}^{nd}\left({D}{eval}_{F}{E}\right)⟨{1}^{st}\left({G}\right)\left({Z}\right),{W}⟩\right){S}=\left(⟨{1}^{st}\left({G}\right)\left({X}\right),{Y}⟩{2}^{nd}\left({D}{eval}_{F}{E}\right)⟨{1}^{st}\left({G}\right)\left({Z}\right),{W}⟩\right)\left(⟨\left({X}{2}^{nd}\left({G}\right){Z}\right)\left({R}\right),{S}⟩\right)$
95 93 94 syl6eqr ${⊢}{\phi }\to \left({1}^{st}\left(\left({G}{\circ }_{\mathrm{func}}\left({C}{{1}^{st}}_{F}{D}\right)\right){⟨,⟩}_{F}\left({C}{{2}^{nd}}_{F}{D}\right)\right)\left(⟨{X},{Y}⟩\right){2}^{nd}\left({D}{eval}_{F}{E}\right){1}^{st}\left(\left({G}{\circ }_{\mathrm{func}}\left({C}{{1}^{st}}_{F}{D}\right)\right){⟨,⟩}_{F}\left({C}{{2}^{nd}}_{F}{D}\right)\right)\left(⟨{Z},{W}⟩\right)\right)\left(\left(⟨{X},{Y}⟩{2}^{nd}\left(\left({G}{\circ }_{\mathrm{func}}\left({C}{{1}^{st}}_{F}{D}\right)\right){⟨,⟩}_{F}\left({C}{{2}^{nd}}_{F}{D}\right)\right)⟨{Z},{W}⟩\right)\left(⟨{R},{S}⟩\right)\right)=\left({X}{2}^{nd}\left({G}\right){Z}\right)\left({R}\right)\left(⟨{1}^{st}\left({G}\right)\left({X}\right),{Y}⟩{2}^{nd}\left({D}{eval}_{F}{E}\right)⟨{1}^{st}\left({G}\right)\left({Z}\right),{W}⟩\right){S}$
96 eqid ${⊢}\mathrm{comp}\left({E}\right)=\mathrm{comp}\left({E}\right)$
97 eqid ${⊢}{D}\mathrm{Nat}{E}={D}\mathrm{Nat}{E}$
98 34 fucbas ${⊢}{D}\mathrm{Func}{E}={\mathrm{Base}}_{\left({D}\mathrm{FuncCat}{E}\right)}$
99 relfunc ${⊢}\mathrm{Rel}\left({C}\mathrm{Func}\left({D}\mathrm{FuncCat}{E}\right)\right)$
100 1st2ndbr ${⊢}\left(\mathrm{Rel}\left({C}\mathrm{Func}\left({D}\mathrm{FuncCat}{E}\right)\right)\wedge {G}\in \left({C}\mathrm{Func}\left({D}\mathrm{FuncCat}{E}\right)\right)\right)\to {1}^{st}\left({G}\right)\left({C}\mathrm{Func}\left({D}\mathrm{FuncCat}{E}\right)\right){2}^{nd}\left({G}\right)$
101 99 4 100 sylancr ${⊢}{\phi }\to {1}^{st}\left({G}\right)\left({C}\mathrm{Func}\left({D}\mathrm{FuncCat}{E}\right)\right){2}^{nd}\left({G}\right)$
102 5 98 101 funcf1 ${⊢}{\phi }\to {1}^{st}\left({G}\right):{A}⟶{D}\mathrm{Func}{E}$
103 102 7 ffvelrnd ${⊢}{\phi }\to {1}^{st}\left({G}\right)\left({X}\right)\in \left({D}\mathrm{Func}{E}\right)$
104 102 11 ffvelrnd ${⊢}{\phi }\to {1}^{st}\left({G}\right)\left({Z}\right)\in \left({D}\mathrm{Func}{E}\right)$
105 eqid ${⊢}⟨{1}^{st}\left({G}\right)\left({X}\right),{Y}⟩{2}^{nd}\left({D}{eval}_{F}{E}\right)⟨{1}^{st}\left({G}\right)\left({Z}\right),{W}⟩=⟨{1}^{st}\left({G}\right)\left({X}\right),{Y}⟩{2}^{nd}\left({D}{eval}_{F}{E}\right)⟨{1}^{st}\left({G}\right)\left({Z}\right),{W}⟩$
106 34 97 fuchom ${⊢}{D}\mathrm{Nat}{E}=\mathrm{Hom}\left({D}\mathrm{FuncCat}{E}\right)$
107 5 9 106 101 7 11 funcf2 ${⊢}{\phi }\to \left({X}{2}^{nd}\left({G}\right){Z}\right):{X}{H}{Z}⟶{1}^{st}\left({G}\right)\left({X}\right)\left({D}\mathrm{Nat}{E}\right){1}^{st}\left({G}\right)\left({Z}\right)$
108 107 13 ffvelrnd ${⊢}{\phi }\to \left({X}{2}^{nd}\left({G}\right){Z}\right)\left({R}\right)\in \left({1}^{st}\left({G}\right)\left({X}\right)\left({D}\mathrm{Nat}{E}\right){1}^{st}\left({G}\right)\left({Z}\right)\right)$
109 33 2 3 6 10 96 97 103 104 8 12 105 108 14 evlf2val ${⊢}{\phi }\to \left({X}{2}^{nd}\left({G}\right){Z}\right)\left({R}\right)\left(⟨{1}^{st}\left({G}\right)\left({X}\right),{Y}⟩{2}^{nd}\left({D}{eval}_{F}{E}\right)⟨{1}^{st}\left({G}\right)\left({Z}\right),{W}⟩\right){S}=\left({X}{2}^{nd}\left({G}\right){Z}\right)\left({R}\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({S}\right)$
110 44 95 109 3eqtrd ${⊢}{\phi }\to {R}\left(⟨{X},{Y}⟩{2}^{nd}\left({F}\right)⟨{Z},{W}⟩\right){S}=\left({X}{2}^{nd}\left({G}\right){Z}\right)\left({R}\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({S}\right)$