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 ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
funcres.h ⊢ ( 𝜑 → 𝐻 ∈ ( Subcat ‘ 𝐶 ) )
Assertion funcres ( 𝜑 → ( 𝐹 ↾f 𝐻 ) ∈ ( ( 𝐶 ↾cat 𝐻 ) Func 𝐷 ) )

Proof

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