# Metamath Proof Explorer

## Theorem cofucl

Description: The composition of two functors is a functor. Proposition 3.23 of Adamek p. 33. (Contributed by Mario Carneiro, 3-Jan-2017)

Ref Expression
Hypotheses cofucl.f ${⊢}{\phi }\to {F}\in \left({C}\mathrm{Func}{D}\right)$
cofucl.g ${⊢}{\phi }\to {G}\in \left({D}\mathrm{Func}{E}\right)$
Assertion cofucl ${⊢}{\phi }\to {G}{\circ }_{\mathrm{func}}{F}\in \left({C}\mathrm{Func}{E}\right)$

### Proof

Step Hyp Ref Expression
1 cofucl.f ${⊢}{\phi }\to {F}\in \left({C}\mathrm{Func}{D}\right)$
2 cofucl.g ${⊢}{\phi }\to {G}\in \left({D}\mathrm{Func}{E}\right)$
3 eqid ${⊢}{\mathrm{Base}}_{{C}}={\mathrm{Base}}_{{C}}$
4 3 1 2 cofuval ${⊢}{\phi }\to {G}{\circ }_{\mathrm{func}}{F}=⟨{1}^{st}\left({G}\right)\circ {1}^{st}\left({F}\right),\left({x}\in {\mathrm{Base}}_{{C}},{y}\in {\mathrm{Base}}_{{C}}⟼\left({1}^{st}\left({F}\right)\left({x}\right){2}^{nd}\left({G}\right){1}^{st}\left({F}\right)\left({y}\right)\right)\circ \left({x}{2}^{nd}\left({F}\right){y}\right)\right)⟩$
5 3 1 2 cofu1st ${⊢}{\phi }\to {1}^{st}\left({G}{\circ }_{\mathrm{func}}{F}\right)={1}^{st}\left({G}\right)\circ {1}^{st}\left({F}\right)$
6 4 fveq2d ${⊢}{\phi }\to {2}^{nd}\left({G}{\circ }_{\mathrm{func}}{F}\right)={2}^{nd}\left(⟨{1}^{st}\left({G}\right)\circ {1}^{st}\left({F}\right),\left({x}\in {\mathrm{Base}}_{{C}},{y}\in {\mathrm{Base}}_{{C}}⟼\left({1}^{st}\left({F}\right)\left({x}\right){2}^{nd}\left({G}\right){1}^{st}\left({F}\right)\left({y}\right)\right)\circ \left({x}{2}^{nd}\left({F}\right){y}\right)\right)⟩\right)$
7 fvex ${⊢}{1}^{st}\left({G}\right)\in \mathrm{V}$
8 fvex ${⊢}{1}^{st}\left({F}\right)\in \mathrm{V}$
9 7 8 coex ${⊢}{1}^{st}\left({G}\right)\circ {1}^{st}\left({F}\right)\in \mathrm{V}$
10 fvex ${⊢}{\mathrm{Base}}_{{C}}\in \mathrm{V}$
11 10 10 mpoex ${⊢}\left({x}\in {\mathrm{Base}}_{{C}},{y}\in {\mathrm{Base}}_{{C}}⟼\left({1}^{st}\left({F}\right)\left({x}\right){2}^{nd}\left({G}\right){1}^{st}\left({F}\right)\left({y}\right)\right)\circ \left({x}{2}^{nd}\left({F}\right){y}\right)\right)\in \mathrm{V}$
12 9 11 op2nd ${⊢}{2}^{nd}\left(⟨{1}^{st}\left({G}\right)\circ {1}^{st}\left({F}\right),\left({x}\in {\mathrm{Base}}_{{C}},{y}\in {\mathrm{Base}}_{{C}}⟼\left({1}^{st}\left({F}\right)\left({x}\right){2}^{nd}\left({G}\right){1}^{st}\left({F}\right)\left({y}\right)\right)\circ \left({x}{2}^{nd}\left({F}\right){y}\right)\right)⟩\right)=\left({x}\in {\mathrm{Base}}_{{C}},{y}\in {\mathrm{Base}}_{{C}}⟼\left({1}^{st}\left({F}\right)\left({x}\right){2}^{nd}\left({G}\right){1}^{st}\left({F}\right)\left({y}\right)\right)\circ \left({x}{2}^{nd}\left({F}\right){y}\right)\right)$
13 6 12 syl6eq ${⊢}{\phi }\to {2}^{nd}\left({G}{\circ }_{\mathrm{func}}{F}\right)=\left({x}\in {\mathrm{Base}}_{{C}},{y}\in {\mathrm{Base}}_{{C}}⟼\left({1}^{st}\left({F}\right)\left({x}\right){2}^{nd}\left({G}\right){1}^{st}\left({F}\right)\left({y}\right)\right)\circ \left({x}{2}^{nd}\left({F}\right){y}\right)\right)$
14 5 13 opeq12d ${⊢}{\phi }\to ⟨{1}^{st}\left({G}{\circ }_{\mathrm{func}}{F}\right),{2}^{nd}\left({G}{\circ }_{\mathrm{func}}{F}\right)⟩=⟨{1}^{st}\left({G}\right)\circ {1}^{st}\left({F}\right),\left({x}\in {\mathrm{Base}}_{{C}},{y}\in {\mathrm{Base}}_{{C}}⟼\left({1}^{st}\left({F}\right)\left({x}\right){2}^{nd}\left({G}\right){1}^{st}\left({F}\right)\left({y}\right)\right)\circ \left({x}{2}^{nd}\left({F}\right){y}\right)\right)⟩$
15 4 14 eqtr4d ${⊢}{\phi }\to {G}{\circ }_{\mathrm{func}}{F}=⟨{1}^{st}\left({G}{\circ }_{\mathrm{func}}{F}\right),{2}^{nd}\left({G}{\circ }_{\mathrm{func}}{F}\right)⟩$
16 eqid ${⊢}{\mathrm{Base}}_{{D}}={\mathrm{Base}}_{{D}}$
17 eqid ${⊢}{\mathrm{Base}}_{{E}}={\mathrm{Base}}_{{E}}$
18 relfunc ${⊢}\mathrm{Rel}\left({D}\mathrm{Func}{E}\right)$
19 1st2ndbr ${⊢}\left(\mathrm{Rel}\left({D}\mathrm{Func}{E}\right)\wedge {G}\in \left({D}\mathrm{Func}{E}\right)\right)\to {1}^{st}\left({G}\right)\left({D}\mathrm{Func}{E}\right){2}^{nd}\left({G}\right)$
20 18 2 19 sylancr ${⊢}{\phi }\to {1}^{st}\left({G}\right)\left({D}\mathrm{Func}{E}\right){2}^{nd}\left({G}\right)$
21 16 17 20 funcf1 ${⊢}{\phi }\to {1}^{st}\left({G}\right):{\mathrm{Base}}_{{D}}⟶{\mathrm{Base}}_{{E}}$
22 relfunc ${⊢}\mathrm{Rel}\left({C}\mathrm{Func}{D}\right)$
23 1st2ndbr ${⊢}\left(\mathrm{Rel}\left({C}\mathrm{Func}{D}\right)\wedge {F}\in \left({C}\mathrm{Func}{D}\right)\right)\to {1}^{st}\left({F}\right)\left({C}\mathrm{Func}{D}\right){2}^{nd}\left({F}\right)$
24 22 1 23 sylancr ${⊢}{\phi }\to {1}^{st}\left({F}\right)\left({C}\mathrm{Func}{D}\right){2}^{nd}\left({F}\right)$
25 3 16 24 funcf1 ${⊢}{\phi }\to {1}^{st}\left({F}\right):{\mathrm{Base}}_{{C}}⟶{\mathrm{Base}}_{{D}}$
26 fco ${⊢}\left({1}^{st}\left({G}\right):{\mathrm{Base}}_{{D}}⟶{\mathrm{Base}}_{{E}}\wedge {1}^{st}\left({F}\right):{\mathrm{Base}}_{{C}}⟶{\mathrm{Base}}_{{D}}\right)\to \left({1}^{st}\left({G}\right)\circ {1}^{st}\left({F}\right)\right):{\mathrm{Base}}_{{C}}⟶{\mathrm{Base}}_{{E}}$
27 21 25 26 syl2anc ${⊢}{\phi }\to \left({1}^{st}\left({G}\right)\circ {1}^{st}\left({F}\right)\right):{\mathrm{Base}}_{{C}}⟶{\mathrm{Base}}_{{E}}$
28 5 feq1d ${⊢}{\phi }\to \left({1}^{st}\left({G}{\circ }_{\mathrm{func}}{F}\right):{\mathrm{Base}}_{{C}}⟶{\mathrm{Base}}_{{E}}↔\left({1}^{st}\left({G}\right)\circ {1}^{st}\left({F}\right)\right):{\mathrm{Base}}_{{C}}⟶{\mathrm{Base}}_{{E}}\right)$
29 27 28 mpbird ${⊢}{\phi }\to {1}^{st}\left({G}{\circ }_{\mathrm{func}}{F}\right):{\mathrm{Base}}_{{C}}⟶{\mathrm{Base}}_{{E}}$
30 eqid ${⊢}\left({x}\in {\mathrm{Base}}_{{C}},{y}\in {\mathrm{Base}}_{{C}}⟼\left({1}^{st}\left({F}\right)\left({x}\right){2}^{nd}\left({G}\right){1}^{st}\left({F}\right)\left({y}\right)\right)\circ \left({x}{2}^{nd}\left({F}\right){y}\right)\right)=\left({x}\in {\mathrm{Base}}_{{C}},{y}\in {\mathrm{Base}}_{{C}}⟼\left({1}^{st}\left({F}\right)\left({x}\right){2}^{nd}\left({G}\right){1}^{st}\left({F}\right)\left({y}\right)\right)\circ \left({x}{2}^{nd}\left({F}\right){y}\right)\right)$
31 ovex ${⊢}{1}^{st}\left({F}\right)\left({x}\right){2}^{nd}\left({G}\right){1}^{st}\left({F}\right)\left({y}\right)\in \mathrm{V}$
32 ovex ${⊢}{x}{2}^{nd}\left({F}\right){y}\in \mathrm{V}$
33 31 32 coex ${⊢}\left({1}^{st}\left({F}\right)\left({x}\right){2}^{nd}\left({G}\right){1}^{st}\left({F}\right)\left({y}\right)\right)\circ \left({x}{2}^{nd}\left({F}\right){y}\right)\in \mathrm{V}$
34 30 33 fnmpoi ${⊢}\left({x}\in {\mathrm{Base}}_{{C}},{y}\in {\mathrm{Base}}_{{C}}⟼\left({1}^{st}\left({F}\right)\left({x}\right){2}^{nd}\left({G}\right){1}^{st}\left({F}\right)\left({y}\right)\right)\circ \left({x}{2}^{nd}\left({F}\right){y}\right)\right)Fn\left({\mathrm{Base}}_{{C}}×{\mathrm{Base}}_{{C}}\right)$
35 13 fneq1d ${⊢}{\phi }\to \left({2}^{nd}\left({G}{\circ }_{\mathrm{func}}{F}\right)Fn\left({\mathrm{Base}}_{{C}}×{\mathrm{Base}}_{{C}}\right)↔\left({x}\in {\mathrm{Base}}_{{C}},{y}\in {\mathrm{Base}}_{{C}}⟼\left({1}^{st}\left({F}\right)\left({x}\right){2}^{nd}\left({G}\right){1}^{st}\left({F}\right)\left({y}\right)\right)\circ \left({x}{2}^{nd}\left({F}\right){y}\right)\right)Fn\left({\mathrm{Base}}_{{C}}×{\mathrm{Base}}_{{C}}\right)\right)$
36 34 35 mpbiri ${⊢}{\phi }\to {2}^{nd}\left({G}{\circ }_{\mathrm{func}}{F}\right)Fn\left({\mathrm{Base}}_{{C}}×{\mathrm{Base}}_{{C}}\right)$
37 eqid ${⊢}\mathrm{Hom}\left({D}\right)=\mathrm{Hom}\left({D}\right)$
38 eqid ${⊢}\mathrm{Hom}\left({E}\right)=\mathrm{Hom}\left({E}\right)$
39 20 adantr ${⊢}\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\right)\right)\to {1}^{st}\left({G}\right)\left({D}\mathrm{Func}{E}\right){2}^{nd}\left({G}\right)$
40 25 adantr ${⊢}\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\right)\right)\to {1}^{st}\left({F}\right):{\mathrm{Base}}_{{C}}⟶{\mathrm{Base}}_{{D}}$
41 simprl ${⊢}\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\right)\right)\to {x}\in {\mathrm{Base}}_{{C}}$
42 40 41 ffvelrnd ${⊢}\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\right)\right)\to {1}^{st}\left({F}\right)\left({x}\right)\in {\mathrm{Base}}_{{D}}$
43 simprr ${⊢}\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\right)\right)\to {y}\in {\mathrm{Base}}_{{C}}$
44 40 43 ffvelrnd ${⊢}\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\right)\right)\to {1}^{st}\left({F}\right)\left({y}\right)\in {\mathrm{Base}}_{{D}}$
45 16 37 38 39 42 44 funcf2 ${⊢}\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\right)\right)\to \left({1}^{st}\left({F}\right)\left({x}\right){2}^{nd}\left({G}\right){1}^{st}\left({F}\right)\left({y}\right)\right):{1}^{st}\left({F}\right)\left({x}\right)\mathrm{Hom}\left({D}\right){1}^{st}\left({F}\right)\left({y}\right)⟶{1}^{st}\left({G}\right)\left({1}^{st}\left({F}\right)\left({x}\right)\right)\mathrm{Hom}\left({E}\right){1}^{st}\left({G}\right)\left({1}^{st}\left({F}\right)\left({y}\right)\right)$
46 eqid ${⊢}\mathrm{Hom}\left({C}\right)=\mathrm{Hom}\left({C}\right)$
47 24 adantr ${⊢}\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\right)\right)\to {1}^{st}\left({F}\right)\left({C}\mathrm{Func}{D}\right){2}^{nd}\left({F}\right)$
48 3 46 37 47 41 43 funcf2 ${⊢}\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\right)\right)\to \left({x}{2}^{nd}\left({F}\right){y}\right):{x}\mathrm{Hom}\left({C}\right){y}⟶{1}^{st}\left({F}\right)\left({x}\right)\mathrm{Hom}\left({D}\right){1}^{st}\left({F}\right)\left({y}\right)$
49 fco ${⊢}\left(\left({1}^{st}\left({F}\right)\left({x}\right){2}^{nd}\left({G}\right){1}^{st}\left({F}\right)\left({y}\right)\right):{1}^{st}\left({F}\right)\left({x}\right)\mathrm{Hom}\left({D}\right){1}^{st}\left({F}\right)\left({y}\right)⟶{1}^{st}\left({G}\right)\left({1}^{st}\left({F}\right)\left({x}\right)\right)\mathrm{Hom}\left({E}\right){1}^{st}\left({G}\right)\left({1}^{st}\left({F}\right)\left({y}\right)\right)\wedge \left({x}{2}^{nd}\left({F}\right){y}\right):{x}\mathrm{Hom}\left({C}\right){y}⟶{1}^{st}\left({F}\right)\left({x}\right)\mathrm{Hom}\left({D}\right){1}^{st}\left({F}\right)\left({y}\right)\right)\to \left(\left({1}^{st}\left({F}\right)\left({x}\right){2}^{nd}\left({G}\right){1}^{st}\left({F}\right)\left({y}\right)\right)\circ \left({x}{2}^{nd}\left({F}\right){y}\right)\right):{x}\mathrm{Hom}\left({C}\right){y}⟶{1}^{st}\left({G}\right)\left({1}^{st}\left({F}\right)\left({x}\right)\right)\mathrm{Hom}\left({E}\right){1}^{st}\left({G}\right)\left({1}^{st}\left({F}\right)\left({y}\right)\right)$
50 45 48 49 syl2anc ${⊢}\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\right)\right)\to \left(\left({1}^{st}\left({F}\right)\left({x}\right){2}^{nd}\left({G}\right){1}^{st}\left({F}\right)\left({y}\right)\right)\circ \left({x}{2}^{nd}\left({F}\right){y}\right)\right):{x}\mathrm{Hom}\left({C}\right){y}⟶{1}^{st}\left({G}\right)\left({1}^{st}\left({F}\right)\left({x}\right)\right)\mathrm{Hom}\left({E}\right){1}^{st}\left({G}\right)\left({1}^{st}\left({F}\right)\left({y}\right)\right)$
51 ovex ${⊢}{1}^{st}\left({G}\right)\left({1}^{st}\left({F}\right)\left({x}\right)\right)\mathrm{Hom}\left({E}\right){1}^{st}\left({G}\right)\left({1}^{st}\left({F}\right)\left({y}\right)\right)\in \mathrm{V}$
52 ovex ${⊢}{x}\mathrm{Hom}\left({C}\right){y}\in \mathrm{V}$
53 51 52 elmap ${⊢}\left({1}^{st}\left({F}\right)\left({x}\right){2}^{nd}\left({G}\right){1}^{st}\left({F}\right)\left({y}\right)\right)\circ \left({x}{2}^{nd}\left({F}\right){y}\right)\in \left({\left({1}^{st}\left({G}\right)\left({1}^{st}\left({F}\right)\left({x}\right)\right)\mathrm{Hom}\left({E}\right){1}^{st}\left({G}\right)\left({1}^{st}\left({F}\right)\left({y}\right)\right)\right)}^{\left({x}\mathrm{Hom}\left({C}\right){y}\right)}\right)↔\left(\left({1}^{st}\left({F}\right)\left({x}\right){2}^{nd}\left({G}\right){1}^{st}\left({F}\right)\left({y}\right)\right)\circ \left({x}{2}^{nd}\left({F}\right){y}\right)\right):{x}\mathrm{Hom}\left({C}\right){y}⟶{1}^{st}\left({G}\right)\left({1}^{st}\left({F}\right)\left({x}\right)\right)\mathrm{Hom}\left({E}\right){1}^{st}\left({G}\right)\left({1}^{st}\left({F}\right)\left({y}\right)\right)$
54 50 53 sylibr ${⊢}\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\right)\right)\to \left({1}^{st}\left({F}\right)\left({x}\right){2}^{nd}\left({G}\right){1}^{st}\left({F}\right)\left({y}\right)\right)\circ \left({x}{2}^{nd}\left({F}\right){y}\right)\in \left({\left({1}^{st}\left({G}\right)\left({1}^{st}\left({F}\right)\left({x}\right)\right)\mathrm{Hom}\left({E}\right){1}^{st}\left({G}\right)\left({1}^{st}\left({F}\right)\left({y}\right)\right)\right)}^{\left({x}\mathrm{Hom}\left({C}\right){y}\right)}\right)$
55 1 adantr ${⊢}\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\right)\right)\to {F}\in \left({C}\mathrm{Func}{D}\right)$
56 2 adantr ${⊢}\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\right)\right)\to {G}\in \left({D}\mathrm{Func}{E}\right)$
57 3 55 56 41 43 cofu2nd ${⊢}\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\right)\right)\to {x}{2}^{nd}\left({G}{\circ }_{\mathrm{func}}{F}\right){y}=\left({1}^{st}\left({F}\right)\left({x}\right){2}^{nd}\left({G}\right){1}^{st}\left({F}\right)\left({y}\right)\right)\circ \left({x}{2}^{nd}\left({F}\right){y}\right)$
58 3 55 56 41 cofu1 ${⊢}\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\right)\right)\to {1}^{st}\left({G}{\circ }_{\mathrm{func}}{F}\right)\left({x}\right)={1}^{st}\left({G}\right)\left({1}^{st}\left({F}\right)\left({x}\right)\right)$
59 3 55 56 43 cofu1 ${⊢}\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\right)\right)\to {1}^{st}\left({G}{\circ }_{\mathrm{func}}{F}\right)\left({y}\right)={1}^{st}\left({G}\right)\left({1}^{st}\left({F}\right)\left({y}\right)\right)$
60 58 59 oveq12d ${⊢}\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\right)\right)\to {1}^{st}\left({G}{\circ }_{\mathrm{func}}{F}\right)\left({x}\right)\mathrm{Hom}\left({E}\right){1}^{st}\left({G}{\circ }_{\mathrm{func}}{F}\right)\left({y}\right)={1}^{st}\left({G}\right)\left({1}^{st}\left({F}\right)\left({x}\right)\right)\mathrm{Hom}\left({E}\right){1}^{st}\left({G}\right)\left({1}^{st}\left({F}\right)\left({y}\right)\right)$
61 60 oveq1d ${⊢}\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\right)\right)\to {\left({1}^{st}\left({G}{\circ }_{\mathrm{func}}{F}\right)\left({x}\right)\mathrm{Hom}\left({E}\right){1}^{st}\left({G}{\circ }_{\mathrm{func}}{F}\right)\left({y}\right)\right)}^{\left({x}\mathrm{Hom}\left({C}\right){y}\right)}={\left({1}^{st}\left({G}\right)\left({1}^{st}\left({F}\right)\left({x}\right)\right)\mathrm{Hom}\left({E}\right){1}^{st}\left({G}\right)\left({1}^{st}\left({F}\right)\left({y}\right)\right)\right)}^{\left({x}\mathrm{Hom}\left({C}\right){y}\right)}$
62 54 57 61 3eltr4d ${⊢}\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\right)\right)\to {x}{2}^{nd}\left({G}{\circ }_{\mathrm{func}}{F}\right){y}\in \left({\left({1}^{st}\left({G}{\circ }_{\mathrm{func}}{F}\right)\left({x}\right)\mathrm{Hom}\left({E}\right){1}^{st}\left({G}{\circ }_{\mathrm{func}}{F}\right)\left({y}\right)\right)}^{\left({x}\mathrm{Hom}\left({C}\right){y}\right)}\right)$
63 62 ralrimivva ${⊢}{\phi }\to \forall {x}\in {\mathrm{Base}}_{{C}}\phantom{\rule{.4em}{0ex}}\forall {y}\in {\mathrm{Base}}_{{C}}\phantom{\rule{.4em}{0ex}}{x}{2}^{nd}\left({G}{\circ }_{\mathrm{func}}{F}\right){y}\in \left({\left({1}^{st}\left({G}{\circ }_{\mathrm{func}}{F}\right)\left({x}\right)\mathrm{Hom}\left({E}\right){1}^{st}\left({G}{\circ }_{\mathrm{func}}{F}\right)\left({y}\right)\right)}^{\left({x}\mathrm{Hom}\left({C}\right){y}\right)}\right)$
64 fveq2 ${⊢}{z}=⟨{x},{y}⟩\to {2}^{nd}\left({G}{\circ }_{\mathrm{func}}{F}\right)\left({z}\right)={2}^{nd}\left({G}{\circ }_{\mathrm{func}}{F}\right)\left(⟨{x},{y}⟩\right)$
65 df-ov ${⊢}{x}{2}^{nd}\left({G}{\circ }_{\mathrm{func}}{F}\right){y}={2}^{nd}\left({G}{\circ }_{\mathrm{func}}{F}\right)\left(⟨{x},{y}⟩\right)$
66 64 65 syl6eqr ${⊢}{z}=⟨{x},{y}⟩\to {2}^{nd}\left({G}{\circ }_{\mathrm{func}}{F}\right)\left({z}\right)={x}{2}^{nd}\left({G}{\circ }_{\mathrm{func}}{F}\right){y}$
67 vex ${⊢}{x}\in \mathrm{V}$
68 vex ${⊢}{y}\in \mathrm{V}$
69 67 68 op1std ${⊢}{z}=⟨{x},{y}⟩\to {1}^{st}\left({z}\right)={x}$
70 69 fveq2d ${⊢}{z}=⟨{x},{y}⟩\to {1}^{st}\left({G}{\circ }_{\mathrm{func}}{F}\right)\left({1}^{st}\left({z}\right)\right)={1}^{st}\left({G}{\circ }_{\mathrm{func}}{F}\right)\left({x}\right)$
71 67 68 op2ndd ${⊢}{z}=⟨{x},{y}⟩\to {2}^{nd}\left({z}\right)={y}$
72 71 fveq2d ${⊢}{z}=⟨{x},{y}⟩\to {1}^{st}\left({G}{\circ }_{\mathrm{func}}{F}\right)\left({2}^{nd}\left({z}\right)\right)={1}^{st}\left({G}{\circ }_{\mathrm{func}}{F}\right)\left({y}\right)$
73 70 72 oveq12d ${⊢}{z}=⟨{x},{y}⟩\to {1}^{st}\left({G}{\circ }_{\mathrm{func}}{F}\right)\left({1}^{st}\left({z}\right)\right)\mathrm{Hom}\left({E}\right){1}^{st}\left({G}{\circ }_{\mathrm{func}}{F}\right)\left({2}^{nd}\left({z}\right)\right)={1}^{st}\left({G}{\circ }_{\mathrm{func}}{F}\right)\left({x}\right)\mathrm{Hom}\left({E}\right){1}^{st}\left({G}{\circ }_{\mathrm{func}}{F}\right)\left({y}\right)$
74 fveq2 ${⊢}{z}=⟨{x},{y}⟩\to \mathrm{Hom}\left({C}\right)\left({z}\right)=\mathrm{Hom}\left({C}\right)\left(⟨{x},{y}⟩\right)$
75 df-ov ${⊢}{x}\mathrm{Hom}\left({C}\right){y}=\mathrm{Hom}\left({C}\right)\left(⟨{x},{y}⟩\right)$
76 74 75 syl6eqr ${⊢}{z}=⟨{x},{y}⟩\to \mathrm{Hom}\left({C}\right)\left({z}\right)={x}\mathrm{Hom}\left({C}\right){y}$
77 73 76 oveq12d ${⊢}{z}=⟨{x},{y}⟩\to {\left({1}^{st}\left({G}{\circ }_{\mathrm{func}}{F}\right)\left({1}^{st}\left({z}\right)\right)\mathrm{Hom}\left({E}\right){1}^{st}\left({G}{\circ }_{\mathrm{func}}{F}\right)\left({2}^{nd}\left({z}\right)\right)\right)}^{\mathrm{Hom}\left({C}\right)\left({z}\right)}={\left({1}^{st}\left({G}{\circ }_{\mathrm{func}}{F}\right)\left({x}\right)\mathrm{Hom}\left({E}\right){1}^{st}\left({G}{\circ }_{\mathrm{func}}{F}\right)\left({y}\right)\right)}^{\left({x}\mathrm{Hom}\left({C}\right){y}\right)}$
78 66 77 eleq12d ${⊢}{z}=⟨{x},{y}⟩\to \left({2}^{nd}\left({G}{\circ }_{\mathrm{func}}{F}\right)\left({z}\right)\in \left({\left({1}^{st}\left({G}{\circ }_{\mathrm{func}}{F}\right)\left({1}^{st}\left({z}\right)\right)\mathrm{Hom}\left({E}\right){1}^{st}\left({G}{\circ }_{\mathrm{func}}{F}\right)\left({2}^{nd}\left({z}\right)\right)\right)}^{\mathrm{Hom}\left({C}\right)\left({z}\right)}\right)↔{x}{2}^{nd}\left({G}{\circ }_{\mathrm{func}}{F}\right){y}\in \left({\left({1}^{st}\left({G}{\circ }_{\mathrm{func}}{F}\right)\left({x}\right)\mathrm{Hom}\left({E}\right){1}^{st}\left({G}{\circ }_{\mathrm{func}}{F}\right)\left({y}\right)\right)}^{\left({x}\mathrm{Hom}\left({C}\right){y}\right)}\right)\right)$
79 78 ralxp ${⊢}\forall {z}\in \left({\mathrm{Base}}_{{C}}×{\mathrm{Base}}_{{C}}\right)\phantom{\rule{.4em}{0ex}}{2}^{nd}\left({G}{\circ }_{\mathrm{func}}{F}\right)\left({z}\right)\in \left({\left({1}^{st}\left({G}{\circ }_{\mathrm{func}}{F}\right)\left({1}^{st}\left({z}\right)\right)\mathrm{Hom}\left({E}\right){1}^{st}\left({G}{\circ }_{\mathrm{func}}{F}\right)\left({2}^{nd}\left({z}\right)\right)\right)}^{\mathrm{Hom}\left({C}\right)\left({z}\right)}\right)↔\forall {x}\in {\mathrm{Base}}_{{C}}\phantom{\rule{.4em}{0ex}}\forall {y}\in {\mathrm{Base}}_{{C}}\phantom{\rule{.4em}{0ex}}{x}{2}^{nd}\left({G}{\circ }_{\mathrm{func}}{F}\right){y}\in \left({\left({1}^{st}\left({G}{\circ }_{\mathrm{func}}{F}\right)\left({x}\right)\mathrm{Hom}\left({E}\right){1}^{st}\left({G}{\circ }_{\mathrm{func}}{F}\right)\left({y}\right)\right)}^{\left({x}\mathrm{Hom}\left({C}\right){y}\right)}\right)$
80 63 79 sylibr ${⊢}{\phi }\to \forall {z}\in \left({\mathrm{Base}}_{{C}}×{\mathrm{Base}}_{{C}}\right)\phantom{\rule{.4em}{0ex}}{2}^{nd}\left({G}{\circ }_{\mathrm{func}}{F}\right)\left({z}\right)\in \left({\left({1}^{st}\left({G}{\circ }_{\mathrm{func}}{F}\right)\left({1}^{st}\left({z}\right)\right)\mathrm{Hom}\left({E}\right){1}^{st}\left({G}{\circ }_{\mathrm{func}}{F}\right)\left({2}^{nd}\left({z}\right)\right)\right)}^{\mathrm{Hom}\left({C}\right)\left({z}\right)}\right)$
81 fvex ${⊢}{2}^{nd}\left({G}{\circ }_{\mathrm{func}}{F}\right)\in \mathrm{V}$
82 81 elixp ${⊢}{2}^{nd}\left({G}{\circ }_{\mathrm{func}}{F}\right)\in \underset{{z}\in {\mathrm{Base}}_{{C}}×{\mathrm{Base}}_{{C}}}{⨉}\left({\left({1}^{st}\left({G}{\circ }_{\mathrm{func}}{F}\right)\left({1}^{st}\left({z}\right)\right)\mathrm{Hom}\left({E}\right){1}^{st}\left({G}{\circ }_{\mathrm{func}}{F}\right)\left({2}^{nd}\left({z}\right)\right)\right)}^{\mathrm{Hom}\left({C}\right)\left({z}\right)}\right)↔\left({2}^{nd}\left({G}{\circ }_{\mathrm{func}}{F}\right)Fn\left({\mathrm{Base}}_{{C}}×{\mathrm{Base}}_{{C}}\right)\wedge \forall {z}\in \left({\mathrm{Base}}_{{C}}×{\mathrm{Base}}_{{C}}\right)\phantom{\rule{.4em}{0ex}}{2}^{nd}\left({G}{\circ }_{\mathrm{func}}{F}\right)\left({z}\right)\in \left({\left({1}^{st}\left({G}{\circ }_{\mathrm{func}}{F}\right)\left({1}^{st}\left({z}\right)\right)\mathrm{Hom}\left({E}\right){1}^{st}\left({G}{\circ }_{\mathrm{func}}{F}\right)\left({2}^{nd}\left({z}\right)\right)\right)}^{\mathrm{Hom}\left({C}\right)\left({z}\right)}\right)\right)$
83 36 80 82 sylanbrc ${⊢}{\phi }\to {2}^{nd}\left({G}{\circ }_{\mathrm{func}}{F}\right)\in \underset{{z}\in {\mathrm{Base}}_{{C}}×{\mathrm{Base}}_{{C}}}{⨉}\left({\left({1}^{st}\left({G}{\circ }_{\mathrm{func}}{F}\right)\left({1}^{st}\left({z}\right)\right)\mathrm{Hom}\left({E}\right){1}^{st}\left({G}{\circ }_{\mathrm{func}}{F}\right)\left({2}^{nd}\left({z}\right)\right)\right)}^{\mathrm{Hom}\left({C}\right)\left({z}\right)}\right)$
84 eqid ${⊢}\mathrm{Id}\left({C}\right)=\mathrm{Id}\left({C}\right)$
85 eqid ${⊢}\mathrm{Id}\left({D}\right)=\mathrm{Id}\left({D}\right)$
86 24 adantr ${⊢}\left({\phi }\wedge {x}\in {\mathrm{Base}}_{{C}}\right)\to {1}^{st}\left({F}\right)\left({C}\mathrm{Func}{D}\right){2}^{nd}\left({F}\right)$
87 simpr ${⊢}\left({\phi }\wedge {x}\in {\mathrm{Base}}_{{C}}\right)\to {x}\in {\mathrm{Base}}_{{C}}$
88 3 84 85 86 87 funcid ${⊢}\left({\phi }\wedge {x}\in {\mathrm{Base}}_{{C}}\right)\to \left({x}{2}^{nd}\left({F}\right){x}\right)\left(\mathrm{Id}\left({C}\right)\left({x}\right)\right)=\mathrm{Id}\left({D}\right)\left({1}^{st}\left({F}\right)\left({x}\right)\right)$
89 88 fveq2d ${⊢}\left({\phi }\wedge {x}\in {\mathrm{Base}}_{{C}}\right)\to \left({1}^{st}\left({F}\right)\left({x}\right){2}^{nd}\left({G}\right){1}^{st}\left({F}\right)\left({x}\right)\right)\left(\left({x}{2}^{nd}\left({F}\right){x}\right)\left(\mathrm{Id}\left({C}\right)\left({x}\right)\right)\right)=\left({1}^{st}\left({F}\right)\left({x}\right){2}^{nd}\left({G}\right){1}^{st}\left({F}\right)\left({x}\right)\right)\left(\mathrm{Id}\left({D}\right)\left({1}^{st}\left({F}\right)\left({x}\right)\right)\right)$
90 eqid ${⊢}\mathrm{Id}\left({E}\right)=\mathrm{Id}\left({E}\right)$
91 20 adantr ${⊢}\left({\phi }\wedge {x}\in {\mathrm{Base}}_{{C}}\right)\to {1}^{st}\left({G}\right)\left({D}\mathrm{Func}{E}\right){2}^{nd}\left({G}\right)$
92 25 ffvelrnda ${⊢}\left({\phi }\wedge {x}\in {\mathrm{Base}}_{{C}}\right)\to {1}^{st}\left({F}\right)\left({x}\right)\in {\mathrm{Base}}_{{D}}$
93 16 85 90 91 92 funcid ${⊢}\left({\phi }\wedge {x}\in {\mathrm{Base}}_{{C}}\right)\to \left({1}^{st}\left({F}\right)\left({x}\right){2}^{nd}\left({G}\right){1}^{st}\left({F}\right)\left({x}\right)\right)\left(\mathrm{Id}\left({D}\right)\left({1}^{st}\left({F}\right)\left({x}\right)\right)\right)=\mathrm{Id}\left({E}\right)\left({1}^{st}\left({G}\right)\left({1}^{st}\left({F}\right)\left({x}\right)\right)\right)$
94 89 93 eqtrd ${⊢}\left({\phi }\wedge {x}\in {\mathrm{Base}}_{{C}}\right)\to \left({1}^{st}\left({F}\right)\left({x}\right){2}^{nd}\left({G}\right){1}^{st}\left({F}\right)\left({x}\right)\right)\left(\left({x}{2}^{nd}\left({F}\right){x}\right)\left(\mathrm{Id}\left({C}\right)\left({x}\right)\right)\right)=\mathrm{Id}\left({E}\right)\left({1}^{st}\left({G}\right)\left({1}^{st}\left({F}\right)\left({x}\right)\right)\right)$
95 1 adantr ${⊢}\left({\phi }\wedge {x}\in {\mathrm{Base}}_{{C}}\right)\to {F}\in \left({C}\mathrm{Func}{D}\right)$
96 2 adantr ${⊢}\left({\phi }\wedge {x}\in {\mathrm{Base}}_{{C}}\right)\to {G}\in \left({D}\mathrm{Func}{E}\right)$
97 funcrcl ${⊢}{F}\in \left({C}\mathrm{Func}{D}\right)\to \left({C}\in \mathrm{Cat}\wedge {D}\in \mathrm{Cat}\right)$
98 1 97 syl ${⊢}{\phi }\to \left({C}\in \mathrm{Cat}\wedge {D}\in \mathrm{Cat}\right)$
99 98 simpld ${⊢}{\phi }\to {C}\in \mathrm{Cat}$
100 99 adantr ${⊢}\left({\phi }\wedge {x}\in {\mathrm{Base}}_{{C}}\right)\to {C}\in \mathrm{Cat}$
101 3 46 84 100 87 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)$
102 3 95 96 87 87 46 101 cofu2 ${⊢}\left({\phi }\wedge {x}\in {\mathrm{Base}}_{{C}}\right)\to \left({x}{2}^{nd}\left({G}{\circ }_{\mathrm{func}}{F}\right){x}\right)\left(\mathrm{Id}\left({C}\right)\left({x}\right)\right)=\left({1}^{st}\left({F}\right)\left({x}\right){2}^{nd}\left({G}\right){1}^{st}\left({F}\right)\left({x}\right)\right)\left(\left({x}{2}^{nd}\left({F}\right){x}\right)\left(\mathrm{Id}\left({C}\right)\left({x}\right)\right)\right)$
103 3 95 96 87 cofu1 ${⊢}\left({\phi }\wedge {x}\in {\mathrm{Base}}_{{C}}\right)\to {1}^{st}\left({G}{\circ }_{\mathrm{func}}{F}\right)\left({x}\right)={1}^{st}\left({G}\right)\left({1}^{st}\left({F}\right)\left({x}\right)\right)$
104 103 fveq2d ${⊢}\left({\phi }\wedge {x}\in {\mathrm{Base}}_{{C}}\right)\to \mathrm{Id}\left({E}\right)\left({1}^{st}\left({G}{\circ }_{\mathrm{func}}{F}\right)\left({x}\right)\right)=\mathrm{Id}\left({E}\right)\left({1}^{st}\left({G}\right)\left({1}^{st}\left({F}\right)\left({x}\right)\right)\right)$
105 94 102 104 3eqtr4d ${⊢}\left({\phi }\wedge {x}\in {\mathrm{Base}}_{{C}}\right)\to \left({x}{2}^{nd}\left({G}{\circ }_{\mathrm{func}}{F}\right){x}\right)\left(\mathrm{Id}\left({C}\right)\left({x}\right)\right)=\mathrm{Id}\left({E}\right)\left({1}^{st}\left({G}{\circ }_{\mathrm{func}}{F}\right)\left({x}\right)\right)$
106 86 adantr ${⊢}\left(\left({\phi }\wedge {x}\in {\mathrm{Base}}_{{C}}\right)\wedge \left(\left({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)\right)\to {1}^{st}\left({F}\right)\left({C}\mathrm{Func}{D}\right){2}^{nd}\left({F}\right)$
107 simplr ${⊢}\left(\left({\phi }\wedge {x}\in {\mathrm{Base}}_{{C}}\right)\wedge \left(\left({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)\right)\to {x}\in {\mathrm{Base}}_{{C}}$
108 simprlr ${⊢}\left(\left({\phi }\wedge {x}\in {\mathrm{Base}}_{{C}}\right)\wedge \left(\left({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)\right)\to {z}\in {\mathrm{Base}}_{{C}}$
109 3 46 37 106 107 108 funcf2 ${⊢}\left(\left({\phi }\wedge {x}\in {\mathrm{Base}}_{{C}}\right)\wedge \left(\left({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)\right)\to \left({x}{2}^{nd}\left({F}\right){z}\right):{x}\mathrm{Hom}\left({C}\right){z}⟶{1}^{st}\left({F}\right)\left({x}\right)\mathrm{Hom}\left({D}\right){1}^{st}\left({F}\right)\left({z}\right)$
110 eqid ${⊢}\mathrm{comp}\left({C}\right)=\mathrm{comp}\left({C}\right)$
111 100 adantr ${⊢}\left(\left({\phi }\wedge {x}\in {\mathrm{Base}}_{{C}}\right)\wedge \left(\left({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)\right)\to {C}\in \mathrm{Cat}$
112 simprll ${⊢}\left(\left({\phi }\wedge {x}\in {\mathrm{Base}}_{{C}}\right)\wedge \left(\left({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)\right)\to {y}\in {\mathrm{Base}}_{{C}}$
113 simprrl ${⊢}\left(\left({\phi }\wedge {x}\in {\mathrm{Base}}_{{C}}\right)\wedge \left(\left({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)\right)\to {f}\in \left({x}\mathrm{Hom}\left({C}\right){y}\right)$
114 simprrr ${⊢}\left(\left({\phi }\wedge {x}\in {\mathrm{Base}}_{{C}}\right)\wedge \left(\left({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)\right)\to {g}\in \left({y}\mathrm{Hom}\left({C}\right){z}\right)$
115 3 46 110 111 107 112 108 113 114 catcocl ${⊢}\left(\left({\phi }\wedge {x}\in {\mathrm{Base}}_{{C}}\right)\wedge \left(\left({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)\right)\to {g}\left(⟨{x},{y}⟩\mathrm{comp}\left({C}\right){z}\right){f}\in \left({x}\mathrm{Hom}\left({C}\right){z}\right)$
116 fvco3 ${⊢}\left(\left({x}{2}^{nd}\left({F}\right){z}\right):{x}\mathrm{Hom}\left({C}\right){z}⟶{1}^{st}\left({F}\right)\left({x}\right)\mathrm{Hom}\left({D}\right){1}^{st}\left({F}\right)\left({z}\right)\wedge {g}\left(⟨{x},{y}⟩\mathrm{comp}\left({C}\right){z}\right){f}\in \left({x}\mathrm{Hom}\left({C}\right){z}\right)\right)\to \left(\left({1}^{st}\left({F}\right)\left({x}\right){2}^{nd}\left({G}\right){1}^{st}\left({F}\right)\left({z}\right)\right)\circ \left({x}{2}^{nd}\left({F}\right){z}\right)\right)\left({g}\left(⟨{x},{y}⟩\mathrm{comp}\left({C}\right){z}\right){f}\right)=\left({1}^{st}\left({F}\right)\left({x}\right){2}^{nd}\left({G}\right){1}^{st}\left({F}\right)\left({z}\right)\right)\left(\left({x}{2}^{nd}\left({F}\right){z}\right)\left({g}\left(⟨{x},{y}⟩\mathrm{comp}\left({C}\right){z}\right){f}\right)\right)$
117 109 115 116 syl2anc ${⊢}\left(\left({\phi }\wedge {x}\in {\mathrm{Base}}_{{C}}\right)\wedge \left(\left({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)\right)\to \left(\left({1}^{st}\left({F}\right)\left({x}\right){2}^{nd}\left({G}\right){1}^{st}\left({F}\right)\left({z}\right)\right)\circ \left({x}{2}^{nd}\left({F}\right){z}\right)\right)\left({g}\left(⟨{x},{y}⟩\mathrm{comp}\left({C}\right){z}\right){f}\right)=\left({1}^{st}\left({F}\right)\left({x}\right){2}^{nd}\left({G}\right){1}^{st}\left({F}\right)\left({z}\right)\right)\left(\left({x}{2}^{nd}\left({F}\right){z}\right)\left({g}\left(⟨{x},{y}⟩\mathrm{comp}\left({C}\right){z}\right){f}\right)\right)$
118 eqid ${⊢}\mathrm{comp}\left({D}\right)=\mathrm{comp}\left({D}\right)$
119 3 46 110 118 106 107 112 108 113 114 funcco ${⊢}\left(\left({\phi }\wedge {x}\in {\mathrm{Base}}_{{C}}\right)\wedge \left(\left({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)\right)\to \left({x}{2}^{nd}\left({F}\right){z}\right)\left({g}\left(⟨{x},{y}⟩\mathrm{comp}\left({C}\right){z}\right){f}\right)=\left({y}{2}^{nd}\left({F}\right){z}\right)\left({g}\right)\left(⟨{1}^{st}\left({F}\right)\left({x}\right),{1}^{st}\left({F}\right)\left({y}\right)⟩\mathrm{comp}\left({D}\right){1}^{st}\left({F}\right)\left({z}\right)\right)\left({x}{2}^{nd}\left({F}\right){y}\right)\left({f}\right)$
120 119 fveq2d ${⊢}\left(\left({\phi }\wedge {x}\in {\mathrm{Base}}_{{C}}\right)\wedge \left(\left({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)\right)\to \left({1}^{st}\left({F}\right)\left({x}\right){2}^{nd}\left({G}\right){1}^{st}\left({F}\right)\left({z}\right)\right)\left(\left({x}{2}^{nd}\left({F}\right){z}\right)\left({g}\left(⟨{x},{y}⟩\mathrm{comp}\left({C}\right){z}\right){f}\right)\right)=\left({1}^{st}\left({F}\right)\left({x}\right){2}^{nd}\left({G}\right){1}^{st}\left({F}\right)\left({z}\right)\right)\left(\left({y}{2}^{nd}\left({F}\right){z}\right)\left({g}\right)\left(⟨{1}^{st}\left({F}\right)\left({x}\right),{1}^{st}\left({F}\right)\left({y}\right)⟩\mathrm{comp}\left({D}\right){1}^{st}\left({F}\right)\left({z}\right)\right)\left({x}{2}^{nd}\left({F}\right){y}\right)\left({f}\right)\right)$
121 eqid ${⊢}\mathrm{comp}\left({E}\right)=\mathrm{comp}\left({E}\right)$
122 91 adantr ${⊢}\left(\left({\phi }\wedge {x}\in {\mathrm{Base}}_{{C}}\right)\wedge \left(\left({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)\right)\to {1}^{st}\left({G}\right)\left({D}\mathrm{Func}{E}\right){2}^{nd}\left({G}\right)$
123 92 adantr ${⊢}\left(\left({\phi }\wedge {x}\in {\mathrm{Base}}_{{C}}\right)\wedge \left(\left({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)\right)\to {1}^{st}\left({F}\right)\left({x}\right)\in {\mathrm{Base}}_{{D}}$
124 25 adantr ${⊢}\left({\phi }\wedge {x}\in {\mathrm{Base}}_{{C}}\right)\to {1}^{st}\left({F}\right):{\mathrm{Base}}_{{C}}⟶{\mathrm{Base}}_{{D}}$
125 124 adantr ${⊢}\left(\left({\phi }\wedge {x}\in {\mathrm{Base}}_{{C}}\right)\wedge \left(\left({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)\right)\to {1}^{st}\left({F}\right):{\mathrm{Base}}_{{C}}⟶{\mathrm{Base}}_{{D}}$
126 125 112 ffvelrnd ${⊢}\left(\left({\phi }\wedge {x}\in {\mathrm{Base}}_{{C}}\right)\wedge \left(\left({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)\right)\to {1}^{st}\left({F}\right)\left({y}\right)\in {\mathrm{Base}}_{{D}}$
127 125 108 ffvelrnd ${⊢}\left(\left({\phi }\wedge {x}\in {\mathrm{Base}}_{{C}}\right)\wedge \left(\left({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)\right)\to {1}^{st}\left({F}\right)\left({z}\right)\in {\mathrm{Base}}_{{D}}$
128 3 46 37 106 107 112 funcf2 ${⊢}\left(\left({\phi }\wedge {x}\in {\mathrm{Base}}_{{C}}\right)\wedge \left(\left({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)\right)\to \left({x}{2}^{nd}\left({F}\right){y}\right):{x}\mathrm{Hom}\left({C}\right){y}⟶{1}^{st}\left({F}\right)\left({x}\right)\mathrm{Hom}\left({D}\right){1}^{st}\left({F}\right)\left({y}\right)$
129 128 113 ffvelrnd ${⊢}\left(\left({\phi }\wedge {x}\in {\mathrm{Base}}_{{C}}\right)\wedge \left(\left({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)\right)\to \left({x}{2}^{nd}\left({F}\right){y}\right)\left({f}\right)\in \left({1}^{st}\left({F}\right)\left({x}\right)\mathrm{Hom}\left({D}\right){1}^{st}\left({F}\right)\left({y}\right)\right)$
130 3 46 37 106 112 108 funcf2 ${⊢}\left(\left({\phi }\wedge {x}\in {\mathrm{Base}}_{{C}}\right)\wedge \left(\left({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)\right)\to \left({y}{2}^{nd}\left({F}\right){z}\right):{y}\mathrm{Hom}\left({C}\right){z}⟶{1}^{st}\left({F}\right)\left({y}\right)\mathrm{Hom}\left({D}\right){1}^{st}\left({F}\right)\left({z}\right)$
131 130 114 ffvelrnd ${⊢}\left(\left({\phi }\wedge {x}\in {\mathrm{Base}}_{{C}}\right)\wedge \left(\left({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)\right)\to \left({y}{2}^{nd}\left({F}\right){z}\right)\left({g}\right)\in \left({1}^{st}\left({F}\right)\left({y}\right)\mathrm{Hom}\left({D}\right){1}^{st}\left({F}\right)\left({z}\right)\right)$
132 16 37 118 121 122 123 126 127 129 131 funcco ${⊢}\left(\left({\phi }\wedge {x}\in {\mathrm{Base}}_{{C}}\right)\wedge \left(\left({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)\right)\to \left({1}^{st}\left({F}\right)\left({x}\right){2}^{nd}\left({G}\right){1}^{st}\left({F}\right)\left({z}\right)\right)\left(\left({y}{2}^{nd}\left({F}\right){z}\right)\left({g}\right)\left(⟨{1}^{st}\left({F}\right)\left({x}\right),{1}^{st}\left({F}\right)\left({y}\right)⟩\mathrm{comp}\left({D}\right){1}^{st}\left({F}\right)\left({z}\right)\right)\left({x}{2}^{nd}\left({F}\right){y}\right)\left({f}\right)\right)=\left({1}^{st}\left({F}\right)\left({y}\right){2}^{nd}\left({G}\right){1}^{st}\left({F}\right)\left({z}\right)\right)\left(\left({y}{2}^{nd}\left({F}\right){z}\right)\left({g}\right)\right)\left(⟨{1}^{st}\left({G}\right)\left({1}^{st}\left({F}\right)\left({x}\right)\right),{1}^{st}\left({G}\right)\left({1}^{st}\left({F}\right)\left({y}\right)\right)⟩\mathrm{comp}\left({E}\right){1}^{st}\left({G}\right)\left({1}^{st}\left({F}\right)\left({z}\right)\right)\right)\left({1}^{st}\left({F}\right)\left({x}\right){2}^{nd}\left({G}\right){1}^{st}\left({F}\right)\left({y}\right)\right)\left(\left({x}{2}^{nd}\left({F}\right){y}\right)\left({f}\right)\right)$
133 117 120 132 3eqtrd ${⊢}\left(\left({\phi }\wedge {x}\in {\mathrm{Base}}_{{C}}\right)\wedge \left(\left({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)\right)\to \left(\left({1}^{st}\left({F}\right)\left({x}\right){2}^{nd}\left({G}\right){1}^{st}\left({F}\right)\left({z}\right)\right)\circ \left({x}{2}^{nd}\left({F}\right){z}\right)\right)\left({g}\left(⟨{x},{y}⟩\mathrm{comp}\left({C}\right){z}\right){f}\right)=\left({1}^{st}\left({F}\right)\left({y}\right){2}^{nd}\left({G}\right){1}^{st}\left({F}\right)\left({z}\right)\right)\left(\left({y}{2}^{nd}\left({F}\right){z}\right)\left({g}\right)\right)\left(⟨{1}^{st}\left({G}\right)\left({1}^{st}\left({F}\right)\left({x}\right)\right),{1}^{st}\left({G}\right)\left({1}^{st}\left({F}\right)\left({y}\right)\right)⟩\mathrm{comp}\left({E}\right){1}^{st}\left({G}\right)\left({1}^{st}\left({F}\right)\left({z}\right)\right)\right)\left({1}^{st}\left({F}\right)\left({x}\right){2}^{nd}\left({G}\right){1}^{st}\left({F}\right)\left({y}\right)\right)\left(\left({x}{2}^{nd}\left({F}\right){y}\right)\left({f}\right)\right)$
134 95 adantr ${⊢}\left(\left({\phi }\wedge {x}\in {\mathrm{Base}}_{{C}}\right)\wedge \left(\left({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)\right)\to {F}\in \left({C}\mathrm{Func}{D}\right)$
135 96 adantr ${⊢}\left(\left({\phi }\wedge {x}\in {\mathrm{Base}}_{{C}}\right)\wedge \left(\left({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)\right)\to {G}\in \left({D}\mathrm{Func}{E}\right)$
136 3 134 135 107 108 cofu2nd ${⊢}\left(\left({\phi }\wedge {x}\in {\mathrm{Base}}_{{C}}\right)\wedge \left(\left({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)\right)\to {x}{2}^{nd}\left({G}{\circ }_{\mathrm{func}}{F}\right){z}=\left({1}^{st}\left({F}\right)\left({x}\right){2}^{nd}\left({G}\right){1}^{st}\left({F}\right)\left({z}\right)\right)\circ \left({x}{2}^{nd}\left({F}\right){z}\right)$
137 136 fveq1d ${⊢}\left(\left({\phi }\wedge {x}\in {\mathrm{Base}}_{{C}}\right)\wedge \left(\left({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)\right)\to \left({x}{2}^{nd}\left({G}{\circ }_{\mathrm{func}}{F}\right){z}\right)\left({g}\left(⟨{x},{y}⟩\mathrm{comp}\left({C}\right){z}\right){f}\right)=\left(\left({1}^{st}\left({F}\right)\left({x}\right){2}^{nd}\left({G}\right){1}^{st}\left({F}\right)\left({z}\right)\right)\circ \left({x}{2}^{nd}\left({F}\right){z}\right)\right)\left({g}\left(⟨{x},{y}⟩\mathrm{comp}\left({C}\right){z}\right){f}\right)$
138 103 adantr ${⊢}\left(\left({\phi }\wedge {x}\in {\mathrm{Base}}_{{C}}\right)\wedge \left(\left({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)\right)\to {1}^{st}\left({G}{\circ }_{\mathrm{func}}{F}\right)\left({x}\right)={1}^{st}\left({G}\right)\left({1}^{st}\left({F}\right)\left({x}\right)\right)$
139 3 134 135 112 cofu1 ${⊢}\left(\left({\phi }\wedge {x}\in {\mathrm{Base}}_{{C}}\right)\wedge \left(\left({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)\right)\to {1}^{st}\left({G}{\circ }_{\mathrm{func}}{F}\right)\left({y}\right)={1}^{st}\left({G}\right)\left({1}^{st}\left({F}\right)\left({y}\right)\right)$
140 138 139 opeq12d ${⊢}\left(\left({\phi }\wedge {x}\in {\mathrm{Base}}_{{C}}\right)\wedge \left(\left({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)\right)\to ⟨{1}^{st}\left({G}{\circ }_{\mathrm{func}}{F}\right)\left({x}\right),{1}^{st}\left({G}{\circ }_{\mathrm{func}}{F}\right)\left({y}\right)⟩=⟨{1}^{st}\left({G}\right)\left({1}^{st}\left({F}\right)\left({x}\right)\right),{1}^{st}\left({G}\right)\left({1}^{st}\left({F}\right)\left({y}\right)\right)⟩$
141 3 134 135 108 cofu1 ${⊢}\left(\left({\phi }\wedge {x}\in {\mathrm{Base}}_{{C}}\right)\wedge \left(\left({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)\right)\to {1}^{st}\left({G}{\circ }_{\mathrm{func}}{F}\right)\left({z}\right)={1}^{st}\left({G}\right)\left({1}^{st}\left({F}\right)\left({z}\right)\right)$
142 140 141 oveq12d ${⊢}\left(\left({\phi }\wedge {x}\in {\mathrm{Base}}_{{C}}\right)\wedge \left(\left({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)\right)\to ⟨{1}^{st}\left({G}{\circ }_{\mathrm{func}}{F}\right)\left({x}\right),{1}^{st}\left({G}{\circ }_{\mathrm{func}}{F}\right)\left({y}\right)⟩\mathrm{comp}\left({E}\right){1}^{st}\left({G}{\circ }_{\mathrm{func}}{F}\right)\left({z}\right)=⟨{1}^{st}\left({G}\right)\left({1}^{st}\left({F}\right)\left({x}\right)\right),{1}^{st}\left({G}\right)\left({1}^{st}\left({F}\right)\left({y}\right)\right)⟩\mathrm{comp}\left({E}\right){1}^{st}\left({G}\right)\left({1}^{st}\left({F}\right)\left({z}\right)\right)$
143 3 134 135 112 108 46 114 cofu2 ${⊢}\left(\left({\phi }\wedge {x}\in {\mathrm{Base}}_{{C}}\right)\wedge \left(\left({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)\right)\to \left({y}{2}^{nd}\left({G}{\circ }_{\mathrm{func}}{F}\right){z}\right)\left({g}\right)=\left({1}^{st}\left({F}\right)\left({y}\right){2}^{nd}\left({G}\right){1}^{st}\left({F}\right)\left({z}\right)\right)\left(\left({y}{2}^{nd}\left({F}\right){z}\right)\left({g}\right)\right)$
144 3 134 135 107 112 46 113 cofu2 ${⊢}\left(\left({\phi }\wedge {x}\in {\mathrm{Base}}_{{C}}\right)\wedge \left(\left({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)\right)\to \left({x}{2}^{nd}\left({G}{\circ }_{\mathrm{func}}{F}\right){y}\right)\left({f}\right)=\left({1}^{st}\left({F}\right)\left({x}\right){2}^{nd}\left({G}\right){1}^{st}\left({F}\right)\left({y}\right)\right)\left(\left({x}{2}^{nd}\left({F}\right){y}\right)\left({f}\right)\right)$
145 142 143 144 oveq123d ${⊢}\left(\left({\phi }\wedge {x}\in {\mathrm{Base}}_{{C}}\right)\wedge \left(\left({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)\right)\to \left({y}{2}^{nd}\left({G}{\circ }_{\mathrm{func}}{F}\right){z}\right)\left({g}\right)\left(⟨{1}^{st}\left({G}{\circ }_{\mathrm{func}}{F}\right)\left({x}\right),{1}^{st}\left({G}{\circ }_{\mathrm{func}}{F}\right)\left({y}\right)⟩\mathrm{comp}\left({E}\right){1}^{st}\left({G}{\circ }_{\mathrm{func}}{F}\right)\left({z}\right)\right)\left({x}{2}^{nd}\left({G}{\circ }_{\mathrm{func}}{F}\right){y}\right)\left({f}\right)=\left({1}^{st}\left({F}\right)\left({y}\right){2}^{nd}\left({G}\right){1}^{st}\left({F}\right)\left({z}\right)\right)\left(\left({y}{2}^{nd}\left({F}\right){z}\right)\left({g}\right)\right)\left(⟨{1}^{st}\left({G}\right)\left({1}^{st}\left({F}\right)\left({x}\right)\right),{1}^{st}\left({G}\right)\left({1}^{st}\left({F}\right)\left({y}\right)\right)⟩\mathrm{comp}\left({E}\right){1}^{st}\left({G}\right)\left({1}^{st}\left({F}\right)\left({z}\right)\right)\right)\left({1}^{st}\left({F}\right)\left({x}\right){2}^{nd}\left({G}\right){1}^{st}\left({F}\right)\left({y}\right)\right)\left(\left({x}{2}^{nd}\left({F}\right){y}\right)\left({f}\right)\right)$
146 133 137 145 3eqtr4d ${⊢}\left(\left({\phi }\wedge {x}\in {\mathrm{Base}}_{{C}}\right)\wedge \left(\left({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)\right)\to \left({x}{2}^{nd}\left({G}{\circ }_{\mathrm{func}}{F}\right){z}\right)\left({g}\left(⟨{x},{y}⟩\mathrm{comp}\left({C}\right){z}\right){f}\right)=\left({y}{2}^{nd}\left({G}{\circ }_{\mathrm{func}}{F}\right){z}\right)\left({g}\right)\left(⟨{1}^{st}\left({G}{\circ }_{\mathrm{func}}{F}\right)\left({x}\right),{1}^{st}\left({G}{\circ }_{\mathrm{func}}{F}\right)\left({y}\right)⟩\mathrm{comp}\left({E}\right){1}^{st}\left({G}{\circ }_{\mathrm{func}}{F}\right)\left({z}\right)\right)\left({x}{2}^{nd}\left({G}{\circ }_{\mathrm{func}}{F}\right){y}\right)\left({f}\right)$
147 146 anassrs ${⊢}\left(\left(\left({\phi }\wedge {x}\in {\mathrm{Base}}_{{C}}\right)\wedge \left({y}\in {\mathrm{Base}}_{{C}}\wedge {z}\in {\mathrm{Base}}_{{C}}\right)\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}{\circ }_{\mathrm{func}}{F}\right){z}\right)\left({g}\left(⟨{x},{y}⟩\mathrm{comp}\left({C}\right){z}\right){f}\right)=\left({y}{2}^{nd}\left({G}{\circ }_{\mathrm{func}}{F}\right){z}\right)\left({g}\right)\left(⟨{1}^{st}\left({G}{\circ }_{\mathrm{func}}{F}\right)\left({x}\right),{1}^{st}\left({G}{\circ }_{\mathrm{func}}{F}\right)\left({y}\right)⟩\mathrm{comp}\left({E}\right){1}^{st}\left({G}{\circ }_{\mathrm{func}}{F}\right)\left({z}\right)\right)\left({x}{2}^{nd}\left({G}{\circ }_{\mathrm{func}}{F}\right){y}\right)\left({f}\right)$
148 147 ralrimivva ${⊢}\left(\left({\phi }\wedge {x}\in {\mathrm{Base}}_{{C}}\right)\wedge \left({y}\in {\mathrm{Base}}_{{C}}\wedge {z}\in {\mathrm{Base}}_{{C}}\right)\right)\to \forall {f}\in \left({x}\mathrm{Hom}\left({C}\right){y}\right)\phantom{\rule{.4em}{0ex}}\forall {g}\in \left({y}\mathrm{Hom}\left({C}\right){z}\right)\phantom{\rule{.4em}{0ex}}\left({x}{2}^{nd}\left({G}{\circ }_{\mathrm{func}}{F}\right){z}\right)\left({g}\left(⟨{x},{y}⟩\mathrm{comp}\left({C}\right){z}\right){f}\right)=\left({y}{2}^{nd}\left({G}{\circ }_{\mathrm{func}}{F}\right){z}\right)\left({g}\right)\left(⟨{1}^{st}\left({G}{\circ }_{\mathrm{func}}{F}\right)\left({x}\right),{1}^{st}\left({G}{\circ }_{\mathrm{func}}{F}\right)\left({y}\right)⟩\mathrm{comp}\left({E}\right){1}^{st}\left({G}{\circ }_{\mathrm{func}}{F}\right)\left({z}\right)\right)\left({x}{2}^{nd}\left({G}{\circ }_{\mathrm{func}}{F}\right){y}\right)\left({f}\right)$
149 148 ralrimivva ${⊢}\left({\phi }\wedge {x}\in {\mathrm{Base}}_{{C}}\right)\to \forall {y}\in {\mathrm{Base}}_{{C}}\phantom{\rule{.4em}{0ex}}\forall {z}\in {\mathrm{Base}}_{{C}}\phantom{\rule{.4em}{0ex}}\forall {f}\in \left({x}\mathrm{Hom}\left({C}\right){y}\right)\phantom{\rule{.4em}{0ex}}\forall {g}\in \left({y}\mathrm{Hom}\left({C}\right){z}\right)\phantom{\rule{.4em}{0ex}}\left({x}{2}^{nd}\left({G}{\circ }_{\mathrm{func}}{F}\right){z}\right)\left({g}\left(⟨{x},{y}⟩\mathrm{comp}\left({C}\right){z}\right){f}\right)=\left({y}{2}^{nd}\left({G}{\circ }_{\mathrm{func}}{F}\right){z}\right)\left({g}\right)\left(⟨{1}^{st}\left({G}{\circ }_{\mathrm{func}}{F}\right)\left({x}\right),{1}^{st}\left({G}{\circ }_{\mathrm{func}}{F}\right)\left({y}\right)⟩\mathrm{comp}\left({E}\right){1}^{st}\left({G}{\circ }_{\mathrm{func}}{F}\right)\left({z}\right)\right)\left({x}{2}^{nd}\left({G}{\circ }_{\mathrm{func}}{F}\right){y}\right)\left({f}\right)$
150 105 149 jca ${⊢}\left({\phi }\wedge {x}\in {\mathrm{Base}}_{{C}}\right)\to \left(\left({x}{2}^{nd}\left({G}{\circ }_{\mathrm{func}}{F}\right){x}\right)\left(\mathrm{Id}\left({C}\right)\left({x}\right)\right)=\mathrm{Id}\left({E}\right)\left({1}^{st}\left({G}{\circ }_{\mathrm{func}}{F}\right)\left({x}\right)\right)\wedge \forall {y}\in {\mathrm{Base}}_{{C}}\phantom{\rule{.4em}{0ex}}\forall {z}\in {\mathrm{Base}}_{{C}}\phantom{\rule{.4em}{0ex}}\forall {f}\in \left({x}\mathrm{Hom}\left({C}\right){y}\right)\phantom{\rule{.4em}{0ex}}\forall {g}\in \left({y}\mathrm{Hom}\left({C}\right){z}\right)\phantom{\rule{.4em}{0ex}}\left({x}{2}^{nd}\left({G}{\circ }_{\mathrm{func}}{F}\right){z}\right)\left({g}\left(⟨{x},{y}⟩\mathrm{comp}\left({C}\right){z}\right){f}\right)=\left({y}{2}^{nd}\left({G}{\circ }_{\mathrm{func}}{F}\right){z}\right)\left({g}\right)\left(⟨{1}^{st}\left({G}{\circ }_{\mathrm{func}}{F}\right)\left({x}\right),{1}^{st}\left({G}{\circ }_{\mathrm{func}}{F}\right)\left({y}\right)⟩\mathrm{comp}\left({E}\right){1}^{st}\left({G}{\circ }_{\mathrm{func}}{F}\right)\left({z}\right)\right)\left({x}{2}^{nd}\left({G}{\circ }_{\mathrm{func}}{F}\right){y}\right)\left({f}\right)\right)$
151 150 ralrimiva ${⊢}{\phi }\to \forall {x}\in {\mathrm{Base}}_{{C}}\phantom{\rule{.4em}{0ex}}\left(\left({x}{2}^{nd}\left({G}{\circ }_{\mathrm{func}}{F}\right){x}\right)\left(\mathrm{Id}\left({C}\right)\left({x}\right)\right)=\mathrm{Id}\left({E}\right)\left({1}^{st}\left({G}{\circ }_{\mathrm{func}}{F}\right)\left({x}\right)\right)\wedge \forall {y}\in {\mathrm{Base}}_{{C}}\phantom{\rule{.4em}{0ex}}\forall {z}\in {\mathrm{Base}}_{{C}}\phantom{\rule{.4em}{0ex}}\forall {f}\in \left({x}\mathrm{Hom}\left({C}\right){y}\right)\phantom{\rule{.4em}{0ex}}\forall {g}\in \left({y}\mathrm{Hom}\left({C}\right){z}\right)\phantom{\rule{.4em}{0ex}}\left({x}{2}^{nd}\left({G}{\circ }_{\mathrm{func}}{F}\right){z}\right)\left({g}\left(⟨{x},{y}⟩\mathrm{comp}\left({C}\right){z}\right){f}\right)=\left({y}{2}^{nd}\left({G}{\circ }_{\mathrm{func}}{F}\right){z}\right)\left({g}\right)\left(⟨{1}^{st}\left({G}{\circ }_{\mathrm{func}}{F}\right)\left({x}\right),{1}^{st}\left({G}{\circ }_{\mathrm{func}}{F}\right)\left({y}\right)⟩\mathrm{comp}\left({E}\right){1}^{st}\left({G}{\circ }_{\mathrm{func}}{F}\right)\left({z}\right)\right)\left({x}{2}^{nd}\left({G}{\circ }_{\mathrm{func}}{F}\right){y}\right)\left({f}\right)\right)$
152 funcrcl ${⊢}{G}\in \left({D}\mathrm{Func}{E}\right)\to \left({D}\in \mathrm{Cat}\wedge {E}\in \mathrm{Cat}\right)$
153 2 152 syl ${⊢}{\phi }\to \left({D}\in \mathrm{Cat}\wedge {E}\in \mathrm{Cat}\right)$
154 153 simprd ${⊢}{\phi }\to {E}\in \mathrm{Cat}$
155 3 17 46 38 84 90 110 121 99 154 isfunc ${⊢}{\phi }\to \left({1}^{st}\left({G}{\circ }_{\mathrm{func}}{F}\right)\left({C}\mathrm{Func}{E}\right){2}^{nd}\left({G}{\circ }_{\mathrm{func}}{F}\right)↔\left({1}^{st}\left({G}{\circ }_{\mathrm{func}}{F}\right):{\mathrm{Base}}_{{C}}⟶{\mathrm{Base}}_{{E}}\wedge {2}^{nd}\left({G}{\circ }_{\mathrm{func}}{F}\right)\in \underset{{z}\in {\mathrm{Base}}_{{C}}×{\mathrm{Base}}_{{C}}}{⨉}\left({\left({1}^{st}\left({G}{\circ }_{\mathrm{func}}{F}\right)\left({1}^{st}\left({z}\right)\right)\mathrm{Hom}\left({E}\right){1}^{st}\left({G}{\circ }_{\mathrm{func}}{F}\right)\left({2}^{nd}\left({z}\right)\right)\right)}^{\mathrm{Hom}\left({C}\right)\left({z}\right)}\right)\wedge \forall {x}\in {\mathrm{Base}}_{{C}}\phantom{\rule{.4em}{0ex}}\left(\left({x}{2}^{nd}\left({G}{\circ }_{\mathrm{func}}{F}\right){x}\right)\left(\mathrm{Id}\left({C}\right)\left({x}\right)\right)=\mathrm{Id}\left({E}\right)\left({1}^{st}\left({G}{\circ }_{\mathrm{func}}{F}\right)\left({x}\right)\right)\wedge \forall {y}\in {\mathrm{Base}}_{{C}}\phantom{\rule{.4em}{0ex}}\forall {z}\in {\mathrm{Base}}_{{C}}\phantom{\rule{.4em}{0ex}}\forall {f}\in \left({x}\mathrm{Hom}\left({C}\right){y}\right)\phantom{\rule{.4em}{0ex}}\forall {g}\in \left({y}\mathrm{Hom}\left({C}\right){z}\right)\phantom{\rule{.4em}{0ex}}\left({x}{2}^{nd}\left({G}{\circ }_{\mathrm{func}}{F}\right){z}\right)\left({g}\left(⟨{x},{y}⟩\mathrm{comp}\left({C}\right){z}\right){f}\right)=\left({y}{2}^{nd}\left({G}{\circ }_{\mathrm{func}}{F}\right){z}\right)\left({g}\right)\left(⟨{1}^{st}\left({G}{\circ }_{\mathrm{func}}{F}\right)\left({x}\right),{1}^{st}\left({G}{\circ }_{\mathrm{func}}{F}\right)\left({y}\right)⟩\mathrm{comp}\left({E}\right){1}^{st}\left({G}{\circ }_{\mathrm{func}}{F}\right)\left({z}\right)\right)\left({x}{2}^{nd}\left({G}{\circ }_{\mathrm{func}}{F}\right){y}\right)\left({f}\right)\right)\right)\right)$
156 29 83 151 155 mpbir3and ${⊢}{\phi }\to {1}^{st}\left({G}{\circ }_{\mathrm{func}}{F}\right)\left({C}\mathrm{Func}{E}\right){2}^{nd}\left({G}{\circ }_{\mathrm{func}}{F}\right)$
157 df-br ${⊢}{1}^{st}\left({G}{\circ }_{\mathrm{func}}{F}\right)\left({C}\mathrm{Func}{E}\right){2}^{nd}\left({G}{\circ }_{\mathrm{func}}{F}\right)↔⟨{1}^{st}\left({G}{\circ }_{\mathrm{func}}{F}\right),{2}^{nd}\left({G}{\circ }_{\mathrm{func}}{F}\right)⟩\in \left({C}\mathrm{Func}{E}\right)$
158 156 157 sylib ${⊢}{\phi }\to ⟨{1}^{st}\left({G}{\circ }_{\mathrm{func}}{F}\right),{2}^{nd}\left({G}{\circ }_{\mathrm{func}}{F}\right)⟩\in \left({C}\mathrm{Func}{E}\right)$
159 15 158 eqeltrd ${⊢}{\phi }\to {G}{\circ }_{\mathrm{func}}{F}\in \left({C}\mathrm{Func}{E}\right)$