# Metamath Proof Explorer

## Theorem funcres

Description: A functor restricted to a subcategory is a functor. (Contributed by Mario Carneiro, 6-Jan-2017)

Ref Expression
Hypotheses funcres.f ${⊢}{\phi }\to {F}\in \left({C}\mathrm{Func}{D}\right)$
funcres.h ${⊢}{\phi }\to {H}\in \mathrm{Subcat}\left({C}\right)$
Assertion funcres ${⊢}{\phi }\to {F}{↾}_{f}{H}\in \left(\left({C}{↾}_{\mathrm{cat}}{H}\right)\mathrm{Func}{D}\right)$

### Proof

Step Hyp Ref Expression
1 funcres.f ${⊢}{\phi }\to {F}\in \left({C}\mathrm{Func}{D}\right)$
2 funcres.h ${⊢}{\phi }\to {H}\in \mathrm{Subcat}\left({C}\right)$
3 1 2 resfval ${⊢}{\phi }\to {F}{↾}_{f}{H}=⟨{{1}^{st}\left({F}\right)↾}_{\mathrm{dom}\mathrm{dom}{H}},\left({z}\in \mathrm{dom}{H}⟼{{2}^{nd}\left({F}\right)\left({z}\right)↾}_{{H}\left({z}\right)}\right)⟩$
4 3 fveq2d ${⊢}{\phi }\to {2}^{nd}\left({F}{↾}_{f}{H}\right)={2}^{nd}\left(⟨{{1}^{st}\left({F}\right)↾}_{\mathrm{dom}\mathrm{dom}{H}},\left({z}\in \mathrm{dom}{H}⟼{{2}^{nd}\left({F}\right)\left({z}\right)↾}_{{H}\left({z}\right)}\right)⟩\right)$
5 fvex ${⊢}{1}^{st}\left({F}\right)\in \mathrm{V}$
6 5 resex ${⊢}{{1}^{st}\left({F}\right)↾}_{\mathrm{dom}\mathrm{dom}{H}}\in \mathrm{V}$
7 dmexg ${⊢}{H}\in \mathrm{Subcat}\left({C}\right)\to \mathrm{dom}{H}\in \mathrm{V}$
8 mptexg ${⊢}\mathrm{dom}{H}\in \mathrm{V}\to \left({z}\in \mathrm{dom}{H}⟼{{2}^{nd}\left({F}\right)\left({z}\right)↾}_{{H}\left({z}\right)}\right)\in \mathrm{V}$
9 2 7 8 3syl ${⊢}{\phi }\to \left({z}\in \mathrm{dom}{H}⟼{{2}^{nd}\left({F}\right)\left({z}\right)↾}_{{H}\left({z}\right)}\right)\in \mathrm{V}$
10 op2ndg ${⊢}\left({{1}^{st}\left({F}\right)↾}_{\mathrm{dom}\mathrm{dom}{H}}\in \mathrm{V}\wedge \left({z}\in \mathrm{dom}{H}⟼{{2}^{nd}\left({F}\right)\left({z}\right)↾}_{{H}\left({z}\right)}\right)\in \mathrm{V}\right)\to {2}^{nd}\left(⟨{{1}^{st}\left({F}\right)↾}_{\mathrm{dom}\mathrm{dom}{H}},\left({z}\in \mathrm{dom}{H}⟼{{2}^{nd}\left({F}\right)\left({z}\right)↾}_{{H}\left({z}\right)}\right)⟩\right)=\left({z}\in \mathrm{dom}{H}⟼{{2}^{nd}\left({F}\right)\left({z}\right)↾}_{{H}\left({z}\right)}\right)$
11 6 9 10 sylancr ${⊢}{\phi }\to {2}^{nd}\left(⟨{{1}^{st}\left({F}\right)↾}_{\mathrm{dom}\mathrm{dom}{H}},\left({z}\in \mathrm{dom}{H}⟼{{2}^{nd}\left({F}\right)\left({z}\right)↾}_{{H}\left({z}\right)}\right)⟩\right)=\left({z}\in \mathrm{dom}{H}⟼{{2}^{nd}\left({F}\right)\left({z}\right)↾}_{{H}\left({z}\right)}\right)$
12 4 11 eqtrd ${⊢}{\phi }\to {2}^{nd}\left({F}{↾}_{f}{H}\right)=\left({z}\in \mathrm{dom}{H}⟼{{2}^{nd}\left({F}\right)\left({z}\right)↾}_{{H}\left({z}\right)}\right)$
13 12 opeq2d ${⊢}{\phi }\to ⟨{{1}^{st}\left({F}\right)↾}_{\mathrm{dom}\mathrm{dom}{H}},{2}^{nd}\left({F}{↾}_{f}{H}\right)⟩=⟨{{1}^{st}\left({F}\right)↾}_{\mathrm{dom}\mathrm{dom}{H}},\left({z}\in \mathrm{dom}{H}⟼{{2}^{nd}\left({F}\right)\left({z}\right)↾}_{{H}\left({z}\right)}\right)⟩$
14 3 13 eqtr4d ${⊢}{\phi }\to {F}{↾}_{f}{H}=⟨{{1}^{st}\left({F}\right)↾}_{\mathrm{dom}\mathrm{dom}{H}},{2}^{nd}\left({F}{↾}_{f}{H}\right)⟩$
15 eqid ${⊢}{\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}={\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}$
16 eqid ${⊢}{\mathrm{Base}}_{{D}}={\mathrm{Base}}_{{D}}$
17 eqid ${⊢}\mathrm{Hom}\left({C}{↾}_{\mathrm{cat}}{H}\right)=\mathrm{Hom}\left({C}{↾}_{\mathrm{cat}}{H}\right)$
18 eqid ${⊢}\mathrm{Hom}\left({D}\right)=\mathrm{Hom}\left({D}\right)$
19 eqid ${⊢}\mathrm{Id}\left({C}{↾}_{\mathrm{cat}}{H}\right)=\mathrm{Id}\left({C}{↾}_{\mathrm{cat}}{H}\right)$
20 eqid ${⊢}\mathrm{Id}\left({D}\right)=\mathrm{Id}\left({D}\right)$
21 eqid ${⊢}\mathrm{comp}\left({C}{↾}_{\mathrm{cat}}{H}\right)=\mathrm{comp}\left({C}{↾}_{\mathrm{cat}}{H}\right)$
22 eqid ${⊢}\mathrm{comp}\left({D}\right)=\mathrm{comp}\left({D}\right)$
23 eqid ${⊢}{C}{↾}_{\mathrm{cat}}{H}={C}{↾}_{\mathrm{cat}}{H}$
24 23 2 subccat ${⊢}{\phi }\to {C}{↾}_{\mathrm{cat}}{H}\in \mathrm{Cat}$
25 funcrcl ${⊢}{F}\in \left({C}\mathrm{Func}{D}\right)\to \left({C}\in \mathrm{Cat}\wedge {D}\in \mathrm{Cat}\right)$
26 1 25 syl ${⊢}{\phi }\to \left({C}\in \mathrm{Cat}\wedge {D}\in \mathrm{Cat}\right)$
27 26 simprd ${⊢}{\phi }\to {D}\in \mathrm{Cat}$
28 eqid ${⊢}{\mathrm{Base}}_{{C}}={\mathrm{Base}}_{{C}}$
29 relfunc ${⊢}\mathrm{Rel}\left({C}\mathrm{Func}{D}\right)$
30 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)$
31 29 1 30 sylancr ${⊢}{\phi }\to {1}^{st}\left({F}\right)\left({C}\mathrm{Func}{D}\right){2}^{nd}\left({F}\right)$
32 28 16 31 funcf1 ${⊢}{\phi }\to {1}^{st}\left({F}\right):{\mathrm{Base}}_{{C}}⟶{\mathrm{Base}}_{{D}}$
33 eqidd ${⊢}{\phi }\to \mathrm{dom}\mathrm{dom}{H}=\mathrm{dom}\mathrm{dom}{H}$
34 2 33 subcfn ${⊢}{\phi }\to {H}Fn\left(\mathrm{dom}\mathrm{dom}{H}×\mathrm{dom}\mathrm{dom}{H}\right)$
35 2 34 28 subcss1 ${⊢}{\phi }\to \mathrm{dom}\mathrm{dom}{H}\subseteq {\mathrm{Base}}_{{C}}$
36 32 35 fssresd ${⊢}{\phi }\to \left({{1}^{st}\left({F}\right)↾}_{\mathrm{dom}\mathrm{dom}{H}}\right):\mathrm{dom}\mathrm{dom}{H}⟶{\mathrm{Base}}_{{D}}$
37 26 simpld ${⊢}{\phi }\to {C}\in \mathrm{Cat}$
38 23 28 37 34 35 rescbas ${⊢}{\phi }\to \mathrm{dom}\mathrm{dom}{H}={\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}$
39 38 feq2d ${⊢}{\phi }\to \left(\left({{1}^{st}\left({F}\right)↾}_{\mathrm{dom}\mathrm{dom}{H}}\right):\mathrm{dom}\mathrm{dom}{H}⟶{\mathrm{Base}}_{{D}}↔\left({{1}^{st}\left({F}\right)↾}_{\mathrm{dom}\mathrm{dom}{H}}\right):{\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}⟶{\mathrm{Base}}_{{D}}\right)$
40 36 39 mpbid ${⊢}{\phi }\to \left({{1}^{st}\left({F}\right)↾}_{\mathrm{dom}\mathrm{dom}{H}}\right):{\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}⟶{\mathrm{Base}}_{{D}}$
41 fvex ${⊢}{2}^{nd}\left({F}\right)\left({z}\right)\in \mathrm{V}$
42 41 resex ${⊢}{{2}^{nd}\left({F}\right)\left({z}\right)↾}_{{H}\left({z}\right)}\in \mathrm{V}$
43 eqid ${⊢}\left({z}\in \mathrm{dom}{H}⟼{{2}^{nd}\left({F}\right)\left({z}\right)↾}_{{H}\left({z}\right)}\right)=\left({z}\in \mathrm{dom}{H}⟼{{2}^{nd}\left({F}\right)\left({z}\right)↾}_{{H}\left({z}\right)}\right)$
44 42 43 fnmpti ${⊢}\left({z}\in \mathrm{dom}{H}⟼{{2}^{nd}\left({F}\right)\left({z}\right)↾}_{{H}\left({z}\right)}\right)Fn\mathrm{dom}{H}$
45 12 eqcomd ${⊢}{\phi }\to \left({z}\in \mathrm{dom}{H}⟼{{2}^{nd}\left({F}\right)\left({z}\right)↾}_{{H}\left({z}\right)}\right)={2}^{nd}\left({F}{↾}_{f}{H}\right)$
46 fndm ${⊢}{H}Fn\left(\mathrm{dom}\mathrm{dom}{H}×\mathrm{dom}\mathrm{dom}{H}\right)\to \mathrm{dom}{H}=\mathrm{dom}\mathrm{dom}{H}×\mathrm{dom}\mathrm{dom}{H}$
47 34 46 syl ${⊢}{\phi }\to \mathrm{dom}{H}=\mathrm{dom}\mathrm{dom}{H}×\mathrm{dom}\mathrm{dom}{H}$
48 38 sqxpeqd ${⊢}{\phi }\to \mathrm{dom}\mathrm{dom}{H}×\mathrm{dom}\mathrm{dom}{H}={\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}×{\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}$
49 47 48 eqtrd ${⊢}{\phi }\to \mathrm{dom}{H}={\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}×{\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}$
50 45 49 fneq12d ${⊢}{\phi }\to \left(\left({z}\in \mathrm{dom}{H}⟼{{2}^{nd}\left({F}\right)\left({z}\right)↾}_{{H}\left({z}\right)}\right)Fn\mathrm{dom}{H}↔{2}^{nd}\left({F}{↾}_{f}{H}\right)Fn\left({\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}×{\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\right)\right)$
51 44 50 mpbii ${⊢}{\phi }\to {2}^{nd}\left({F}{↾}_{f}{H}\right)Fn\left({\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}×{\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\right)$
52 eqid ${⊢}\mathrm{Hom}\left({C}\right)=\mathrm{Hom}\left({C}\right)$
53 31 adantr ${⊢}\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\wedge {y}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\right)\right)\to {1}^{st}\left({F}\right)\left({C}\mathrm{Func}{D}\right){2}^{nd}\left({F}\right)$
54 35 adantr ${⊢}\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\wedge {y}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\right)\right)\to \mathrm{dom}\mathrm{dom}{H}\subseteq {\mathrm{Base}}_{{C}}$
55 simprl ${⊢}\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\wedge {y}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\right)\right)\to {x}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}$
56 38 adantr ${⊢}\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\wedge {y}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\right)\right)\to \mathrm{dom}\mathrm{dom}{H}={\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}$
57 55 56 eleqtrrd ${⊢}\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\wedge {y}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\right)\right)\to {x}\in \mathrm{dom}\mathrm{dom}{H}$
58 54 57 sseldd ${⊢}\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\wedge {y}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\right)\right)\to {x}\in {\mathrm{Base}}_{{C}}$
59 simprr ${⊢}\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\wedge {y}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\right)\right)\to {y}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}$
60 59 56 eleqtrrd ${⊢}\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\wedge {y}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\right)\right)\to {y}\in \mathrm{dom}\mathrm{dom}{H}$
61 54 60 sseldd ${⊢}\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\wedge {y}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\right)\right)\to {y}\in {\mathrm{Base}}_{{C}}$
62 28 52 18 53 58 61 funcf2 ${⊢}\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\wedge {y}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\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)$
63 2 adantr ${⊢}\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\wedge {y}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\right)\right)\to {H}\in \mathrm{Subcat}\left({C}\right)$
64 34 adantr ${⊢}\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\wedge {y}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\right)\right)\to {H}Fn\left(\mathrm{dom}\mathrm{dom}{H}×\mathrm{dom}\mathrm{dom}{H}\right)$
65 63 64 52 57 60 subcss2 ${⊢}\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\wedge {y}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\right)\right)\to {x}{H}{y}\subseteq {x}\mathrm{Hom}\left({C}\right){y}$
66 62 65 fssresd ${⊢}\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\wedge {y}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\right)\right)\to \left({\left({x}{2}^{nd}\left({F}\right){y}\right)↾}_{\left({x}{H}{y}\right)}\right):{x}{H}{y}⟶{1}^{st}\left({F}\right)\left({x}\right)\mathrm{Hom}\left({D}\right){1}^{st}\left({F}\right)\left({y}\right)$
67 1 adantr ${⊢}\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\wedge {y}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\right)\right)\to {F}\in \left({C}\mathrm{Func}{D}\right)$
68 67 63 64 57 60 resf2nd ${⊢}\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\wedge {y}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\right)\right)\to {x}{2}^{nd}\left({F}{↾}_{f}{H}\right){y}={\left({x}{2}^{nd}\left({F}\right){y}\right)↾}_{\left({x}{H}{y}\right)}$
69 68 feq1d ${⊢}\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\wedge {y}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\right)\right)\to \left(\left({x}{2}^{nd}\left({F}{↾}_{f}{H}\right){y}\right):{x}{H}{y}⟶{1}^{st}\left({F}\right)\left({x}\right)\mathrm{Hom}\left({D}\right){1}^{st}\left({F}\right)\left({y}\right)↔\left({\left({x}{2}^{nd}\left({F}\right){y}\right)↾}_{\left({x}{H}{y}\right)}\right):{x}{H}{y}⟶{1}^{st}\left({F}\right)\left({x}\right)\mathrm{Hom}\left({D}\right){1}^{st}\left({F}\right)\left({y}\right)\right)$
70 66 69 mpbird ${⊢}\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\wedge {y}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\right)\right)\to \left({x}{2}^{nd}\left({F}{↾}_{f}{H}\right){y}\right):{x}{H}{y}⟶{1}^{st}\left({F}\right)\left({x}\right)\mathrm{Hom}\left({D}\right){1}^{st}\left({F}\right)\left({y}\right)$
71 23 28 37 34 35 reschom ${⊢}{\phi }\to {H}=\mathrm{Hom}\left({C}{↾}_{\mathrm{cat}}{H}\right)$
72 71 adantr ${⊢}\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\wedge {y}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\right)\right)\to {H}=\mathrm{Hom}\left({C}{↾}_{\mathrm{cat}}{H}\right)$
73 72 oveqd ${⊢}\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\wedge {y}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\right)\right)\to {x}{H}{y}={x}\mathrm{Hom}\left({C}{↾}_{\mathrm{cat}}{H}\right){y}$
74 57 fvresd ${⊢}\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\wedge {y}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\right)\right)\to \left({{1}^{st}\left({F}\right)↾}_{\mathrm{dom}\mathrm{dom}{H}}\right)\left({x}\right)={1}^{st}\left({F}\right)\left({x}\right)$
75 60 fvresd ${⊢}\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\wedge {y}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\right)\right)\to \left({{1}^{st}\left({F}\right)↾}_{\mathrm{dom}\mathrm{dom}{H}}\right)\left({y}\right)={1}^{st}\left({F}\right)\left({y}\right)$
76 74 75 oveq12d ${⊢}\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\wedge {y}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\right)\right)\to \left({{1}^{st}\left({F}\right)↾}_{\mathrm{dom}\mathrm{dom}{H}}\right)\left({x}\right)\mathrm{Hom}\left({D}\right)\left({{1}^{st}\left({F}\right)↾}_{\mathrm{dom}\mathrm{dom}{H}}\right)\left({y}\right)={1}^{st}\left({F}\right)\left({x}\right)\mathrm{Hom}\left({D}\right){1}^{st}\left({F}\right)\left({y}\right)$
77 76 eqcomd ${⊢}\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\wedge {y}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\right)\right)\to {1}^{st}\left({F}\right)\left({x}\right)\mathrm{Hom}\left({D}\right){1}^{st}\left({F}\right)\left({y}\right)=\left({{1}^{st}\left({F}\right)↾}_{\mathrm{dom}\mathrm{dom}{H}}\right)\left({x}\right)\mathrm{Hom}\left({D}\right)\left({{1}^{st}\left({F}\right)↾}_{\mathrm{dom}\mathrm{dom}{H}}\right)\left({y}\right)$
78 73 77 feq23d ${⊢}\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\wedge {y}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\right)\right)\to \left(\left({x}{2}^{nd}\left({F}{↾}_{f}{H}\right){y}\right):{x}{H}{y}⟶{1}^{st}\left({F}\right)\left({x}\right)\mathrm{Hom}\left({D}\right){1}^{st}\left({F}\right)\left({y}\right)↔\left({x}{2}^{nd}\left({F}{↾}_{f}{H}\right){y}\right):{x}\mathrm{Hom}\left({C}{↾}_{\mathrm{cat}}{H}\right){y}⟶\left({{1}^{st}\left({F}\right)↾}_{\mathrm{dom}\mathrm{dom}{H}}\right)\left({x}\right)\mathrm{Hom}\left({D}\right)\left({{1}^{st}\left({F}\right)↾}_{\mathrm{dom}\mathrm{dom}{H}}\right)\left({y}\right)\right)$
79 70 78 mpbid ${⊢}\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\wedge {y}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\right)\right)\to \left({x}{2}^{nd}\left({F}{↾}_{f}{H}\right){y}\right):{x}\mathrm{Hom}\left({C}{↾}_{\mathrm{cat}}{H}\right){y}⟶\left({{1}^{st}\left({F}\right)↾}_{\mathrm{dom}\mathrm{dom}{H}}\right)\left({x}\right)\mathrm{Hom}\left({D}\right)\left({{1}^{st}\left({F}\right)↾}_{\mathrm{dom}\mathrm{dom}{H}}\right)\left({y}\right)$
80 1 adantr ${⊢}\left({\phi }\wedge {x}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\right)\to {F}\in \left({C}\mathrm{Func}{D}\right)$
81 2 adantr ${⊢}\left({\phi }\wedge {x}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\right)\to {H}\in \mathrm{Subcat}\left({C}\right)$
82 34 adantr ${⊢}\left({\phi }\wedge {x}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\right)\to {H}Fn\left(\mathrm{dom}\mathrm{dom}{H}×\mathrm{dom}\mathrm{dom}{H}\right)$
83 38 eleq2d ${⊢}{\phi }\to \left({x}\in \mathrm{dom}\mathrm{dom}{H}↔{x}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\right)$
84 83 biimpar ${⊢}\left({\phi }\wedge {x}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\right)\to {x}\in \mathrm{dom}\mathrm{dom}{H}$
85 80 81 82 84 84 resf2nd ${⊢}\left({\phi }\wedge {x}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\right)\to {x}{2}^{nd}\left({F}{↾}_{f}{H}\right){x}={\left({x}{2}^{nd}\left({F}\right){x}\right)↾}_{\left({x}{H}{x}\right)}$
86 eqid ${⊢}\mathrm{Id}\left({C}\right)=\mathrm{Id}\left({C}\right)$
87 23 81 82 86 84 subcid ${⊢}\left({\phi }\wedge {x}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\right)\to \mathrm{Id}\left({C}\right)\left({x}\right)=\mathrm{Id}\left({C}{↾}_{\mathrm{cat}}{H}\right)\left({x}\right)$
88 87 eqcomd ${⊢}\left({\phi }\wedge {x}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\right)\to \mathrm{Id}\left({C}{↾}_{\mathrm{cat}}{H}\right)\left({x}\right)=\mathrm{Id}\left({C}\right)\left({x}\right)$
89 85 88 fveq12d ${⊢}\left({\phi }\wedge {x}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\right)\to \left({x}{2}^{nd}\left({F}{↾}_{f}{H}\right){x}\right)\left(\mathrm{Id}\left({C}{↾}_{\mathrm{cat}}{H}\right)\left({x}\right)\right)=\left({\left({x}{2}^{nd}\left({F}\right){x}\right)↾}_{\left({x}{H}{x}\right)}\right)\left(\mathrm{Id}\left({C}\right)\left({x}\right)\right)$
90 31 adantr ${⊢}\left({\phi }\wedge {x}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\right)\to {1}^{st}\left({F}\right)\left({C}\mathrm{Func}{D}\right){2}^{nd}\left({F}\right)$
91 38 35 eqsstrrd ${⊢}{\phi }\to {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\subseteq {\mathrm{Base}}_{{C}}$
92 91 sselda ${⊢}\left({\phi }\wedge {x}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\right)\to {x}\in {\mathrm{Base}}_{{C}}$
93 28 86 20 90 92 funcid ${⊢}\left({\phi }\wedge {x}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\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)$
94 81 82 84 86 subcidcl ${⊢}\left({\phi }\wedge {x}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\right)\to \mathrm{Id}\left({C}\right)\left({x}\right)\in \left({x}{H}{x}\right)$
95 94 fvresd ${⊢}\left({\phi }\wedge {x}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\right)\to \left({\left({x}{2}^{nd}\left({F}\right){x}\right)↾}_{\left({x}{H}{x}\right)}\right)\left(\mathrm{Id}\left({C}\right)\left({x}\right)\right)=\left({x}{2}^{nd}\left({F}\right){x}\right)\left(\mathrm{Id}\left({C}\right)\left({x}\right)\right)$
96 84 fvresd ${⊢}\left({\phi }\wedge {x}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\right)\to \left({{1}^{st}\left({F}\right)↾}_{\mathrm{dom}\mathrm{dom}{H}}\right)\left({x}\right)={1}^{st}\left({F}\right)\left({x}\right)$
97 96 fveq2d ${⊢}\left({\phi }\wedge {x}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\right)\to \mathrm{Id}\left({D}\right)\left(\left({{1}^{st}\left({F}\right)↾}_{\mathrm{dom}\mathrm{dom}{H}}\right)\left({x}\right)\right)=\mathrm{Id}\left({D}\right)\left({1}^{st}\left({F}\right)\left({x}\right)\right)$
98 93 95 97 3eqtr4d ${⊢}\left({\phi }\wedge {x}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\right)\to \left({\left({x}{2}^{nd}\left({F}\right){x}\right)↾}_{\left({x}{H}{x}\right)}\right)\left(\mathrm{Id}\left({C}\right)\left({x}\right)\right)=\mathrm{Id}\left({D}\right)\left(\left({{1}^{st}\left({F}\right)↾}_{\mathrm{dom}\mathrm{dom}{H}}\right)\left({x}\right)\right)$
99 89 98 eqtrd ${⊢}\left({\phi }\wedge {x}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\right)\to \left({x}{2}^{nd}\left({F}{↾}_{f}{H}\right){x}\right)\left(\mathrm{Id}\left({C}{↾}_{\mathrm{cat}}{H}\right)\left({x}\right)\right)=\mathrm{Id}\left({D}\right)\left(\left({{1}^{st}\left({F}\right)↾}_{\mathrm{dom}\mathrm{dom}{H}}\right)\left({x}\right)\right)$
100 2 3ad2ant1 ${⊢}\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\wedge {y}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\wedge {z}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}{↾}_{\mathrm{cat}}{H}\right){y}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({C}{↾}_{\mathrm{cat}}{H}\right){z}\right)\right)\right)\to {H}\in \mathrm{Subcat}\left({C}\right)$
101 34 3ad2ant1 ${⊢}\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\wedge {y}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\wedge {z}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}{↾}_{\mathrm{cat}}{H}\right){y}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({C}{↾}_{\mathrm{cat}}{H}\right){z}\right)\right)\right)\to {H}Fn\left(\mathrm{dom}\mathrm{dom}{H}×\mathrm{dom}\mathrm{dom}{H}\right)$
102 simp21 ${⊢}\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\wedge {y}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\wedge {z}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}{↾}_{\mathrm{cat}}{H}\right){y}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({C}{↾}_{\mathrm{cat}}{H}\right){z}\right)\right)\right)\to {x}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}$
103 38 3ad2ant1 ${⊢}\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\wedge {y}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\wedge {z}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}{↾}_{\mathrm{cat}}{H}\right){y}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({C}{↾}_{\mathrm{cat}}{H}\right){z}\right)\right)\right)\to \mathrm{dom}\mathrm{dom}{H}={\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}$
104 102 103 eleqtrrd ${⊢}\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\wedge {y}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\wedge {z}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}{↾}_{\mathrm{cat}}{H}\right){y}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({C}{↾}_{\mathrm{cat}}{H}\right){z}\right)\right)\right)\to {x}\in \mathrm{dom}\mathrm{dom}{H}$
105 eqid ${⊢}\mathrm{comp}\left({C}\right)=\mathrm{comp}\left({C}\right)$
106 simp22 ${⊢}\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\wedge {y}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\wedge {z}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}{↾}_{\mathrm{cat}}{H}\right){y}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({C}{↾}_{\mathrm{cat}}{H}\right){z}\right)\right)\right)\to {y}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}$
107 106 103 eleqtrrd ${⊢}\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\wedge {y}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\wedge {z}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}{↾}_{\mathrm{cat}}{H}\right){y}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({C}{↾}_{\mathrm{cat}}{H}\right){z}\right)\right)\right)\to {y}\in \mathrm{dom}\mathrm{dom}{H}$
108 simp23 ${⊢}\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\wedge {y}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\wedge {z}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}{↾}_{\mathrm{cat}}{H}\right){y}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({C}{↾}_{\mathrm{cat}}{H}\right){z}\right)\right)\right)\to {z}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}$
109 108 103 eleqtrrd ${⊢}\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\wedge {y}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\wedge {z}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}{↾}_{\mathrm{cat}}{H}\right){y}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({C}{↾}_{\mathrm{cat}}{H}\right){z}\right)\right)\right)\to {z}\in \mathrm{dom}\mathrm{dom}{H}$
110 simp3l ${⊢}\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\wedge {y}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\wedge {z}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}{↾}_{\mathrm{cat}}{H}\right){y}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({C}{↾}_{\mathrm{cat}}{H}\right){z}\right)\right)\right)\to {f}\in \left({x}\mathrm{Hom}\left({C}{↾}_{\mathrm{cat}}{H}\right){y}\right)$
111 71 3ad2ant1 ${⊢}\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\wedge {y}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\wedge {z}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}{↾}_{\mathrm{cat}}{H}\right){y}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({C}{↾}_{\mathrm{cat}}{H}\right){z}\right)\right)\right)\to {H}=\mathrm{Hom}\left({C}{↾}_{\mathrm{cat}}{H}\right)$
112 111 oveqd ${⊢}\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\wedge {y}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\wedge {z}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}{↾}_{\mathrm{cat}}{H}\right){y}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({C}{↾}_{\mathrm{cat}}{H}\right){z}\right)\right)\right)\to {x}{H}{y}={x}\mathrm{Hom}\left({C}{↾}_{\mathrm{cat}}{H}\right){y}$
113 110 112 eleqtrrd ${⊢}\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\wedge {y}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\wedge {z}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}{↾}_{\mathrm{cat}}{H}\right){y}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({C}{↾}_{\mathrm{cat}}{H}\right){z}\right)\right)\right)\to {f}\in \left({x}{H}{y}\right)$
114 simp3r ${⊢}\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\wedge {y}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\wedge {z}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}{↾}_{\mathrm{cat}}{H}\right){y}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({C}{↾}_{\mathrm{cat}}{H}\right){z}\right)\right)\right)\to {g}\in \left({y}\mathrm{Hom}\left({C}{↾}_{\mathrm{cat}}{H}\right){z}\right)$
115 111 oveqd ${⊢}\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\wedge {y}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\wedge {z}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}{↾}_{\mathrm{cat}}{H}\right){y}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({C}{↾}_{\mathrm{cat}}{H}\right){z}\right)\right)\right)\to {y}{H}{z}={y}\mathrm{Hom}\left({C}{↾}_{\mathrm{cat}}{H}\right){z}$
116 114 115 eleqtrrd ${⊢}\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\wedge {y}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\wedge {z}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}{↾}_{\mathrm{cat}}{H}\right){y}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({C}{↾}_{\mathrm{cat}}{H}\right){z}\right)\right)\right)\to {g}\in \left({y}{H}{z}\right)$
117 100 101 104 105 107 109 113 116 subccocl ${⊢}\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\wedge {y}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\wedge {z}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}{↾}_{\mathrm{cat}}{H}\right){y}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({C}{↾}_{\mathrm{cat}}{H}\right){z}\right)\right)\right)\to {g}\left(⟨{x},{y}⟩\mathrm{comp}\left({C}\right){z}\right){f}\in \left({x}{H}{z}\right)$
118 117 fvresd ${⊢}\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\wedge {y}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\wedge {z}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}{↾}_{\mathrm{cat}}{H}\right){y}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({C}{↾}_{\mathrm{cat}}{H}\right){z}\right)\right)\right)\to \left({\left({x}{2}^{nd}\left({F}\right){z}\right)↾}_{\left({x}{H}{z}\right)}\right)\left({g}\left(⟨{x},{y}⟩\mathrm{comp}\left({C}\right){z}\right){f}\right)=\left({x}{2}^{nd}\left({F}\right){z}\right)\left({g}\left(⟨{x},{y}⟩\mathrm{comp}\left({C}\right){z}\right){f}\right)$
119 31 3ad2ant1 ${⊢}\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\wedge {y}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\wedge {z}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}{↾}_{\mathrm{cat}}{H}\right){y}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({C}{↾}_{\mathrm{cat}}{H}\right){z}\right)\right)\right)\to {1}^{st}\left({F}\right)\left({C}\mathrm{Func}{D}\right){2}^{nd}\left({F}\right)$
120 35 3ad2ant1 ${⊢}\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\wedge {y}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\wedge {z}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}{↾}_{\mathrm{cat}}{H}\right){y}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({C}{↾}_{\mathrm{cat}}{H}\right){z}\right)\right)\right)\to \mathrm{dom}\mathrm{dom}{H}\subseteq {\mathrm{Base}}_{{C}}$
121 120 104 sseldd ${⊢}\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\wedge {y}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\wedge {z}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}{↾}_{\mathrm{cat}}{H}\right){y}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({C}{↾}_{\mathrm{cat}}{H}\right){z}\right)\right)\right)\to {x}\in {\mathrm{Base}}_{{C}}$
122 120 107 sseldd ${⊢}\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\wedge {y}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\wedge {z}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}{↾}_{\mathrm{cat}}{H}\right){y}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({C}{↾}_{\mathrm{cat}}{H}\right){z}\right)\right)\right)\to {y}\in {\mathrm{Base}}_{{C}}$
123 120 109 sseldd ${⊢}\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\wedge {y}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\wedge {z}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}{↾}_{\mathrm{cat}}{H}\right){y}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({C}{↾}_{\mathrm{cat}}{H}\right){z}\right)\right)\right)\to {z}\in {\mathrm{Base}}_{{C}}$
124 100 101 52 104 107 subcss2 ${⊢}\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\wedge {y}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\wedge {z}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}{↾}_{\mathrm{cat}}{H}\right){y}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({C}{↾}_{\mathrm{cat}}{H}\right){z}\right)\right)\right)\to {x}{H}{y}\subseteq {x}\mathrm{Hom}\left({C}\right){y}$
125 124 113 sseldd ${⊢}\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\wedge {y}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\wedge {z}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}{↾}_{\mathrm{cat}}{H}\right){y}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({C}{↾}_{\mathrm{cat}}{H}\right){z}\right)\right)\right)\to {f}\in \left({x}\mathrm{Hom}\left({C}\right){y}\right)$
126 100 101 52 107 109 subcss2 ${⊢}\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\wedge {y}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\wedge {z}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}{↾}_{\mathrm{cat}}{H}\right){y}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({C}{↾}_{\mathrm{cat}}{H}\right){z}\right)\right)\right)\to {y}{H}{z}\subseteq {y}\mathrm{Hom}\left({C}\right){z}$
127 126 116 sseldd ${⊢}\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\wedge {y}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\wedge {z}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}{↾}_{\mathrm{cat}}{H}\right){y}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({C}{↾}_{\mathrm{cat}}{H}\right){z}\right)\right)\right)\to {g}\in \left({y}\mathrm{Hom}\left({C}\right){z}\right)$
128 28 52 105 22 119 121 122 123 125 127 funcco ${⊢}\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\wedge {y}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\wedge {z}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}{↾}_{\mathrm{cat}}{H}\right){y}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({C}{↾}_{\mathrm{cat}}{H}\right){z}\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)$
129 118 128 eqtrd ${⊢}\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\wedge {y}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\wedge {z}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}{↾}_{\mathrm{cat}}{H}\right){y}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({C}{↾}_{\mathrm{cat}}{H}\right){z}\right)\right)\right)\to \left({\left({x}{2}^{nd}\left({F}\right){z}\right)↾}_{\left({x}{H}{z}\right)}\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)$
130 1 3ad2ant1 ${⊢}\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\wedge {y}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\wedge {z}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}{↾}_{\mathrm{cat}}{H}\right){y}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({C}{↾}_{\mathrm{cat}}{H}\right){z}\right)\right)\right)\to {F}\in \left({C}\mathrm{Func}{D}\right)$
131 130 100 101 104 109 resf2nd ${⊢}\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\wedge {y}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\wedge {z}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}{↾}_{\mathrm{cat}}{H}\right){y}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({C}{↾}_{\mathrm{cat}}{H}\right){z}\right)\right)\right)\to {x}{2}^{nd}\left({F}{↾}_{f}{H}\right){z}={\left({x}{2}^{nd}\left({F}\right){z}\right)↾}_{\left({x}{H}{z}\right)}$
132 23 28 37 34 35 105 rescco ${⊢}{\phi }\to \mathrm{comp}\left({C}\right)=\mathrm{comp}\left({C}{↾}_{\mathrm{cat}}{H}\right)$
133 132 3ad2ant1 ${⊢}\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\wedge {y}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\wedge {z}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}{↾}_{\mathrm{cat}}{H}\right){y}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({C}{↾}_{\mathrm{cat}}{H}\right){z}\right)\right)\right)\to \mathrm{comp}\left({C}\right)=\mathrm{comp}\left({C}{↾}_{\mathrm{cat}}{H}\right)$
134 133 eqcomd ${⊢}\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\wedge {y}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\wedge {z}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}{↾}_{\mathrm{cat}}{H}\right){y}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({C}{↾}_{\mathrm{cat}}{H}\right){z}\right)\right)\right)\to \mathrm{comp}\left({C}{↾}_{\mathrm{cat}}{H}\right)=\mathrm{comp}\left({C}\right)$
135 134 oveqd ${⊢}\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\wedge {y}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\wedge {z}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}{↾}_{\mathrm{cat}}{H}\right){y}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({C}{↾}_{\mathrm{cat}}{H}\right){z}\right)\right)\right)\to ⟨{x},{y}⟩\mathrm{comp}\left({C}{↾}_{\mathrm{cat}}{H}\right){z}=⟨{x},{y}⟩\mathrm{comp}\left({C}\right){z}$
136 135 oveqd ${⊢}\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\wedge {y}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\wedge {z}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}{↾}_{\mathrm{cat}}{H}\right){y}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({C}{↾}_{\mathrm{cat}}{H}\right){z}\right)\right)\right)\to {g}\left(⟨{x},{y}⟩\mathrm{comp}\left({C}{↾}_{\mathrm{cat}}{H}\right){z}\right){f}={g}\left(⟨{x},{y}⟩\mathrm{comp}\left({C}\right){z}\right){f}$
137 131 136 fveq12d ${⊢}\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\wedge {y}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\wedge {z}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}{↾}_{\mathrm{cat}}{H}\right){y}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({C}{↾}_{\mathrm{cat}}{H}\right){z}\right)\right)\right)\to \left({x}{2}^{nd}\left({F}{↾}_{f}{H}\right){z}\right)\left({g}\left(⟨{x},{y}⟩\mathrm{comp}\left({C}{↾}_{\mathrm{cat}}{H}\right){z}\right){f}\right)=\left({\left({x}{2}^{nd}\left({F}\right){z}\right)↾}_{\left({x}{H}{z}\right)}\right)\left({g}\left(⟨{x},{y}⟩\mathrm{comp}\left({C}\right){z}\right){f}\right)$
138 104 fvresd ${⊢}\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\wedge {y}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\wedge {z}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}{↾}_{\mathrm{cat}}{H}\right){y}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({C}{↾}_{\mathrm{cat}}{H}\right){z}\right)\right)\right)\to \left({{1}^{st}\left({F}\right)↾}_{\mathrm{dom}\mathrm{dom}{H}}\right)\left({x}\right)={1}^{st}\left({F}\right)\left({x}\right)$
139 107 fvresd ${⊢}\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\wedge {y}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\wedge {z}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}{↾}_{\mathrm{cat}}{H}\right){y}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({C}{↾}_{\mathrm{cat}}{H}\right){z}\right)\right)\right)\to \left({{1}^{st}\left({F}\right)↾}_{\mathrm{dom}\mathrm{dom}{H}}\right)\left({y}\right)={1}^{st}\left({F}\right)\left({y}\right)$
140 138 139 opeq12d ${⊢}\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\wedge {y}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\wedge {z}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}{↾}_{\mathrm{cat}}{H}\right){y}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({C}{↾}_{\mathrm{cat}}{H}\right){z}\right)\right)\right)\to ⟨\left({{1}^{st}\left({F}\right)↾}_{\mathrm{dom}\mathrm{dom}{H}}\right)\left({x}\right),\left({{1}^{st}\left({F}\right)↾}_{\mathrm{dom}\mathrm{dom}{H}}\right)\left({y}\right)⟩=⟨{1}^{st}\left({F}\right)\left({x}\right),{1}^{st}\left({F}\right)\left({y}\right)⟩$
141 109 fvresd ${⊢}\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\wedge {y}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\wedge {z}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}{↾}_{\mathrm{cat}}{H}\right){y}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({C}{↾}_{\mathrm{cat}}{H}\right){z}\right)\right)\right)\to \left({{1}^{st}\left({F}\right)↾}_{\mathrm{dom}\mathrm{dom}{H}}\right)\left({z}\right)={1}^{st}\left({F}\right)\left({z}\right)$
142 140 141 oveq12d ${⊢}\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\wedge {y}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\wedge {z}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}{↾}_{\mathrm{cat}}{H}\right){y}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({C}{↾}_{\mathrm{cat}}{H}\right){z}\right)\right)\right)\to ⟨\left({{1}^{st}\left({F}\right)↾}_{\mathrm{dom}\mathrm{dom}{H}}\right)\left({x}\right),\left({{1}^{st}\left({F}\right)↾}_{\mathrm{dom}\mathrm{dom}{H}}\right)\left({y}\right)⟩\mathrm{comp}\left({D}\right)\left({{1}^{st}\left({F}\right)↾}_{\mathrm{dom}\mathrm{dom}{H}}\right)\left({z}\right)=⟨{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)$
143 130 100 101 107 109 resf2nd ${⊢}\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\wedge {y}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\wedge {z}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}{↾}_{\mathrm{cat}}{H}\right){y}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({C}{↾}_{\mathrm{cat}}{H}\right){z}\right)\right)\right)\to {y}{2}^{nd}\left({F}{↾}_{f}{H}\right){z}={\left({y}{2}^{nd}\left({F}\right){z}\right)↾}_{\left({y}{H}{z}\right)}$
144 143 fveq1d ${⊢}\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\wedge {y}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\wedge {z}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}{↾}_{\mathrm{cat}}{H}\right){y}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({C}{↾}_{\mathrm{cat}}{H}\right){z}\right)\right)\right)\to \left({y}{2}^{nd}\left({F}{↾}_{f}{H}\right){z}\right)\left({g}\right)=\left({\left({y}{2}^{nd}\left({F}\right){z}\right)↾}_{\left({y}{H}{z}\right)}\right)\left({g}\right)$
145 116 fvresd ${⊢}\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\wedge {y}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\wedge {z}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}{↾}_{\mathrm{cat}}{H}\right){y}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({C}{↾}_{\mathrm{cat}}{H}\right){z}\right)\right)\right)\to \left({\left({y}{2}^{nd}\left({F}\right){z}\right)↾}_{\left({y}{H}{z}\right)}\right)\left({g}\right)=\left({y}{2}^{nd}\left({F}\right){z}\right)\left({g}\right)$
146 144 145 eqtrd ${⊢}\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\wedge {y}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\wedge {z}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}{↾}_{\mathrm{cat}}{H}\right){y}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({C}{↾}_{\mathrm{cat}}{H}\right){z}\right)\right)\right)\to \left({y}{2}^{nd}\left({F}{↾}_{f}{H}\right){z}\right)\left({g}\right)=\left({y}{2}^{nd}\left({F}\right){z}\right)\left({g}\right)$
147 130 100 101 104 107 resf2nd ${⊢}\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\wedge {y}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\wedge {z}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}{↾}_{\mathrm{cat}}{H}\right){y}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({C}{↾}_{\mathrm{cat}}{H}\right){z}\right)\right)\right)\to {x}{2}^{nd}\left({F}{↾}_{f}{H}\right){y}={\left({x}{2}^{nd}\left({F}\right){y}\right)↾}_{\left({x}{H}{y}\right)}$
148 147 fveq1d ${⊢}\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\wedge {y}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\wedge {z}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}{↾}_{\mathrm{cat}}{H}\right){y}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({C}{↾}_{\mathrm{cat}}{H}\right){z}\right)\right)\right)\to \left({x}{2}^{nd}\left({F}{↾}_{f}{H}\right){y}\right)\left({f}\right)=\left({\left({x}{2}^{nd}\left({F}\right){y}\right)↾}_{\left({x}{H}{y}\right)}\right)\left({f}\right)$
149 113 fvresd ${⊢}\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\wedge {y}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\wedge {z}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}{↾}_{\mathrm{cat}}{H}\right){y}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({C}{↾}_{\mathrm{cat}}{H}\right){z}\right)\right)\right)\to \left({\left({x}{2}^{nd}\left({F}\right){y}\right)↾}_{\left({x}{H}{y}\right)}\right)\left({f}\right)=\left({x}{2}^{nd}\left({F}\right){y}\right)\left({f}\right)$
150 148 149 eqtrd ${⊢}\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\wedge {y}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\wedge {z}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}{↾}_{\mathrm{cat}}{H}\right){y}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({C}{↾}_{\mathrm{cat}}{H}\right){z}\right)\right)\right)\to \left({x}{2}^{nd}\left({F}{↾}_{f}{H}\right){y}\right)\left({f}\right)=\left({x}{2}^{nd}\left({F}\right){y}\right)\left({f}\right)$
151 142 146 150 oveq123d ${⊢}\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\wedge {y}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\wedge {z}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}{↾}_{\mathrm{cat}}{H}\right){y}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({C}{↾}_{\mathrm{cat}}{H}\right){z}\right)\right)\right)\to \left({y}{2}^{nd}\left({F}{↾}_{f}{H}\right){z}\right)\left({g}\right)\left(⟨\left({{1}^{st}\left({F}\right)↾}_{\mathrm{dom}\mathrm{dom}{H}}\right)\left({x}\right),\left({{1}^{st}\left({F}\right)↾}_{\mathrm{dom}\mathrm{dom}{H}}\right)\left({y}\right)⟩\mathrm{comp}\left({D}\right)\left({{1}^{st}\left({F}\right)↾}_{\mathrm{dom}\mathrm{dom}{H}}\right)\left({z}\right)\right)\left({x}{2}^{nd}\left({F}{↾}_{f}{H}\right){y}\right)\left({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)$
152 129 137 151 3eqtr4d ${⊢}\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\wedge {y}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\wedge {z}\in {\mathrm{Base}}_{\left({C}{↾}_{\mathrm{cat}}{H}\right)}\right)\wedge \left({f}\in \left({x}\mathrm{Hom}\left({C}{↾}_{\mathrm{cat}}{H}\right){y}\right)\wedge {g}\in \left({y}\mathrm{Hom}\left({C}{↾}_{\mathrm{cat}}{H}\right){z}\right)\right)\right)\to \left({x}{2}^{nd}\left({F}{↾}_{f}{H}\right){z}\right)\left({g}\left(⟨{x},{y}⟩\mathrm{comp}\left({C}{↾}_{\mathrm{cat}}{H}\right){z}\right){f}\right)=\left({y}{2}^{nd}\left({F}{↾}_{f}{H}\right){z}\right)\left({g}\right)\left(⟨\left({{1}^{st}\left({F}\right)↾}_{\mathrm{dom}\mathrm{dom}{H}}\right)\left({x}\right),\left({{1}^{st}\left({F}\right)↾}_{\mathrm{dom}\mathrm{dom}{H}}\right)\left({y}\right)⟩\mathrm{comp}\left({D}\right)\left({{1}^{st}\left({F}\right)↾}_{\mathrm{dom}\mathrm{dom}{H}}\right)\left({z}\right)\right)\left({x}{2}^{nd}\left({F}{↾}_{f}{H}\right){y}\right)\left({f}\right)$
153 15 16 17 18 19 20 21 22 24 27 40 51 79 99 152 isfuncd ${⊢}{\phi }\to \left({{1}^{st}\left({F}\right)↾}_{\mathrm{dom}\mathrm{dom}{H}}\right)\left(\left({C}{↾}_{\mathrm{cat}}{H}\right)\mathrm{Func}{D}\right){2}^{nd}\left({F}{↾}_{f}{H}\right)$
154 df-br ${⊢}\left({{1}^{st}\left({F}\right)↾}_{\mathrm{dom}\mathrm{dom}{H}}\right)\left(\left({C}{↾}_{\mathrm{cat}}{H}\right)\mathrm{Func}{D}\right){2}^{nd}\left({F}{↾}_{f}{H}\right)↔⟨{{1}^{st}\left({F}\right)↾}_{\mathrm{dom}\mathrm{dom}{H}},{2}^{nd}\left({F}{↾}_{f}{H}\right)⟩\in \left(\left({C}{↾}_{\mathrm{cat}}{H}\right)\mathrm{Func}{D}\right)$
155 153 154 sylib ${⊢}{\phi }\to ⟨{{1}^{st}\left({F}\right)↾}_{\mathrm{dom}\mathrm{dom}{H}},{2}^{nd}\left({F}{↾}_{f}{H}\right)⟩\in \left(\left({C}{↾}_{\mathrm{cat}}{H}\right)\mathrm{Func}{D}\right)$
156 14 155 eqeltrd ${⊢}{\phi }\to {F}{↾}_{f}{H}\in \left(\left({C}{↾}_{\mathrm{cat}}{H}\right)\mathrm{Func}{D}\right)$