# Metamath Proof Explorer

## Theorem curfcl

Description: The curry functor of a functor F : C X. D --> E is a functor curryF ( F ) : C --> ( D --> E ) . (Contributed by Mario Carneiro, 13-Jan-2017)

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

### Proof

Step Hyp Ref Expression
1 curfcl.g ${⊢}{G}=⟨{C},{D}⟩{curry}_{F}{F}$
2 curfcl.q ${⊢}{Q}={D}\mathrm{FuncCat}{E}$
3 curfcl.c ${⊢}{\phi }\to {C}\in \mathrm{Cat}$
4 curfcl.d ${⊢}{\phi }\to {D}\in \mathrm{Cat}$
5 curfcl.f ${⊢}{\phi }\to {F}\in \left(\left({C}{×}_{c}{D}\right)\mathrm{Func}{E}\right)$
6 eqid ${⊢}{\mathrm{Base}}_{{C}}={\mathrm{Base}}_{{C}}$
7 eqid ${⊢}{\mathrm{Base}}_{{D}}={\mathrm{Base}}_{{D}}$
8 eqid ${⊢}\mathrm{Hom}\left({D}\right)=\mathrm{Hom}\left({D}\right)$
9 eqid ${⊢}\mathrm{Id}\left({C}\right)=\mathrm{Id}\left({C}\right)$
10 eqid ${⊢}\mathrm{Hom}\left({C}\right)=\mathrm{Hom}\left({C}\right)$
11 eqid ${⊢}\mathrm{Id}\left({D}\right)=\mathrm{Id}\left({D}\right)$
12 1 6 3 4 5 7 8 9 10 11 curfval ${⊢}{\phi }\to {G}=⟨\left({x}\in {\mathrm{Base}}_{{C}}⟼⟨\left({y}\in {\mathrm{Base}}_{{D}}⟼{x}{1}^{st}\left({F}\right){y}\right),\left({y}\in {\mathrm{Base}}_{{D}},{z}\in {\mathrm{Base}}_{{D}}⟼\left({g}\in \left({y}\mathrm{Hom}\left({D}\right){z}\right)⟼\mathrm{Id}\left({C}\right)\left({x}\right)\left(⟨{x},{y}⟩{2}^{nd}\left({F}\right)⟨{x},{z}⟩\right){g}\right)\right)⟩\right),\left({x}\in {\mathrm{Base}}_{{C}},{y}\in {\mathrm{Base}}_{{C}}⟼\left({g}\in \left({x}\mathrm{Hom}\left({C}\right){y}\right)⟼\left({z}\in {\mathrm{Base}}_{{D}}⟼{g}\left(⟨{x},{z}⟩{2}^{nd}\left({F}\right)⟨{y},{z}⟩\right)\mathrm{Id}\left({D}\right)\left({z}\right)\right)\right)\right)⟩$
13 fvex ${⊢}{\mathrm{Base}}_{{C}}\in \mathrm{V}$
14 13 mptex ${⊢}\left({x}\in {\mathrm{Base}}_{{C}}⟼⟨\left({y}\in {\mathrm{Base}}_{{D}}⟼{x}{1}^{st}\left({F}\right){y}\right),\left({y}\in {\mathrm{Base}}_{{D}},{z}\in {\mathrm{Base}}_{{D}}⟼\left({g}\in \left({y}\mathrm{Hom}\left({D}\right){z}\right)⟼\mathrm{Id}\left({C}\right)\left({x}\right)\left(⟨{x},{y}⟩{2}^{nd}\left({F}\right)⟨{x},{z}⟩\right){g}\right)\right)⟩\right)\in \mathrm{V}$
15 13 13 mpoex ${⊢}\left({x}\in {\mathrm{Base}}_{{C}},{y}\in {\mathrm{Base}}_{{C}}⟼\left({g}\in \left({x}\mathrm{Hom}\left({C}\right){y}\right)⟼\left({z}\in {\mathrm{Base}}_{{D}}⟼{g}\left(⟨{x},{z}⟩{2}^{nd}\left({F}\right)⟨{y},{z}⟩\right)\mathrm{Id}\left({D}\right)\left({z}\right)\right)\right)\right)\in \mathrm{V}$
16 14 15 op1std ${⊢}{G}=⟨\left({x}\in {\mathrm{Base}}_{{C}}⟼⟨\left({y}\in {\mathrm{Base}}_{{D}}⟼{x}{1}^{st}\left({F}\right){y}\right),\left({y}\in {\mathrm{Base}}_{{D}},{z}\in {\mathrm{Base}}_{{D}}⟼\left({g}\in \left({y}\mathrm{Hom}\left({D}\right){z}\right)⟼\mathrm{Id}\left({C}\right)\left({x}\right)\left(⟨{x},{y}⟩{2}^{nd}\left({F}\right)⟨{x},{z}⟩\right){g}\right)\right)⟩\right),\left({x}\in {\mathrm{Base}}_{{C}},{y}\in {\mathrm{Base}}_{{C}}⟼\left({g}\in \left({x}\mathrm{Hom}\left({C}\right){y}\right)⟼\left({z}\in {\mathrm{Base}}_{{D}}⟼{g}\left(⟨{x},{z}⟩{2}^{nd}\left({F}\right)⟨{y},{z}⟩\right)\mathrm{Id}\left({D}\right)\left({z}\right)\right)\right)\right)⟩\to {1}^{st}\left({G}\right)=\left({x}\in {\mathrm{Base}}_{{C}}⟼⟨\left({y}\in {\mathrm{Base}}_{{D}}⟼{x}{1}^{st}\left({F}\right){y}\right),\left({y}\in {\mathrm{Base}}_{{D}},{z}\in {\mathrm{Base}}_{{D}}⟼\left({g}\in \left({y}\mathrm{Hom}\left({D}\right){z}\right)⟼\mathrm{Id}\left({C}\right)\left({x}\right)\left(⟨{x},{y}⟩{2}^{nd}\left({F}\right)⟨{x},{z}⟩\right){g}\right)\right)⟩\right)$
17 12 16 syl ${⊢}{\phi }\to {1}^{st}\left({G}\right)=\left({x}\in {\mathrm{Base}}_{{C}}⟼⟨\left({y}\in {\mathrm{Base}}_{{D}}⟼{x}{1}^{st}\left({F}\right){y}\right),\left({y}\in {\mathrm{Base}}_{{D}},{z}\in {\mathrm{Base}}_{{D}}⟼\left({g}\in \left({y}\mathrm{Hom}\left({D}\right){z}\right)⟼\mathrm{Id}\left({C}\right)\left({x}\right)\left(⟨{x},{y}⟩{2}^{nd}\left({F}\right)⟨{x},{z}⟩\right){g}\right)\right)⟩\right)$
18 14 15 op2ndd ${⊢}{G}=⟨\left({x}\in {\mathrm{Base}}_{{C}}⟼⟨\left({y}\in {\mathrm{Base}}_{{D}}⟼{x}{1}^{st}\left({F}\right){y}\right),\left({y}\in {\mathrm{Base}}_{{D}},{z}\in {\mathrm{Base}}_{{D}}⟼\left({g}\in \left({y}\mathrm{Hom}\left({D}\right){z}\right)⟼\mathrm{Id}\left({C}\right)\left({x}\right)\left(⟨{x},{y}⟩{2}^{nd}\left({F}\right)⟨{x},{z}⟩\right){g}\right)\right)⟩\right),\left({x}\in {\mathrm{Base}}_{{C}},{y}\in {\mathrm{Base}}_{{C}}⟼\left({g}\in \left({x}\mathrm{Hom}\left({C}\right){y}\right)⟼\left({z}\in {\mathrm{Base}}_{{D}}⟼{g}\left(⟨{x},{z}⟩{2}^{nd}\left({F}\right)⟨{y},{z}⟩\right)\mathrm{Id}\left({D}\right)\left({z}\right)\right)\right)\right)⟩\to {2}^{nd}\left({G}\right)=\left({x}\in {\mathrm{Base}}_{{C}},{y}\in {\mathrm{Base}}_{{C}}⟼\left({g}\in \left({x}\mathrm{Hom}\left({C}\right){y}\right)⟼\left({z}\in {\mathrm{Base}}_{{D}}⟼{g}\left(⟨{x},{z}⟩{2}^{nd}\left({F}\right)⟨{y},{z}⟩\right)\mathrm{Id}\left({D}\right)\left({z}\right)\right)\right)\right)$
19 12 18 syl ${⊢}{\phi }\to {2}^{nd}\left({G}\right)=\left({x}\in {\mathrm{Base}}_{{C}},{y}\in {\mathrm{Base}}_{{C}}⟼\left({g}\in \left({x}\mathrm{Hom}\left({C}\right){y}\right)⟼\left({z}\in {\mathrm{Base}}_{{D}}⟼{g}\left(⟨{x},{z}⟩{2}^{nd}\left({F}\right)⟨{y},{z}⟩\right)\mathrm{Id}\left({D}\right)\left({z}\right)\right)\right)\right)$
20 17 19 opeq12d ${⊢}{\phi }\to ⟨{1}^{st}\left({G}\right),{2}^{nd}\left({G}\right)⟩=⟨\left({x}\in {\mathrm{Base}}_{{C}}⟼⟨\left({y}\in {\mathrm{Base}}_{{D}}⟼{x}{1}^{st}\left({F}\right){y}\right),\left({y}\in {\mathrm{Base}}_{{D}},{z}\in {\mathrm{Base}}_{{D}}⟼\left({g}\in \left({y}\mathrm{Hom}\left({D}\right){z}\right)⟼\mathrm{Id}\left({C}\right)\left({x}\right)\left(⟨{x},{y}⟩{2}^{nd}\left({F}\right)⟨{x},{z}⟩\right){g}\right)\right)⟩\right),\left({x}\in {\mathrm{Base}}_{{C}},{y}\in {\mathrm{Base}}_{{C}}⟼\left({g}\in \left({x}\mathrm{Hom}\left({C}\right){y}\right)⟼\left({z}\in {\mathrm{Base}}_{{D}}⟼{g}\left(⟨{x},{z}⟩{2}^{nd}\left({F}\right)⟨{y},{z}⟩\right)\mathrm{Id}\left({D}\right)\left({z}\right)\right)\right)\right)⟩$
21 12 20 eqtr4d ${⊢}{\phi }\to {G}=⟨{1}^{st}\left({G}\right),{2}^{nd}\left({G}\right)⟩$
22 2 fucbas ${⊢}{D}\mathrm{Func}{E}={\mathrm{Base}}_{{Q}}$
23 eqid ${⊢}{D}\mathrm{Nat}{E}={D}\mathrm{Nat}{E}$
24 2 23 fuchom ${⊢}{D}\mathrm{Nat}{E}=\mathrm{Hom}\left({Q}\right)$
25 eqid ${⊢}\mathrm{Id}\left({Q}\right)=\mathrm{Id}\left({Q}\right)$
26 eqid ${⊢}\mathrm{comp}\left({C}\right)=\mathrm{comp}\left({C}\right)$
27 eqid ${⊢}\mathrm{comp}\left({Q}\right)=\mathrm{comp}\left({Q}\right)$
28 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)$
29 5 28 syl ${⊢}{\phi }\to \left({C}{×}_{c}{D}\in \mathrm{Cat}\wedge {E}\in \mathrm{Cat}\right)$
30 29 simprd ${⊢}{\phi }\to {E}\in \mathrm{Cat}$
31 2 4 30 fuccat ${⊢}{\phi }\to {Q}\in \mathrm{Cat}$
32 opex ${⊢}⟨\left({y}\in {\mathrm{Base}}_{{D}}⟼{x}{1}^{st}\left({F}\right){y}\right),\left({y}\in {\mathrm{Base}}_{{D}},{z}\in {\mathrm{Base}}_{{D}}⟼\left({g}\in \left({y}\mathrm{Hom}\left({D}\right){z}\right)⟼\mathrm{Id}\left({C}\right)\left({x}\right)\left(⟨{x},{y}⟩{2}^{nd}\left({F}\right)⟨{x},{z}⟩\right){g}\right)\right)⟩\in \mathrm{V}$
33 32 a1i ${⊢}\left({\phi }\wedge {x}\in {\mathrm{Base}}_{{C}}\right)\to ⟨\left({y}\in {\mathrm{Base}}_{{D}}⟼{x}{1}^{st}\left({F}\right){y}\right),\left({y}\in {\mathrm{Base}}_{{D}},{z}\in {\mathrm{Base}}_{{D}}⟼\left({g}\in \left({y}\mathrm{Hom}\left({D}\right){z}\right)⟼\mathrm{Id}\left({C}\right)\left({x}\right)\left(⟨{x},{y}⟩{2}^{nd}\left({F}\right)⟨{x},{z}⟩\right){g}\right)\right)⟩\in \mathrm{V}$
34 3 adantr ${⊢}\left({\phi }\wedge {x}\in {\mathrm{Base}}_{{C}}\right)\to {C}\in \mathrm{Cat}$
35 4 adantr ${⊢}\left({\phi }\wedge {x}\in {\mathrm{Base}}_{{C}}\right)\to {D}\in \mathrm{Cat}$
36 5 adantr ${⊢}\left({\phi }\wedge {x}\in {\mathrm{Base}}_{{C}}\right)\to {F}\in \left(\left({C}{×}_{c}{D}\right)\mathrm{Func}{E}\right)$
37 simpr ${⊢}\left({\phi }\wedge {x}\in {\mathrm{Base}}_{{C}}\right)\to {x}\in {\mathrm{Base}}_{{C}}$
38 eqid ${⊢}{1}^{st}\left({G}\right)\left({x}\right)={1}^{st}\left({G}\right)\left({x}\right)$
39 1 6 34 35 36 7 37 38 curf1cl ${⊢}\left({\phi }\wedge {x}\in {\mathrm{Base}}_{{C}}\right)\to {1}^{st}\left({G}\right)\left({x}\right)\in \left({D}\mathrm{Func}{E}\right)$
40 33 17 39 fmpt2d ${⊢}{\phi }\to {1}^{st}\left({G}\right):{\mathrm{Base}}_{{C}}⟶{D}\mathrm{Func}{E}$
41 eqid ${⊢}\left({x}\in {\mathrm{Base}}_{{C}},{y}\in {\mathrm{Base}}_{{C}}⟼\left({g}\in \left({x}\mathrm{Hom}\left({C}\right){y}\right)⟼\left({z}\in {\mathrm{Base}}_{{D}}⟼{g}\left(⟨{x},{z}⟩{2}^{nd}\left({F}\right)⟨{y},{z}⟩\right)\mathrm{Id}\left({D}\right)\left({z}\right)\right)\right)\right)=\left({x}\in {\mathrm{Base}}_{{C}},{y}\in {\mathrm{Base}}_{{C}}⟼\left({g}\in \left({x}\mathrm{Hom}\left({C}\right){y}\right)⟼\left({z}\in {\mathrm{Base}}_{{D}}⟼{g}\left(⟨{x},{z}⟩{2}^{nd}\left({F}\right)⟨{y},{z}⟩\right)\mathrm{Id}\left({D}\right)\left({z}\right)\right)\right)\right)$
42 ovex ${⊢}{x}\mathrm{Hom}\left({C}\right){y}\in \mathrm{V}$
43 42 mptex ${⊢}\left({g}\in \left({x}\mathrm{Hom}\left({C}\right){y}\right)⟼\left({z}\in {\mathrm{Base}}_{{D}}⟼{g}\left(⟨{x},{z}⟩{2}^{nd}\left({F}\right)⟨{y},{z}⟩\right)\mathrm{Id}\left({D}\right)\left({z}\right)\right)\right)\in \mathrm{V}$
44 41 43 fnmpoi ${⊢}\left({x}\in {\mathrm{Base}}_{{C}},{y}\in {\mathrm{Base}}_{{C}}⟼\left({g}\in \left({x}\mathrm{Hom}\left({C}\right){y}\right)⟼\left({z}\in {\mathrm{Base}}_{{D}}⟼{g}\left(⟨{x},{z}⟩{2}^{nd}\left({F}\right)⟨{y},{z}⟩\right)\mathrm{Id}\left({D}\right)\left({z}\right)\right)\right)\right)Fn\left({\mathrm{Base}}_{{C}}×{\mathrm{Base}}_{{C}}\right)$
45 19 fneq1d ${⊢}{\phi }\to \left({2}^{nd}\left({G}\right)Fn\left({\mathrm{Base}}_{{C}}×{\mathrm{Base}}_{{C}}\right)↔\left({x}\in {\mathrm{Base}}_{{C}},{y}\in {\mathrm{Base}}_{{C}}⟼\left({g}\in \left({x}\mathrm{Hom}\left({C}\right){y}\right)⟼\left({z}\in {\mathrm{Base}}_{{D}}⟼{g}\left(⟨{x},{z}⟩{2}^{nd}\left({F}\right)⟨{y},{z}⟩\right)\mathrm{Id}\left({D}\right)\left({z}\right)\right)\right)\right)Fn\left({\mathrm{Base}}_{{C}}×{\mathrm{Base}}_{{C}}\right)\right)$
46 44 45 mpbiri ${⊢}{\phi }\to {2}^{nd}\left({G}\right)Fn\left({\mathrm{Base}}_{{C}}×{\mathrm{Base}}_{{C}}\right)$
47 fvex ${⊢}{\mathrm{Base}}_{{D}}\in \mathrm{V}$
48 47 mptex ${⊢}\left({z}\in {\mathrm{Base}}_{{D}}⟼{g}\left(⟨{x},{z}⟩{2}^{nd}\left({F}\right)⟨{y},{z}⟩\right)\mathrm{Id}\left({D}\right)\left({z}\right)\right)\in \mathrm{V}$
49 48 a1i ${⊢}\left(\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\right)\right)\wedge {g}\in \left({x}\mathrm{Hom}\left({C}\right){y}\right)\right)\to \left({z}\in {\mathrm{Base}}_{{D}}⟼{g}\left(⟨{x},{z}⟩{2}^{nd}\left({F}\right)⟨{y},{z}⟩\right)\mathrm{Id}\left({D}\right)\left({z}\right)\right)\in \mathrm{V}$
50 19 oveqd ${⊢}{\phi }\to {x}{2}^{nd}\left({G}\right){y}={x}\left({x}\in {\mathrm{Base}}_{{C}},{y}\in {\mathrm{Base}}_{{C}}⟼\left({g}\in \left({x}\mathrm{Hom}\left({C}\right){y}\right)⟼\left({z}\in {\mathrm{Base}}_{{D}}⟼{g}\left(⟨{x},{z}⟩{2}^{nd}\left({F}\right)⟨{y},{z}⟩\right)\mathrm{Id}\left({D}\right)\left({z}\right)\right)\right)\right){y}$
51 41 ovmpt4g ${⊢}\left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\wedge \left({g}\in \left({x}\mathrm{Hom}\left({C}\right){y}\right)⟼\left({z}\in {\mathrm{Base}}_{{D}}⟼{g}\left(⟨{x},{z}⟩{2}^{nd}\left({F}\right)⟨{y},{z}⟩\right)\mathrm{Id}\left({D}\right)\left({z}\right)\right)\right)\in \mathrm{V}\right)\to {x}\left({x}\in {\mathrm{Base}}_{{C}},{y}\in {\mathrm{Base}}_{{C}}⟼\left({g}\in \left({x}\mathrm{Hom}\left({C}\right){y}\right)⟼\left({z}\in {\mathrm{Base}}_{{D}}⟼{g}\left(⟨{x},{z}⟩{2}^{nd}\left({F}\right)⟨{y},{z}⟩\right)\mathrm{Id}\left({D}\right)\left({z}\right)\right)\right)\right){y}=\left({g}\in \left({x}\mathrm{Hom}\left({C}\right){y}\right)⟼\left({z}\in {\mathrm{Base}}_{{D}}⟼{g}\left(⟨{x},{z}⟩{2}^{nd}\left({F}\right)⟨{y},{z}⟩\right)\mathrm{Id}\left({D}\right)\left({z}\right)\right)\right)$
52 43 51 mp3an3 ${⊢}\left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\right)\to {x}\left({x}\in {\mathrm{Base}}_{{C}},{y}\in {\mathrm{Base}}_{{C}}⟼\left({g}\in \left({x}\mathrm{Hom}\left({C}\right){y}\right)⟼\left({z}\in {\mathrm{Base}}_{{D}}⟼{g}\left(⟨{x},{z}⟩{2}^{nd}\left({F}\right)⟨{y},{z}⟩\right)\mathrm{Id}\left({D}\right)\left({z}\right)\right)\right)\right){y}=\left({g}\in \left({x}\mathrm{Hom}\left({C}\right){y}\right)⟼\left({z}\in {\mathrm{Base}}_{{D}}⟼{g}\left(⟨{x},{z}⟩{2}^{nd}\left({F}\right)⟨{y},{z}⟩\right)\mathrm{Id}\left({D}\right)\left({z}\right)\right)\right)$
53 50 52 sylan9eq ${⊢}\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\right)\right)\to {x}{2}^{nd}\left({G}\right){y}=\left({g}\in \left({x}\mathrm{Hom}\left({C}\right){y}\right)⟼\left({z}\in {\mathrm{Base}}_{{D}}⟼{g}\left(⟨{x},{z}⟩{2}^{nd}\left({F}\right)⟨{y},{z}⟩\right)\mathrm{Id}\left({D}\right)\left({z}\right)\right)\right)$
54 3 ad2antrr ${⊢}\left(\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\right)\right)\wedge {g}\in \left({x}\mathrm{Hom}\left({C}\right){y}\right)\right)\to {C}\in \mathrm{Cat}$
55 4 ad2antrr ${⊢}\left(\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\right)\right)\wedge {g}\in \left({x}\mathrm{Hom}\left({C}\right){y}\right)\right)\to {D}\in \mathrm{Cat}$
56 5 ad2antrr ${⊢}\left(\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\right)\right)\wedge {g}\in \left({x}\mathrm{Hom}\left({C}\right){y}\right)\right)\to {F}\in \left(\left({C}{×}_{c}{D}\right)\mathrm{Func}{E}\right)$
57 simplrl ${⊢}\left(\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\right)\right)\wedge {g}\in \left({x}\mathrm{Hom}\left({C}\right){y}\right)\right)\to {x}\in {\mathrm{Base}}_{{C}}$
58 simplrr ${⊢}\left(\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\right)\right)\wedge {g}\in \left({x}\mathrm{Hom}\left({C}\right){y}\right)\right)\to {y}\in {\mathrm{Base}}_{{C}}$
59 simpr ${⊢}\left(\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\right)\right)\wedge {g}\in \left({x}\mathrm{Hom}\left({C}\right){y}\right)\right)\to {g}\in \left({x}\mathrm{Hom}\left({C}\right){y}\right)$
60 eqid ${⊢}\left({x}{2}^{nd}\left({G}\right){y}\right)\left({g}\right)=\left({x}{2}^{nd}\left({G}\right){y}\right)\left({g}\right)$
61 1 6 54 55 56 7 10 11 57 58 59 60 23 curf2cl ${⊢}\left(\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\right)\right)\wedge {g}\in \left({x}\mathrm{Hom}\left({C}\right){y}\right)\right)\to \left({x}{2}^{nd}\left({G}\right){y}\right)\left({g}\right)\in \left({1}^{st}\left({G}\right)\left({x}\right)\left({D}\mathrm{Nat}{E}\right){1}^{st}\left({G}\right)\left({y}\right)\right)$
62 49 53 61 fmpt2d ${⊢}\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\right)\right)\to \left({x}{2}^{nd}\left({G}\right){y}\right):{x}\mathrm{Hom}\left({C}\right){y}⟶{1}^{st}\left({G}\right)\left({x}\right)\left({D}\mathrm{Nat}{E}\right){1}^{st}\left({G}\right)\left({y}\right)$
63 eqid ${⊢}{C}{×}_{c}{D}={C}{×}_{c}{D}$
64 63 6 7 xpcbas ${⊢}{\mathrm{Base}}_{{C}}×{\mathrm{Base}}_{{D}}={\mathrm{Base}}_{\left({C}{×}_{c}{D}\right)}$
65 eqid ${⊢}\mathrm{Id}\left({C}{×}_{c}{D}\right)=\mathrm{Id}\left({C}{×}_{c}{D}\right)$
66 eqid ${⊢}\mathrm{Id}\left({E}\right)=\mathrm{Id}\left({E}\right)$
67 relfunc ${⊢}\mathrm{Rel}\left(\left({C}{×}_{c}{D}\right)\mathrm{Func}{E}\right)$
68 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)$
69 67 5 68 sylancr ${⊢}{\phi }\to {1}^{st}\left({F}\right)\left(\left({C}{×}_{c}{D}\right)\mathrm{Func}{E}\right){2}^{nd}\left({F}\right)$
70 69 ad2antrr ${⊢}\left(\left({\phi }\wedge {x}\in {\mathrm{Base}}_{{C}}\right)\wedge {y}\in {\mathrm{Base}}_{{D}}\right)\to {1}^{st}\left({F}\right)\left(\left({C}{×}_{c}{D}\right)\mathrm{Func}{E}\right){2}^{nd}\left({F}\right)$
71 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)$
72 71 adantll ${⊢}\left(\left({\phi }\wedge {x}\in {\mathrm{Base}}_{{C}}\right)\wedge {y}\in {\mathrm{Base}}_{{D}}\right)\to ⟨{x},{y}⟩\in \left({\mathrm{Base}}_{{C}}×{\mathrm{Base}}_{{D}}\right)$
73 64 65 66 70 72 funcid ${⊢}\left(\left({\phi }\wedge {x}\in {\mathrm{Base}}_{{C}}\right)\wedge {y}\in {\mathrm{Base}}_{{D}}\right)\to \left(⟨{x},{y}⟩{2}^{nd}\left({F}\right)⟨{x},{y}⟩\right)\left(\mathrm{Id}\left({C}{×}_{c}{D}\right)\left(⟨{x},{y}⟩\right)\right)=\mathrm{Id}\left({E}\right)\left({1}^{st}\left({F}\right)\left(⟨{x},{y}⟩\right)\right)$
74 3 ad2antrr ${⊢}\left(\left({\phi }\wedge {x}\in {\mathrm{Base}}_{{C}}\right)\wedge {y}\in {\mathrm{Base}}_{{D}}\right)\to {C}\in \mathrm{Cat}$
75 4 ad2antrr ${⊢}\left(\left({\phi }\wedge {x}\in {\mathrm{Base}}_{{C}}\right)\wedge {y}\in {\mathrm{Base}}_{{D}}\right)\to {D}\in \mathrm{Cat}$
76 37 adantr ${⊢}\left(\left({\phi }\wedge {x}\in {\mathrm{Base}}_{{C}}\right)\wedge {y}\in {\mathrm{Base}}_{{D}}\right)\to {x}\in {\mathrm{Base}}_{{C}}$
77 simpr ${⊢}\left(\left({\phi }\wedge {x}\in {\mathrm{Base}}_{{C}}\right)\wedge {y}\in {\mathrm{Base}}_{{D}}\right)\to {y}\in {\mathrm{Base}}_{{D}}$
78 63 74 75 6 7 9 11 65 76 77 xpcid ${⊢}\left(\left({\phi }\wedge {x}\in {\mathrm{Base}}_{{C}}\right)\wedge {y}\in {\mathrm{Base}}_{{D}}\right)\to \mathrm{Id}\left({C}{×}_{c}{D}\right)\left(⟨{x},{y}⟩\right)=⟨\mathrm{Id}\left({C}\right)\left({x}\right),\mathrm{Id}\left({D}\right)\left({y}\right)⟩$
79 78 fveq2d ${⊢}\left(\left({\phi }\wedge {x}\in {\mathrm{Base}}_{{C}}\right)\wedge {y}\in {\mathrm{Base}}_{{D}}\right)\to \left(⟨{x},{y}⟩{2}^{nd}\left({F}\right)⟨{x},{y}⟩\right)\left(\mathrm{Id}\left({C}{×}_{c}{D}\right)\left(⟨{x},{y}⟩\right)\right)=\left(⟨{x},{y}⟩{2}^{nd}\left({F}\right)⟨{x},{y}⟩\right)\left(⟨\mathrm{Id}\left({C}\right)\left({x}\right),\mathrm{Id}\left({D}\right)\left({y}\right)⟩\right)$
80 df-ov ${⊢}\mathrm{Id}\left({C}\right)\left({x}\right)\left(⟨{x},{y}⟩{2}^{nd}\left({F}\right)⟨{x},{y}⟩\right)\mathrm{Id}\left({D}\right)\left({y}\right)=\left(⟨{x},{y}⟩{2}^{nd}\left({F}\right)⟨{x},{y}⟩\right)\left(⟨\mathrm{Id}\left({C}\right)\left({x}\right),\mathrm{Id}\left({D}\right)\left({y}\right)⟩\right)$
81 79 80 syl6eqr ${⊢}\left(\left({\phi }\wedge {x}\in {\mathrm{Base}}_{{C}}\right)\wedge {y}\in {\mathrm{Base}}_{{D}}\right)\to \left(⟨{x},{y}⟩{2}^{nd}\left({F}\right)⟨{x},{y}⟩\right)\left(\mathrm{Id}\left({C}{×}_{c}{D}\right)\left(⟨{x},{y}⟩\right)\right)=\mathrm{Id}\left({C}\right)\left({x}\right)\left(⟨{x},{y}⟩{2}^{nd}\left({F}\right)⟨{x},{y}⟩\right)\mathrm{Id}\left({D}\right)\left({y}\right)$
82 5 ad2antrr ${⊢}\left(\left({\phi }\wedge {x}\in {\mathrm{Base}}_{{C}}\right)\wedge {y}\in {\mathrm{Base}}_{{D}}\right)\to {F}\in \left(\left({C}{×}_{c}{D}\right)\mathrm{Func}{E}\right)$
83 1 6 74 75 82 7 76 38 77 curf11 ${⊢}\left(\left({\phi }\wedge {x}\in {\mathrm{Base}}_{{C}}\right)\wedge {y}\in {\mathrm{Base}}_{{D}}\right)\to {1}^{st}\left({1}^{st}\left({G}\right)\left({x}\right)\right)\left({y}\right)={x}{1}^{st}\left({F}\right){y}$
84 df-ov ${⊢}{x}{1}^{st}\left({F}\right){y}={1}^{st}\left({F}\right)\left(⟨{x},{y}⟩\right)$
85 83 84 syl6req ${⊢}\left(\left({\phi }\wedge {x}\in {\mathrm{Base}}_{{C}}\right)\wedge {y}\in {\mathrm{Base}}_{{D}}\right)\to {1}^{st}\left({F}\right)\left(⟨{x},{y}⟩\right)={1}^{st}\left({1}^{st}\left({G}\right)\left({x}\right)\right)\left({y}\right)$
86 85 fveq2d ${⊢}\left(\left({\phi }\wedge {x}\in {\mathrm{Base}}_{{C}}\right)\wedge {y}\in {\mathrm{Base}}_{{D}}\right)\to \mathrm{Id}\left({E}\right)\left({1}^{st}\left({F}\right)\left(⟨{x},{y}⟩\right)\right)=\mathrm{Id}\left({E}\right)\left({1}^{st}\left({1}^{st}\left({G}\right)\left({x}\right)\right)\left({y}\right)\right)$
87 73 81 86 3eqtr3d ${⊢}\left(\left({\phi }\wedge {x}\in {\mathrm{Base}}_{{C}}\right)\wedge {y}\in {\mathrm{Base}}_{{D}}\right)\to \mathrm{Id}\left({C}\right)\left({x}\right)\left(⟨{x},{y}⟩{2}^{nd}\left({F}\right)⟨{x},{y}⟩\right)\mathrm{Id}\left({D}\right)\left({y}\right)=\mathrm{Id}\left({E}\right)\left({1}^{st}\left({1}^{st}\left({G}\right)\left({x}\right)\right)\left({y}\right)\right)$
88 87 mpteq2dva ${⊢}\left({\phi }\wedge {x}\in {\mathrm{Base}}_{{C}}\right)\to \left({y}\in {\mathrm{Base}}_{{D}}⟼\mathrm{Id}\left({C}\right)\left({x}\right)\left(⟨{x},{y}⟩{2}^{nd}\left({F}\right)⟨{x},{y}⟩\right)\mathrm{Id}\left({D}\right)\left({y}\right)\right)=\left({y}\in {\mathrm{Base}}_{{D}}⟼\mathrm{Id}\left({E}\right)\left({1}^{st}\left({1}^{st}\left({G}\right)\left({x}\right)\right)\left({y}\right)\right)\right)$
89 30 adantr ${⊢}\left({\phi }\wedge {x}\in {\mathrm{Base}}_{{C}}\right)\to {E}\in \mathrm{Cat}$
90 eqid ${⊢}{\mathrm{Base}}_{{E}}={\mathrm{Base}}_{{E}}$
91 90 66 cidfn ${⊢}{E}\in \mathrm{Cat}\to \mathrm{Id}\left({E}\right)Fn{\mathrm{Base}}_{{E}}$
92 89 91 syl ${⊢}\left({\phi }\wedge {x}\in {\mathrm{Base}}_{{C}}\right)\to \mathrm{Id}\left({E}\right)Fn{\mathrm{Base}}_{{E}}$
93 dffn2 ${⊢}\mathrm{Id}\left({E}\right)Fn{\mathrm{Base}}_{{E}}↔\mathrm{Id}\left({E}\right):{\mathrm{Base}}_{{E}}⟶\mathrm{V}$
94 92 93 sylib ${⊢}\left({\phi }\wedge {x}\in {\mathrm{Base}}_{{C}}\right)\to \mathrm{Id}\left({E}\right):{\mathrm{Base}}_{{E}}⟶\mathrm{V}$
95 relfunc ${⊢}\mathrm{Rel}\left({D}\mathrm{Func}{E}\right)$
96 1st2ndbr ${⊢}\left(\mathrm{Rel}\left({D}\mathrm{Func}{E}\right)\wedge {1}^{st}\left({G}\right)\left({x}\right)\in \left({D}\mathrm{Func}{E}\right)\right)\to {1}^{st}\left({1}^{st}\left({G}\right)\left({x}\right)\right)\left({D}\mathrm{Func}{E}\right){2}^{nd}\left({1}^{st}\left({G}\right)\left({x}\right)\right)$
97 95 39 96 sylancr ${⊢}\left({\phi }\wedge {x}\in {\mathrm{Base}}_{{C}}\right)\to {1}^{st}\left({1}^{st}\left({G}\right)\left({x}\right)\right)\left({D}\mathrm{Func}{E}\right){2}^{nd}\left({1}^{st}\left({G}\right)\left({x}\right)\right)$
98 7 90 97 funcf1 ${⊢}\left({\phi }\wedge {x}\in {\mathrm{Base}}_{{C}}\right)\to {1}^{st}\left({1}^{st}\left({G}\right)\left({x}\right)\right):{\mathrm{Base}}_{{D}}⟶{\mathrm{Base}}_{{E}}$
99 fcompt ${⊢}\left(\mathrm{Id}\left({E}\right):{\mathrm{Base}}_{{E}}⟶\mathrm{V}\wedge {1}^{st}\left({1}^{st}\left({G}\right)\left({x}\right)\right):{\mathrm{Base}}_{{D}}⟶{\mathrm{Base}}_{{E}}\right)\to \mathrm{Id}\left({E}\right)\circ {1}^{st}\left({1}^{st}\left({G}\right)\left({x}\right)\right)=\left({y}\in {\mathrm{Base}}_{{D}}⟼\mathrm{Id}\left({E}\right)\left({1}^{st}\left({1}^{st}\left({G}\right)\left({x}\right)\right)\left({y}\right)\right)\right)$
100 94 98 99 syl2anc ${⊢}\left({\phi }\wedge {x}\in {\mathrm{Base}}_{{C}}\right)\to \mathrm{Id}\left({E}\right)\circ {1}^{st}\left({1}^{st}\left({G}\right)\left({x}\right)\right)=\left({y}\in {\mathrm{Base}}_{{D}}⟼\mathrm{Id}\left({E}\right)\left({1}^{st}\left({1}^{st}\left({G}\right)\left({x}\right)\right)\left({y}\right)\right)\right)$
101 88 100 eqtr4d ${⊢}\left({\phi }\wedge {x}\in {\mathrm{Base}}_{{C}}\right)\to \left({y}\in {\mathrm{Base}}_{{D}}⟼\mathrm{Id}\left({C}\right)\left({x}\right)\left(⟨{x},{y}⟩{2}^{nd}\left({F}\right)⟨{x},{y}⟩\right)\mathrm{Id}\left({D}\right)\left({y}\right)\right)=\mathrm{Id}\left({E}\right)\circ {1}^{st}\left({1}^{st}\left({G}\right)\left({x}\right)\right)$
102 6 10 9 34 37 catidcl ${⊢}\left({\phi }\wedge {x}\in {\mathrm{Base}}_{{C}}\right)\to \mathrm{Id}\left({C}\right)\left({x}\right)\in \left({x}\mathrm{Hom}\left({C}\right){x}\right)$
103 eqid ${⊢}\left({x}{2}^{nd}\left({G}\right){x}\right)\left(\mathrm{Id}\left({C}\right)\left({x}\right)\right)=\left({x}{2}^{nd}\left({G}\right){x}\right)\left(\mathrm{Id}\left({C}\right)\left({x}\right)\right)$
104 1 6 34 35 36 7 10 11 37 37 102 103 curf2 ${⊢}\left({\phi }\wedge {x}\in {\mathrm{Base}}_{{C}}\right)\to \left({x}{2}^{nd}\left({G}\right){x}\right)\left(\mathrm{Id}\left({C}\right)\left({x}\right)\right)=\left({y}\in {\mathrm{Base}}_{{D}}⟼\mathrm{Id}\left({C}\right)\left({x}\right)\left(⟨{x},{y}⟩{2}^{nd}\left({F}\right)⟨{x},{y}⟩\right)\mathrm{Id}\left({D}\right)\left({y}\right)\right)$
105 2 25 66 39 fucid ${⊢}\left({\phi }\wedge {x}\in {\mathrm{Base}}_{{C}}\right)\to \mathrm{Id}\left({Q}\right)\left({1}^{st}\left({G}\right)\left({x}\right)\right)=\mathrm{Id}\left({E}\right)\circ {1}^{st}\left({1}^{st}\left({G}\right)\left({x}\right)\right)$
106 101 104 105 3eqtr4d ${⊢}\left({\phi }\wedge {x}\in {\mathrm{Base}}_{{C}}\right)\to \left({x}{2}^{nd}\left({G}\right){x}\right)\left(\mathrm{Id}\left({C}\right)\left({x}\right)\right)=\mathrm{Id}\left({Q}\right)\left({1}^{st}\left({G}\right)\left({x}\right)\right)$
107 3 3ad2ant1 ${⊢}\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\wedge {z}\in {\mathrm{Base}}_{{C}}\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}\right){y}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({C}\right){z}\right)\right)\right)\to {C}\in \mathrm{Cat}$
108 107 adantr ${⊢}\left(\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\wedge {z}\in {\mathrm{Base}}_{{C}}\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}\right){y}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({C}\right){z}\right)\right)\right)\wedge {w}\in {\mathrm{Base}}_{{D}}\right)\to {C}\in \mathrm{Cat}$
109 4 3ad2ant1 ${⊢}\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\wedge {z}\in {\mathrm{Base}}_{{C}}\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}\right){y}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({C}\right){z}\right)\right)\right)\to {D}\in \mathrm{Cat}$
110 109 adantr ${⊢}\left(\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\wedge {z}\in {\mathrm{Base}}_{{C}}\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}\right){y}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({C}\right){z}\right)\right)\right)\wedge {w}\in {\mathrm{Base}}_{{D}}\right)\to {D}\in \mathrm{Cat}$
111 5 3ad2ant1 ${⊢}\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\wedge {z}\in {\mathrm{Base}}_{{C}}\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}\right){y}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({C}\right){z}\right)\right)\right)\to {F}\in \left(\left({C}{×}_{c}{D}\right)\mathrm{Func}{E}\right)$
112 111 adantr ${⊢}\left(\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\wedge {z}\in {\mathrm{Base}}_{{C}}\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}\right){y}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({C}\right){z}\right)\right)\right)\wedge {w}\in {\mathrm{Base}}_{{D}}\right)\to {F}\in \left(\left({C}{×}_{c}{D}\right)\mathrm{Func}{E}\right)$
113 simp21 ${⊢}\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\wedge {z}\in {\mathrm{Base}}_{{C}}\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}\right){y}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({C}\right){z}\right)\right)\right)\to {x}\in {\mathrm{Base}}_{{C}}$
114 113 adantr ${⊢}\left(\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\wedge {z}\in {\mathrm{Base}}_{{C}}\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}\right){y}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({C}\right){z}\right)\right)\right)\wedge {w}\in {\mathrm{Base}}_{{D}}\right)\to {x}\in {\mathrm{Base}}_{{C}}$
115 simpr ${⊢}\left(\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\wedge {z}\in {\mathrm{Base}}_{{C}}\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}\right){y}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({C}\right){z}\right)\right)\right)\wedge {w}\in {\mathrm{Base}}_{{D}}\right)\to {w}\in {\mathrm{Base}}_{{D}}$
116 1 6 108 110 112 7 114 38 115 curf11 ${⊢}\left(\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\wedge {z}\in {\mathrm{Base}}_{{C}}\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}\right){y}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({C}\right){z}\right)\right)\right)\wedge {w}\in {\mathrm{Base}}_{{D}}\right)\to {1}^{st}\left({1}^{st}\left({G}\right)\left({x}\right)\right)\left({w}\right)={x}{1}^{st}\left({F}\right){w}$
117 df-ov ${⊢}{x}{1}^{st}\left({F}\right){w}={1}^{st}\left({F}\right)\left(⟨{x},{w}⟩\right)$
118 116 117 syl6eq ${⊢}\left(\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\wedge {z}\in {\mathrm{Base}}_{{C}}\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}\right){y}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({C}\right){z}\right)\right)\right)\wedge {w}\in {\mathrm{Base}}_{{D}}\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)$
119 simp22 ${⊢}\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\wedge {z}\in {\mathrm{Base}}_{{C}}\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}\right){y}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({C}\right){z}\right)\right)\right)\to {y}\in {\mathrm{Base}}_{{C}}$
120 119 adantr ${⊢}\left(\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\wedge {z}\in {\mathrm{Base}}_{{C}}\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}\right){y}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({C}\right){z}\right)\right)\right)\wedge {w}\in {\mathrm{Base}}_{{D}}\right)\to {y}\in {\mathrm{Base}}_{{C}}$
121 eqid ${⊢}{1}^{st}\left({G}\right)\left({y}\right)={1}^{st}\left({G}\right)\left({y}\right)$
122 1 6 108 110 112 7 120 121 115 curf11 ${⊢}\left(\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\wedge {z}\in {\mathrm{Base}}_{{C}}\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}\right){y}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({C}\right){z}\right)\right)\right)\wedge {w}\in {\mathrm{Base}}_{{D}}\right)\to {1}^{st}\left({1}^{st}\left({G}\right)\left({y}\right)\right)\left({w}\right)={y}{1}^{st}\left({F}\right){w}$
123 df-ov ${⊢}{y}{1}^{st}\left({F}\right){w}={1}^{st}\left({F}\right)\left(⟨{y},{w}⟩\right)$
124 122 123 syl6eq ${⊢}\left(\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\wedge {z}\in {\mathrm{Base}}_{{C}}\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}\right){y}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({C}\right){z}\right)\right)\right)\wedge {w}\in {\mathrm{Base}}_{{D}}\right)\to {1}^{st}\left({1}^{st}\left({G}\right)\left({y}\right)\right)\left({w}\right)={1}^{st}\left({F}\right)\left(⟨{y},{w}⟩\right)$
125 118 124 opeq12d ${⊢}\left(\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\wedge {z}\in {\mathrm{Base}}_{{C}}\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}\right){y}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({C}\right){z}\right)\right)\right)\wedge {w}\in {\mathrm{Base}}_{{D}}\right)\to ⟨{1}^{st}\left({1}^{st}\left({G}\right)\left({x}\right)\right)\left({w}\right),{1}^{st}\left({1}^{st}\left({G}\right)\left({y}\right)\right)\left({w}\right)⟩=⟨{1}^{st}\left({F}\right)\left(⟨{x},{w}⟩\right),{1}^{st}\left({F}\right)\left(⟨{y},{w}⟩\right)⟩$
126 simp23 ${⊢}\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\wedge {z}\in {\mathrm{Base}}_{{C}}\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}\right){y}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({C}\right){z}\right)\right)\right)\to {z}\in {\mathrm{Base}}_{{C}}$
127 126 adantr ${⊢}\left(\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\wedge {z}\in {\mathrm{Base}}_{{C}}\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}\right){y}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({C}\right){z}\right)\right)\right)\wedge {w}\in {\mathrm{Base}}_{{D}}\right)\to {z}\in {\mathrm{Base}}_{{C}}$
128 eqid ${⊢}{1}^{st}\left({G}\right)\left({z}\right)={1}^{st}\left({G}\right)\left({z}\right)$
129 1 6 108 110 112 7 127 128 115 curf11 ${⊢}\left(\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\wedge {z}\in {\mathrm{Base}}_{{C}}\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}\right){y}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({C}\right){z}\right)\right)\right)\wedge {w}\in {\mathrm{Base}}_{{D}}\right)\to {1}^{st}\left({1}^{st}\left({G}\right)\left({z}\right)\right)\left({w}\right)={z}{1}^{st}\left({F}\right){w}$
130 df-ov ${⊢}{z}{1}^{st}\left({F}\right){w}={1}^{st}\left({F}\right)\left(⟨{z},{w}⟩\right)$
131 129 130 syl6eq ${⊢}\left(\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\wedge {z}\in {\mathrm{Base}}_{{C}}\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}\right){y}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({C}\right){z}\right)\right)\right)\wedge {w}\in {\mathrm{Base}}_{{D}}\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)$
132 125 131 oveq12d ${⊢}\left(\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\wedge {z}\in {\mathrm{Base}}_{{C}}\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}\right){y}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({C}\right){z}\right)\right)\right)\wedge {w}\in {\mathrm{Base}}_{{D}}\right)\to ⟨{1}^{st}\left({1}^{st}\left({G}\right)\left({x}\right)\right)\left({w}\right),{1}^{st}\left({1}^{st}\left({G}\right)\left({y}\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},{w}⟩\right),{1}^{st}\left({F}\right)\left(⟨{y},{w}⟩\right)⟩\mathrm{comp}\left({E}\right){1}^{st}\left({F}\right)\left(⟨{z},{w}⟩\right)$
133 simp3r ${⊢}\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\wedge {z}\in {\mathrm{Base}}_{{C}}\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}\right){y}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({C}\right){z}\right)\right)\right)\to {g}\in \left({y}\mathrm{Hom}\left({C}\right){z}\right)$
134 133 adantr ${⊢}\left(\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\wedge {z}\in {\mathrm{Base}}_{{C}}\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}\right){y}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({C}\right){z}\right)\right)\right)\wedge {w}\in {\mathrm{Base}}_{{D}}\right)\to {g}\in \left({y}\mathrm{Hom}\left({C}\right){z}\right)$
135 eqid ${⊢}\left({y}{2}^{nd}\left({G}\right){z}\right)\left({g}\right)=\left({y}{2}^{nd}\left({G}\right){z}\right)\left({g}\right)$
136 1 6 108 110 112 7 10 11 120 127 134 135 115 curf2val ${⊢}\left(\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\wedge {z}\in {\mathrm{Base}}_{{C}}\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}\right){y}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({C}\right){z}\right)\right)\right)\wedge {w}\in {\mathrm{Base}}_{{D}}\right)\to \left({y}{2}^{nd}\left({G}\right){z}\right)\left({g}\right)\left({w}\right)={g}\left(⟨{y},{w}⟩{2}^{nd}\left({F}\right)⟨{z},{w}⟩\right)\mathrm{Id}\left({D}\right)\left({w}\right)$
137 df-ov ${⊢}{g}\left(⟨{y},{w}⟩{2}^{nd}\left({F}\right)⟨{z},{w}⟩\right)\mathrm{Id}\left({D}\right)\left({w}\right)=\left(⟨{y},{w}⟩{2}^{nd}\left({F}\right)⟨{z},{w}⟩\right)\left(⟨{g},\mathrm{Id}\left({D}\right)\left({w}\right)⟩\right)$
138 136 137 syl6eq ${⊢}\left(\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\wedge {z}\in {\mathrm{Base}}_{{C}}\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}\right){y}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({C}\right){z}\right)\right)\right)\wedge {w}\in {\mathrm{Base}}_{{D}}\right)\to \left({y}{2}^{nd}\left({G}\right){z}\right)\left({g}\right)\left({w}\right)=\left(⟨{y},{w}⟩{2}^{nd}\left({F}\right)⟨{z},{w}⟩\right)\left(⟨{g},\mathrm{Id}\left({D}\right)\left({w}\right)⟩\right)$
139 simp3l ${⊢}\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\wedge {z}\in {\mathrm{Base}}_{{C}}\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}\right){y}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({C}\right){z}\right)\right)\right)\to {f}\in \left({x}\mathrm{Hom}\left({C}\right){y}\right)$
140 139 adantr ${⊢}\left(\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\wedge {z}\in {\mathrm{Base}}_{{C}}\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}\right){y}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({C}\right){z}\right)\right)\right)\wedge {w}\in {\mathrm{Base}}_{{D}}\right)\to {f}\in \left({x}\mathrm{Hom}\left({C}\right){y}\right)$
141 eqid ${⊢}\left({x}{2}^{nd}\left({G}\right){y}\right)\left({f}\right)=\left({x}{2}^{nd}\left({G}\right){y}\right)\left({f}\right)$
142 1 6 108 110 112 7 10 11 114 120 140 141 115 curf2val ${⊢}\left(\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\wedge {z}\in {\mathrm{Base}}_{{C}}\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}\right){y}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({C}\right){z}\right)\right)\right)\wedge {w}\in {\mathrm{Base}}_{{D}}\right)\to \left({x}{2}^{nd}\left({G}\right){y}\right)\left({f}\right)\left({w}\right)={f}\left(⟨{x},{w}⟩{2}^{nd}\left({F}\right)⟨{y},{w}⟩\right)\mathrm{Id}\left({D}\right)\left({w}\right)$
143 df-ov ${⊢}{f}\left(⟨{x},{w}⟩{2}^{nd}\left({F}\right)⟨{y},{w}⟩\right)\mathrm{Id}\left({D}\right)\left({w}\right)=\left(⟨{x},{w}⟩{2}^{nd}\left({F}\right)⟨{y},{w}⟩\right)\left(⟨{f},\mathrm{Id}\left({D}\right)\left({w}\right)⟩\right)$
144 142 143 syl6eq ${⊢}\left(\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\wedge {z}\in {\mathrm{Base}}_{{C}}\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}\right){y}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({C}\right){z}\right)\right)\right)\wedge {w}\in {\mathrm{Base}}_{{D}}\right)\to \left({x}{2}^{nd}\left({G}\right){y}\right)\left({f}\right)\left({w}\right)=\left(⟨{x},{w}⟩{2}^{nd}\left({F}\right)⟨{y},{w}⟩\right)\left(⟨{f},\mathrm{Id}\left({D}\right)\left({w}\right)⟩\right)$
145 132 138 144 oveq123d ${⊢}\left(\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\wedge {z}\in {\mathrm{Base}}_{{C}}\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}\right){y}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({C}\right){z}\right)\right)\right)\wedge {w}\in {\mathrm{Base}}_{{D}}\right)\to \left({y}{2}^{nd}\left({G}\right){z}\right)\left({g}\right)\left({w}\right)\left(⟨{1}^{st}\left({1}^{st}\left({G}\right)\left({x}\right)\right)\left({w}\right),{1}^{st}\left({1}^{st}\left({G}\right)\left({y}\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({x}{2}^{nd}\left({G}\right){y}\right)\left({f}\right)\left({w}\right)=\left(⟨{y},{w}⟩{2}^{nd}\left({F}\right)⟨{z},{w}⟩\right)\left(⟨{g},\mathrm{Id}\left({D}\right)\left({w}\right)⟩\right)\left(⟨{1}^{st}\left({F}\right)\left(⟨{x},{w}⟩\right),{1}^{st}\left({F}\right)\left(⟨{y},{w}⟩\right)⟩\mathrm{comp}\left({E}\right){1}^{st}\left({F}\right)\left(⟨{z},{w}⟩\right)\right)\left(⟨{x},{w}⟩{2}^{nd}\left({F}\right)⟨{y},{w}⟩\right)\left(⟨{f},\mathrm{Id}\left({D}\right)\left({w}\right)⟩\right)$
146 eqid ${⊢}\mathrm{Hom}\left({C}{×}_{c}{D}\right)=\mathrm{Hom}\left({C}{×}_{c}{D}\right)$
147 eqid ${⊢}\mathrm{comp}\left({C}{×}_{c}{D}\right)=\mathrm{comp}\left({C}{×}_{c}{D}\right)$
148 eqid ${⊢}\mathrm{comp}\left({E}\right)=\mathrm{comp}\left({E}\right)$
149 67 112 68 sylancr ${⊢}\left(\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\wedge {z}\in {\mathrm{Base}}_{{C}}\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}\right){y}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({C}\right){z}\right)\right)\right)\wedge {w}\in {\mathrm{Base}}_{{D}}\right)\to {1}^{st}\left({F}\right)\left(\left({C}{×}_{c}{D}\right)\mathrm{Func}{E}\right){2}^{nd}\left({F}\right)$
150 opelxpi ${⊢}\left({x}\in {\mathrm{Base}}_{{C}}\wedge {w}\in {\mathrm{Base}}_{{D}}\right)\to ⟨{x},{w}⟩\in \left({\mathrm{Base}}_{{C}}×{\mathrm{Base}}_{{D}}\right)$
151 113 150 sylan ${⊢}\left(\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\wedge {z}\in {\mathrm{Base}}_{{C}}\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}\right){y}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({C}\right){z}\right)\right)\right)\wedge {w}\in {\mathrm{Base}}_{{D}}\right)\to ⟨{x},{w}⟩\in \left({\mathrm{Base}}_{{C}}×{\mathrm{Base}}_{{D}}\right)$
152 opelxpi ${⊢}\left({y}\in {\mathrm{Base}}_{{C}}\wedge {w}\in {\mathrm{Base}}_{{D}}\right)\to ⟨{y},{w}⟩\in \left({\mathrm{Base}}_{{C}}×{\mathrm{Base}}_{{D}}\right)$
153 119 152 sylan ${⊢}\left(\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\wedge {z}\in {\mathrm{Base}}_{{C}}\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}\right){y}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({C}\right){z}\right)\right)\right)\wedge {w}\in {\mathrm{Base}}_{{D}}\right)\to ⟨{y},{w}⟩\in \left({\mathrm{Base}}_{{C}}×{\mathrm{Base}}_{{D}}\right)$
154 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)$
155 126 154 sylan ${⊢}\left(\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\wedge {z}\in {\mathrm{Base}}_{{C}}\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}\right){y}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({C}\right){z}\right)\right)\right)\wedge {w}\in {\mathrm{Base}}_{{D}}\right)\to ⟨{z},{w}⟩\in \left({\mathrm{Base}}_{{C}}×{\mathrm{Base}}_{{D}}\right)$
156 7 8 11 110 115 catidcl ${⊢}\left(\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\wedge {z}\in {\mathrm{Base}}_{{C}}\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}\right){y}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({C}\right){z}\right)\right)\right)\wedge {w}\in {\mathrm{Base}}_{{D}}\right)\to \mathrm{Id}\left({D}\right)\left({w}\right)\in \left({w}\mathrm{Hom}\left({D}\right){w}\right)$
157 140 156 opelxpd ${⊢}\left(\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\wedge {z}\in {\mathrm{Base}}_{{C}}\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}\right){y}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({C}\right){z}\right)\right)\right)\wedge {w}\in {\mathrm{Base}}_{{D}}\right)\to ⟨{f},\mathrm{Id}\left({D}\right)\left({w}\right)⟩\in \left(\left({x}\mathrm{Hom}\left({C}\right){y}\right)×\left({w}\mathrm{Hom}\left({D}\right){w}\right)\right)$
158 63 6 7 10 8 114 115 120 115 146 xpchom2 ${⊢}\left(\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\wedge {z}\in {\mathrm{Base}}_{{C}}\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}\right){y}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({C}\right){z}\right)\right)\right)\wedge {w}\in {\mathrm{Base}}_{{D}}\right)\to ⟨{x},{w}⟩\mathrm{Hom}\left({C}{×}_{c}{D}\right)⟨{y},{w}⟩=\left({x}\mathrm{Hom}\left({C}\right){y}\right)×\left({w}\mathrm{Hom}\left({D}\right){w}\right)$
159 157 158 eleqtrrd ${⊢}\left(\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\wedge {z}\in {\mathrm{Base}}_{{C}}\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}\right){y}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({C}\right){z}\right)\right)\right)\wedge {w}\in {\mathrm{Base}}_{{D}}\right)\to ⟨{f},\mathrm{Id}\left({D}\right)\left({w}\right)⟩\in \left(⟨{x},{w}⟩\mathrm{Hom}\left({C}{×}_{c}{D}\right)⟨{y},{w}⟩\right)$
160 134 156 opelxpd ${⊢}\left(\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\wedge {z}\in {\mathrm{Base}}_{{C}}\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}\right){y}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({C}\right){z}\right)\right)\right)\wedge {w}\in {\mathrm{Base}}_{{D}}\right)\to ⟨{g},\mathrm{Id}\left({D}\right)\left({w}\right)⟩\in \left(\left({y}\mathrm{Hom}\left({C}\right){z}\right)×\left({w}\mathrm{Hom}\left({D}\right){w}\right)\right)$
161 63 6 7 10 8 120 115 127 115 146 xpchom2 ${⊢}\left(\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\wedge {z}\in {\mathrm{Base}}_{{C}}\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}\right){y}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({C}\right){z}\right)\right)\right)\wedge {w}\in {\mathrm{Base}}_{{D}}\right)\to ⟨{y},{w}⟩\mathrm{Hom}\left({C}{×}_{c}{D}\right)⟨{z},{w}⟩=\left({y}\mathrm{Hom}\left({C}\right){z}\right)×\left({w}\mathrm{Hom}\left({D}\right){w}\right)$
162 160 161 eleqtrrd ${⊢}\left(\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\wedge {z}\in {\mathrm{Base}}_{{C}}\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}\right){y}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({C}\right){z}\right)\right)\right)\wedge {w}\in {\mathrm{Base}}_{{D}}\right)\to ⟨{g},\mathrm{Id}\left({D}\right)\left({w}\right)⟩\in \left(⟨{y},{w}⟩\mathrm{Hom}\left({C}{×}_{c}{D}\right)⟨{z},{w}⟩\right)$
163 64 146 147 148 149 151 153 155 159 162 funcco ${⊢}\left(\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\wedge {z}\in {\mathrm{Base}}_{{C}}\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}\right){y}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({C}\right){z}\right)\right)\right)\wedge {w}\in {\mathrm{Base}}_{{D}}\right)\to \left(⟨{x},{w}⟩{2}^{nd}\left({F}\right)⟨{z},{w}⟩\right)\left(⟨{g},\mathrm{Id}\left({D}\right)\left({w}\right)⟩\left(⟨⟨{x},{w}⟩,⟨{y},{w}⟩⟩\mathrm{comp}\left({C}{×}_{c}{D}\right)⟨{z},{w}⟩\right)⟨{f},\mathrm{Id}\left({D}\right)\left({w}\right)⟩\right)=\left(⟨{y},{w}⟩{2}^{nd}\left({F}\right)⟨{z},{w}⟩\right)\left(⟨{g},\mathrm{Id}\left({D}\right)\left({w}\right)⟩\right)\left(⟨{1}^{st}\left({F}\right)\left(⟨{x},{w}⟩\right),{1}^{st}\left({F}\right)\left(⟨{y},{w}⟩\right)⟩\mathrm{comp}\left({E}\right){1}^{st}\left({F}\right)\left(⟨{z},{w}⟩\right)\right)\left(⟨{x},{w}⟩{2}^{nd}\left({F}\right)⟨{y},{w}⟩\right)\left(⟨{f},\mathrm{Id}\left({D}\right)\left({w}\right)⟩\right)$
164 eqid ${⊢}\mathrm{comp}\left({D}\right)=\mathrm{comp}\left({D}\right)$
165 63 6 7 10 8 114 115 120 115 26 164 147 127 115 140 156 134 156 xpcco2 ${⊢}\left(\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\wedge {z}\in {\mathrm{Base}}_{{C}}\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}\right){y}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({C}\right){z}\right)\right)\right)\wedge {w}\in {\mathrm{Base}}_{{D}}\right)\to ⟨{g},\mathrm{Id}\left({D}\right)\left({w}\right)⟩\left(⟨⟨{x},{w}⟩,⟨{y},{w}⟩⟩\mathrm{comp}\left({C}{×}_{c}{D}\right)⟨{z},{w}⟩\right)⟨{f},\mathrm{Id}\left({D}\right)\left({w}\right)⟩=⟨{g}\left(⟨{x},{y}⟩\mathrm{comp}\left({C}\right){z}\right){f},\mathrm{Id}\left({D}\right)\left({w}\right)\left(⟨{w},{w}⟩\mathrm{comp}\left({D}\right){w}\right)\mathrm{Id}\left({D}\right)\left({w}\right)⟩$
166 7 8 11 110 115 164 115 156 catlid ${⊢}\left(\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\wedge {z}\in {\mathrm{Base}}_{{C}}\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}\right){y}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({C}\right){z}\right)\right)\right)\wedge {w}\in {\mathrm{Base}}_{{D}}\right)\to \mathrm{Id}\left({D}\right)\left({w}\right)\left(⟨{w},{w}⟩\mathrm{comp}\left({D}\right){w}\right)\mathrm{Id}\left({D}\right)\left({w}\right)=\mathrm{Id}\left({D}\right)\left({w}\right)$
167 166 opeq2d ${⊢}\left(\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\wedge {z}\in {\mathrm{Base}}_{{C}}\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}\right){y}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({C}\right){z}\right)\right)\right)\wedge {w}\in {\mathrm{Base}}_{{D}}\right)\to ⟨{g}\left(⟨{x},{y}⟩\mathrm{comp}\left({C}\right){z}\right){f},\mathrm{Id}\left({D}\right)\left({w}\right)\left(⟨{w},{w}⟩\mathrm{comp}\left({D}\right){w}\right)\mathrm{Id}\left({D}\right)\left({w}\right)⟩=⟨{g}\left(⟨{x},{y}⟩\mathrm{comp}\left({C}\right){z}\right){f},\mathrm{Id}\left({D}\right)\left({w}\right)⟩$
168 165 167 eqtrd ${⊢}\left(\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\wedge {z}\in {\mathrm{Base}}_{{C}}\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}\right){y}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({C}\right){z}\right)\right)\right)\wedge {w}\in {\mathrm{Base}}_{{D}}\right)\to ⟨{g},\mathrm{Id}\left({D}\right)\left({w}\right)⟩\left(⟨⟨{x},{w}⟩,⟨{y},{w}⟩⟩\mathrm{comp}\left({C}{×}_{c}{D}\right)⟨{z},{w}⟩\right)⟨{f},\mathrm{Id}\left({D}\right)\left({w}\right)⟩=⟨{g}\left(⟨{x},{y}⟩\mathrm{comp}\left({C}\right){z}\right){f},\mathrm{Id}\left({D}\right)\left({w}\right)⟩$
169 168 fveq2d ${⊢}\left(\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\wedge {z}\in {\mathrm{Base}}_{{C}}\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}\right){y}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({C}\right){z}\right)\right)\right)\wedge {w}\in {\mathrm{Base}}_{{D}}\right)\to \left(⟨{x},{w}⟩{2}^{nd}\left({F}\right)⟨{z},{w}⟩\right)\left(⟨{g},\mathrm{Id}\left({D}\right)\left({w}\right)⟩\left(⟨⟨{x},{w}⟩,⟨{y},{w}⟩⟩\mathrm{comp}\left({C}{×}_{c}{D}\right)⟨{z},{w}⟩\right)⟨{f},\mathrm{Id}\left({D}\right)\left({w}\right)⟩\right)=\left(⟨{x},{w}⟩{2}^{nd}\left({F}\right)⟨{z},{w}⟩\right)\left(⟨{g}\left(⟨{x},{y}⟩\mathrm{comp}\left({C}\right){z}\right){f},\mathrm{Id}\left({D}\right)\left({w}\right)⟩\right)$
170 df-ov ${⊢}\left({g}\left(⟨{x},{y}⟩\mathrm{comp}\left({C}\right){z}\right){f}\right)\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(⟨{g}\left(⟨{x},{y}⟩\mathrm{comp}\left({C}\right){z}\right){f},\mathrm{Id}\left({D}\right)\left({w}\right)⟩\right)$
171 169 170 syl6eqr ${⊢}\left(\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\wedge {z}\in {\mathrm{Base}}_{{C}}\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}\right){y}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({C}\right){z}\right)\right)\right)\wedge {w}\in {\mathrm{Base}}_{{D}}\right)\to \left(⟨{x},{w}⟩{2}^{nd}\left({F}\right)⟨{z},{w}⟩\right)\left(⟨{g},\mathrm{Id}\left({D}\right)\left({w}\right)⟩\left(⟨⟨{x},{w}⟩,⟨{y},{w}⟩⟩\mathrm{comp}\left({C}{×}_{c}{D}\right)⟨{z},{w}⟩\right)⟨{f},\mathrm{Id}\left({D}\right)\left({w}\right)⟩\right)=\left({g}\left(⟨{x},{y}⟩\mathrm{comp}\left({C}\right){z}\right){f}\right)\left(⟨{x},{w}⟩{2}^{nd}\left({F}\right)⟨{z},{w}⟩\right)\mathrm{Id}\left({D}\right)\left({w}\right)$
172 145 163 171 3eqtr2rd ${⊢}\left(\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\wedge {z}\in {\mathrm{Base}}_{{C}}\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}\right){y}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({C}\right){z}\right)\right)\right)\wedge {w}\in {\mathrm{Base}}_{{D}}\right)\to \left({g}\left(⟨{x},{y}⟩\mathrm{comp}\left({C}\right){z}\right){f}\right)\left(⟨{x},{w}⟩{2}^{nd}\left({F}\right)⟨{z},{w}⟩\right)\mathrm{Id}\left({D}\right)\left({w}\right)=\left({y}{2}^{nd}\left({G}\right){z}\right)\left({g}\right)\left({w}\right)\left(⟨{1}^{st}\left({1}^{st}\left({G}\right)\left({x}\right)\right)\left({w}\right),{1}^{st}\left({1}^{st}\left({G}\right)\left({y}\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({x}{2}^{nd}\left({G}\right){y}\right)\left({f}\right)\left({w}\right)$
173 172 mpteq2dva ${⊢}\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\wedge {z}\in {\mathrm{Base}}_{{C}}\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}\right){y}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({C}\right){z}\right)\right)\right)\to \left({w}\in {\mathrm{Base}}_{{D}}⟼\left({g}\left(⟨{x},{y}⟩\mathrm{comp}\left({C}\right){z}\right){f}\right)\left(⟨{x},{w}⟩{2}^{nd}\left({F}\right)⟨{z},{w}⟩\right)\mathrm{Id}\left({D}\right)\left({w}\right)\right)=\left({w}\in {\mathrm{Base}}_{{D}}⟼\left({y}{2}^{nd}\left({G}\right){z}\right)\left({g}\right)\left({w}\right)\left(⟨{1}^{st}\left({1}^{st}\left({G}\right)\left({x}\right)\right)\left({w}\right),{1}^{st}\left({1}^{st}\left({G}\right)\left({y}\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({x}{2}^{nd}\left({G}\right){y}\right)\left({f}\right)\left({w}\right)\right)$
174 6 10 26 107 113 119 126 139 133 catcocl ${⊢}\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\wedge {z}\in {\mathrm{Base}}_{{C}}\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}\right){y}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({C}\right){z}\right)\right)\right)\to {g}\left(⟨{x},{y}⟩\mathrm{comp}\left({C}\right){z}\right){f}\in \left({x}\mathrm{Hom}\left({C}\right){z}\right)$
175 eqid ${⊢}\left({x}{2}^{nd}\left({G}\right){z}\right)\left({g}\left(⟨{x},{y}⟩\mathrm{comp}\left({C}\right){z}\right){f}\right)=\left({x}{2}^{nd}\left({G}\right){z}\right)\left({g}\left(⟨{x},{y}⟩\mathrm{comp}\left({C}\right){z}\right){f}\right)$
176 1 6 107 109 111 7 10 11 113 126 174 175 curf2 ${⊢}\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\wedge {z}\in {\mathrm{Base}}_{{C}}\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}\right){y}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({C}\right){z}\right)\right)\right)\to \left({x}{2}^{nd}\left({G}\right){z}\right)\left({g}\left(⟨{x},{y}⟩\mathrm{comp}\left({C}\right){z}\right){f}\right)=\left({w}\in {\mathrm{Base}}_{{D}}⟼\left({g}\left(⟨{x},{y}⟩\mathrm{comp}\left({C}\right){z}\right){f}\right)\left(⟨{x},{w}⟩{2}^{nd}\left({F}\right)⟨{z},{w}⟩\right)\mathrm{Id}\left({D}\right)\left({w}\right)\right)$
177 1 6 107 109 111 7 10 11 113 119 139 141 23 curf2cl ${⊢}\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\wedge {z}\in {\mathrm{Base}}_{{C}}\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}\right){y}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({C}\right){z}\right)\right)\right)\to \left({x}{2}^{nd}\left({G}\right){y}\right)\left({f}\right)\in \left({1}^{st}\left({G}\right)\left({x}\right)\left({D}\mathrm{Nat}{E}\right){1}^{st}\left({G}\right)\left({y}\right)\right)$
178 1 6 107 109 111 7 10 11 119 126 133 135 23 curf2cl ${⊢}\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\wedge {z}\in {\mathrm{Base}}_{{C}}\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}\right){y}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({C}\right){z}\right)\right)\right)\to \left({y}{2}^{nd}\left({G}\right){z}\right)\left({g}\right)\in \left({1}^{st}\left({G}\right)\left({y}\right)\left({D}\mathrm{Nat}{E}\right){1}^{st}\left({G}\right)\left({z}\right)\right)$
179 2 23 7 148 27 177 178 fucco ${⊢}\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\wedge {z}\in {\mathrm{Base}}_{{C}}\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}\right){y}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({C}\right){z}\right)\right)\right)\to \left({y}{2}^{nd}\left({G}\right){z}\right)\left({g}\right)\left(⟨{1}^{st}\left({G}\right)\left({x}\right),{1}^{st}\left({G}\right)\left({y}\right)⟩\mathrm{comp}\left({Q}\right){1}^{st}\left({G}\right)\left({z}\right)\right)\left({x}{2}^{nd}\left({G}\right){y}\right)\left({f}\right)=\left({w}\in {\mathrm{Base}}_{{D}}⟼\left({y}{2}^{nd}\left({G}\right){z}\right)\left({g}\right)\left({w}\right)\left(⟨{1}^{st}\left({1}^{st}\left({G}\right)\left({x}\right)\right)\left({w}\right),{1}^{st}\left({1}^{st}\left({G}\right)\left({y}\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({x}{2}^{nd}\left({G}\right){y}\right)\left({f}\right)\left({w}\right)\right)$
180 173 176 179 3eqtr4d ${⊢}\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\wedge {z}\in {\mathrm{Base}}_{{C}}\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}\right){y}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({C}\right){z}\right)\right)\right)\to \left({x}{2}^{nd}\left({G}\right){z}\right)\left({g}\left(⟨{x},{y}⟩\mathrm{comp}\left({C}\right){z}\right){f}\right)=\left({y}{2}^{nd}\left({G}\right){z}\right)\left({g}\right)\left(⟨{1}^{st}\left({G}\right)\left({x}\right),{1}^{st}\left({G}\right)\left({y}\right)⟩\mathrm{comp}\left({Q}\right){1}^{st}\left({G}\right)\left({z}\right)\right)\left({x}{2}^{nd}\left({G}\right){y}\right)\left({f}\right)$
181 6 22 10 24 9 25 26 27 3 31 40 46 62 106 180 isfuncd ${⊢}{\phi }\to {1}^{st}\left({G}\right)\left({C}\mathrm{Func}{Q}\right){2}^{nd}\left({G}\right)$
182 df-br ${⊢}{1}^{st}\left({G}\right)\left({C}\mathrm{Func}{Q}\right){2}^{nd}\left({G}\right)↔⟨{1}^{st}\left({G}\right),{2}^{nd}\left({G}\right)⟩\in \left({C}\mathrm{Func}{Q}\right)$
183 181 182 sylib ${⊢}{\phi }\to ⟨{1}^{st}\left({G}\right),{2}^{nd}\left({G}\right)⟩\in \left({C}\mathrm{Func}{Q}\right)$
184 21 183 eqeltrd ${⊢}{\phi }\to {G}\in \left({C}\mathrm{Func}{Q}\right)$