Metamath Proof Explorer


Theorem funcres2b

Description: Condition for a functor to also be a functor into the restriction. (Contributed by Mario Carneiro, 6-Jan-2017)

Ref Expression
Hypotheses funcres2b.a 𝐴 = ( Base ‘ 𝐶 )
funcres2b.h 𝐻 = ( Hom ‘ 𝐶 )
funcres2b.r ( 𝜑𝑅 ∈ ( Subcat ‘ 𝐷 ) )
funcres2b.s ( 𝜑𝑅 Fn ( 𝑆 × 𝑆 ) )
funcres2b.1 ( 𝜑𝐹 : 𝐴𝑆 )
funcres2b.2 ( ( 𝜑 ∧ ( 𝑥𝐴𝑦𝐴 ) ) → ( 𝑥 𝐺 𝑦 ) : 𝑌 ⟶ ( ( 𝐹𝑥 ) 𝑅 ( 𝐹𝑦 ) ) )
Assertion funcres2b ( 𝜑 → ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺𝐹 ( 𝐶 Func ( 𝐷cat 𝑅 ) ) 𝐺 ) )

Proof

Step Hyp Ref Expression
1 funcres2b.a 𝐴 = ( Base ‘ 𝐶 )
2 funcres2b.h 𝐻 = ( Hom ‘ 𝐶 )
3 funcres2b.r ( 𝜑𝑅 ∈ ( Subcat ‘ 𝐷 ) )
4 funcres2b.s ( 𝜑𝑅 Fn ( 𝑆 × 𝑆 ) )
5 funcres2b.1 ( 𝜑𝐹 : 𝐴𝑆 )
6 funcres2b.2 ( ( 𝜑 ∧ ( 𝑥𝐴𝑦𝐴 ) ) → ( 𝑥 𝐺 𝑦 ) : 𝑌 ⟶ ( ( 𝐹𝑥 ) 𝑅 ( 𝐹𝑦 ) ) )
7 df-br ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ↔ ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝐶 Func 𝐷 ) )
8 funcrcl ( ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝐶 Func 𝐷 ) → ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) )
9 7 8 sylbi ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 → ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) )
10 9 simpld ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺𝐶 ∈ Cat )
11 10 a1i ( 𝜑 → ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺𝐶 ∈ Cat ) )
12 df-br ( 𝐹 ( 𝐶 Func ( 𝐷cat 𝑅 ) ) 𝐺 ↔ ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝐶 Func ( 𝐷cat 𝑅 ) ) )
13 funcrcl ( ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝐶 Func ( 𝐷cat 𝑅 ) ) → ( 𝐶 ∈ Cat ∧ ( 𝐷cat 𝑅 ) ∈ Cat ) )
14 12 13 sylbi ( 𝐹 ( 𝐶 Func ( 𝐷cat 𝑅 ) ) 𝐺 → ( 𝐶 ∈ Cat ∧ ( 𝐷cat 𝑅 ) ∈ Cat ) )
15 14 simpld ( 𝐹 ( 𝐶 Func ( 𝐷cat 𝑅 ) ) 𝐺𝐶 ∈ Cat )
16 15 a1i ( 𝜑 → ( 𝐹 ( 𝐶 Func ( 𝐷cat 𝑅 ) ) 𝐺𝐶 ∈ Cat ) )
17 eqid ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
18 3 4 17 subcss1 ( 𝜑𝑆 ⊆ ( Base ‘ 𝐷 ) )
19 5 18 fssd ( 𝜑𝐹 : 𝐴 ⟶ ( Base ‘ 𝐷 ) )
20 eqid ( 𝐷cat 𝑅 ) = ( 𝐷cat 𝑅 )
21 subcrcl ( 𝑅 ∈ ( Subcat ‘ 𝐷 ) → 𝐷 ∈ Cat )
22 3 21 syl ( 𝜑𝐷 ∈ Cat )
23 20 17 22 4 18 rescbas ( 𝜑𝑆 = ( Base ‘ ( 𝐷cat 𝑅 ) ) )
24 23 feq3d ( 𝜑 → ( 𝐹 : 𝐴𝑆𝐹 : 𝐴 ⟶ ( Base ‘ ( 𝐷cat 𝑅 ) ) ) )
25 5 24 mpbid ( 𝜑𝐹 : 𝐴 ⟶ ( Base ‘ ( 𝐷cat 𝑅 ) ) )
26 19 25 2thd ( 𝜑 → ( 𝐹 : 𝐴 ⟶ ( Base ‘ 𝐷 ) ↔ 𝐹 : 𝐴 ⟶ ( Base ‘ ( 𝐷cat 𝑅 ) ) ) )
27 26 adantr ( ( 𝜑𝐶 ∈ Cat ) → ( 𝐹 : 𝐴 ⟶ ( Base ‘ 𝐷 ) ↔ 𝐹 : 𝐴 ⟶ ( Base ‘ ( 𝐷cat 𝑅 ) ) ) )
28 6 adantlr ( ( ( 𝜑𝐶 ∈ Cat ) ∧ ( 𝑥𝐴𝑦𝐴 ) ) → ( 𝑥 𝐺 𝑦 ) : 𝑌 ⟶ ( ( 𝐹𝑥 ) 𝑅 ( 𝐹𝑦 ) ) )
29 28 frnd ( ( ( 𝜑𝐶 ∈ Cat ) ∧ ( 𝑥𝐴𝑦𝐴 ) ) → ran ( 𝑥 𝐺 𝑦 ) ⊆ ( ( 𝐹𝑥 ) 𝑅 ( 𝐹𝑦 ) ) )
30 3 ad2antrr ( ( ( 𝜑𝐶 ∈ Cat ) ∧ ( 𝑥𝐴𝑦𝐴 ) ) → 𝑅 ∈ ( Subcat ‘ 𝐷 ) )
31 4 ad2antrr ( ( ( 𝜑𝐶 ∈ Cat ) ∧ ( 𝑥𝐴𝑦𝐴 ) ) → 𝑅 Fn ( 𝑆 × 𝑆 ) )
32 eqid ( Hom ‘ 𝐷 ) = ( Hom ‘ 𝐷 )
33 5 ad2antrr ( ( ( 𝜑𝐶 ∈ Cat ) ∧ ( 𝑥𝐴𝑦𝐴 ) ) → 𝐹 : 𝐴𝑆 )
34 simprl ( ( ( 𝜑𝐶 ∈ Cat ) ∧ ( 𝑥𝐴𝑦𝐴 ) ) → 𝑥𝐴 )
35 33 34 ffvelrnd ( ( ( 𝜑𝐶 ∈ Cat ) ∧ ( 𝑥𝐴𝑦𝐴 ) ) → ( 𝐹𝑥 ) ∈ 𝑆 )
36 simprr ( ( ( 𝜑𝐶 ∈ Cat ) ∧ ( 𝑥𝐴𝑦𝐴 ) ) → 𝑦𝐴 )
37 33 36 ffvelrnd ( ( ( 𝜑𝐶 ∈ Cat ) ∧ ( 𝑥𝐴𝑦𝐴 ) ) → ( 𝐹𝑦 ) ∈ 𝑆 )
38 30 31 32 35 37 subcss2 ( ( ( 𝜑𝐶 ∈ Cat ) ∧ ( 𝑥𝐴𝑦𝐴 ) ) → ( ( 𝐹𝑥 ) 𝑅 ( 𝐹𝑦 ) ) ⊆ ( ( 𝐹𝑥 ) ( Hom ‘ 𝐷 ) ( 𝐹𝑦 ) ) )
39 29 38 sstrd ( ( ( 𝜑𝐶 ∈ Cat ) ∧ ( 𝑥𝐴𝑦𝐴 ) ) → ran ( 𝑥 𝐺 𝑦 ) ⊆ ( ( 𝐹𝑥 ) ( Hom ‘ 𝐷 ) ( 𝐹𝑦 ) ) )
40 39 29 2thd ( ( ( 𝜑𝐶 ∈ Cat ) ∧ ( 𝑥𝐴𝑦𝐴 ) ) → ( ran ( 𝑥 𝐺 𝑦 ) ⊆ ( ( 𝐹𝑥 ) ( Hom ‘ 𝐷 ) ( 𝐹𝑦 ) ) ↔ ran ( 𝑥 𝐺 𝑦 ) ⊆ ( ( 𝐹𝑥 ) 𝑅 ( 𝐹𝑦 ) ) ) )
41 40 anbi2d ( ( ( 𝜑𝐶 ∈ Cat ) ∧ ( 𝑥𝐴𝑦𝐴 ) ) → ( ( ( 𝑥 𝐺 𝑦 ) Fn ( 𝑥 𝐻 𝑦 ) ∧ ran ( 𝑥 𝐺 𝑦 ) ⊆ ( ( 𝐹𝑥 ) ( Hom ‘ 𝐷 ) ( 𝐹𝑦 ) ) ) ↔ ( ( 𝑥 𝐺 𝑦 ) Fn ( 𝑥 𝐻 𝑦 ) ∧ ran ( 𝑥 𝐺 𝑦 ) ⊆ ( ( 𝐹𝑥 ) 𝑅 ( 𝐹𝑦 ) ) ) ) )
42 df-f ( ( 𝑥 𝐺 𝑦 ) : ( 𝑥 𝐻 𝑦 ) ⟶ ( ( 𝐹𝑥 ) ( Hom ‘ 𝐷 ) ( 𝐹𝑦 ) ) ↔ ( ( 𝑥 𝐺 𝑦 ) Fn ( 𝑥 𝐻 𝑦 ) ∧ ran ( 𝑥 𝐺 𝑦 ) ⊆ ( ( 𝐹𝑥 ) ( Hom ‘ 𝐷 ) ( 𝐹𝑦 ) ) ) )
43 df-f ( ( 𝑥 𝐺 𝑦 ) : ( 𝑥 𝐻 𝑦 ) ⟶ ( ( 𝐹𝑥 ) 𝑅 ( 𝐹𝑦 ) ) ↔ ( ( 𝑥 𝐺 𝑦 ) Fn ( 𝑥 𝐻 𝑦 ) ∧ ran ( 𝑥 𝐺 𝑦 ) ⊆ ( ( 𝐹𝑥 ) 𝑅 ( 𝐹𝑦 ) ) ) )
44 41 42 43 3bitr4g ( ( ( 𝜑𝐶 ∈ Cat ) ∧ ( 𝑥𝐴𝑦𝐴 ) ) → ( ( 𝑥 𝐺 𝑦 ) : ( 𝑥 𝐻 𝑦 ) ⟶ ( ( 𝐹𝑥 ) ( Hom ‘ 𝐷 ) ( 𝐹𝑦 ) ) ↔ ( 𝑥 𝐺 𝑦 ) : ( 𝑥 𝐻 𝑦 ) ⟶ ( ( 𝐹𝑥 ) 𝑅 ( 𝐹𝑦 ) ) ) )
45 20 17 22 4 18 reschom ( 𝜑𝑅 = ( Hom ‘ ( 𝐷cat 𝑅 ) ) )
46 45 ad2antrr ( ( ( 𝜑𝐶 ∈ Cat ) ∧ ( 𝑥𝐴𝑦𝐴 ) ) → 𝑅 = ( Hom ‘ ( 𝐷cat 𝑅 ) ) )
47 46 oveqd ( ( ( 𝜑𝐶 ∈ Cat ) ∧ ( 𝑥𝐴𝑦𝐴 ) ) → ( ( 𝐹𝑥 ) 𝑅 ( 𝐹𝑦 ) ) = ( ( 𝐹𝑥 ) ( Hom ‘ ( 𝐷cat 𝑅 ) ) ( 𝐹𝑦 ) ) )
48 47 feq3d ( ( ( 𝜑𝐶 ∈ Cat ) ∧ ( 𝑥𝐴𝑦𝐴 ) ) → ( ( 𝑥 𝐺 𝑦 ) : ( 𝑥 𝐻 𝑦 ) ⟶ ( ( 𝐹𝑥 ) 𝑅 ( 𝐹𝑦 ) ) ↔ ( 𝑥 𝐺 𝑦 ) : ( 𝑥 𝐻 𝑦 ) ⟶ ( ( 𝐹𝑥 ) ( Hom ‘ ( 𝐷cat 𝑅 ) ) ( 𝐹𝑦 ) ) ) )
49 44 48 bitrd ( ( ( 𝜑𝐶 ∈ Cat ) ∧ ( 𝑥𝐴𝑦𝐴 ) ) → ( ( 𝑥 𝐺 𝑦 ) : ( 𝑥 𝐻 𝑦 ) ⟶ ( ( 𝐹𝑥 ) ( Hom ‘ 𝐷 ) ( 𝐹𝑦 ) ) ↔ ( 𝑥 𝐺 𝑦 ) : ( 𝑥 𝐻 𝑦 ) ⟶ ( ( 𝐹𝑥 ) ( Hom ‘ ( 𝐷cat 𝑅 ) ) ( 𝐹𝑦 ) ) ) )
50 49 ralrimivva ( ( 𝜑𝐶 ∈ Cat ) → ∀ 𝑥𝐴𝑦𝐴 ( ( 𝑥 𝐺 𝑦 ) : ( 𝑥 𝐻 𝑦 ) ⟶ ( ( 𝐹𝑥 ) ( Hom ‘ 𝐷 ) ( 𝐹𝑦 ) ) ↔ ( 𝑥 𝐺 𝑦 ) : ( 𝑥 𝐻 𝑦 ) ⟶ ( ( 𝐹𝑥 ) ( Hom ‘ ( 𝐷cat 𝑅 ) ) ( 𝐹𝑦 ) ) ) )
51 fveq2 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝐺𝑧 ) = ( 𝐺 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) )
52 df-ov ( 𝑥 𝐺 𝑦 ) = ( 𝐺 ‘ ⟨ 𝑥 , 𝑦 ⟩ )
53 51 52 eqtr4di ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝐺𝑧 ) = ( 𝑥 𝐺 𝑦 ) )
54 vex 𝑥 ∈ V
55 vex 𝑦 ∈ V
56 54 55 op1std ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 1st𝑧 ) = 𝑥 )
57 56 fveq2d ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝐹 ‘ ( 1st𝑧 ) ) = ( 𝐹𝑥 ) )
58 54 55 op2ndd ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 2nd𝑧 ) = 𝑦 )
59 58 fveq2d ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝐹 ‘ ( 2nd𝑧 ) ) = ( 𝐹𝑦 ) )
60 57 59 oveq12d ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( 𝐹 ‘ ( 1st𝑧 ) ) ( Hom ‘ 𝐷 ) ( 𝐹 ‘ ( 2nd𝑧 ) ) ) = ( ( 𝐹𝑥 ) ( Hom ‘ 𝐷 ) ( 𝐹𝑦 ) ) )
61 fveq2 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝐻𝑧 ) = ( 𝐻 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) )
62 df-ov ( 𝑥 𝐻 𝑦 ) = ( 𝐻 ‘ ⟨ 𝑥 , 𝑦 ⟩ )
63 61 62 eqtr4di ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝐻𝑧 ) = ( 𝑥 𝐻 𝑦 ) )
64 60 63 oveq12d ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( ( 𝐹 ‘ ( 1st𝑧 ) ) ( Hom ‘ 𝐷 ) ( 𝐹 ‘ ( 2nd𝑧 ) ) ) ↑m ( 𝐻𝑧 ) ) = ( ( ( 𝐹𝑥 ) ( Hom ‘ 𝐷 ) ( 𝐹𝑦 ) ) ↑m ( 𝑥 𝐻 𝑦 ) ) )
65 53 64 eleq12d ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( 𝐺𝑧 ) ∈ ( ( ( 𝐹 ‘ ( 1st𝑧 ) ) ( Hom ‘ 𝐷 ) ( 𝐹 ‘ ( 2nd𝑧 ) ) ) ↑m ( 𝐻𝑧 ) ) ↔ ( 𝑥 𝐺 𝑦 ) ∈ ( ( ( 𝐹𝑥 ) ( Hom ‘ 𝐷 ) ( 𝐹𝑦 ) ) ↑m ( 𝑥 𝐻 𝑦 ) ) ) )
66 ovex ( ( 𝐹𝑥 ) ( Hom ‘ 𝐷 ) ( 𝐹𝑦 ) ) ∈ V
67 ovex ( 𝑥 𝐻 𝑦 ) ∈ V
68 66 67 elmap ( ( 𝑥 𝐺 𝑦 ) ∈ ( ( ( 𝐹𝑥 ) ( Hom ‘ 𝐷 ) ( 𝐹𝑦 ) ) ↑m ( 𝑥 𝐻 𝑦 ) ) ↔ ( 𝑥 𝐺 𝑦 ) : ( 𝑥 𝐻 𝑦 ) ⟶ ( ( 𝐹𝑥 ) ( Hom ‘ 𝐷 ) ( 𝐹𝑦 ) ) )
69 65 68 bitrdi ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( 𝐺𝑧 ) ∈ ( ( ( 𝐹 ‘ ( 1st𝑧 ) ) ( Hom ‘ 𝐷 ) ( 𝐹 ‘ ( 2nd𝑧 ) ) ) ↑m ( 𝐻𝑧 ) ) ↔ ( 𝑥 𝐺 𝑦 ) : ( 𝑥 𝐻 𝑦 ) ⟶ ( ( 𝐹𝑥 ) ( Hom ‘ 𝐷 ) ( 𝐹𝑦 ) ) ) )
70 57 59 oveq12d ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( 𝐹 ‘ ( 1st𝑧 ) ) ( Hom ‘ ( 𝐷cat 𝑅 ) ) ( 𝐹 ‘ ( 2nd𝑧 ) ) ) = ( ( 𝐹𝑥 ) ( Hom ‘ ( 𝐷cat 𝑅 ) ) ( 𝐹𝑦 ) ) )
71 70 63 oveq12d ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( ( 𝐹 ‘ ( 1st𝑧 ) ) ( Hom ‘ ( 𝐷cat 𝑅 ) ) ( 𝐹 ‘ ( 2nd𝑧 ) ) ) ↑m ( 𝐻𝑧 ) ) = ( ( ( 𝐹𝑥 ) ( Hom ‘ ( 𝐷cat 𝑅 ) ) ( 𝐹𝑦 ) ) ↑m ( 𝑥 𝐻 𝑦 ) ) )
72 53 71 eleq12d ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( 𝐺𝑧 ) ∈ ( ( ( 𝐹 ‘ ( 1st𝑧 ) ) ( Hom ‘ ( 𝐷cat 𝑅 ) ) ( 𝐹 ‘ ( 2nd𝑧 ) ) ) ↑m ( 𝐻𝑧 ) ) ↔ ( 𝑥 𝐺 𝑦 ) ∈ ( ( ( 𝐹𝑥 ) ( Hom ‘ ( 𝐷cat 𝑅 ) ) ( 𝐹𝑦 ) ) ↑m ( 𝑥 𝐻 𝑦 ) ) ) )
73 ovex ( ( 𝐹𝑥 ) ( Hom ‘ ( 𝐷cat 𝑅 ) ) ( 𝐹𝑦 ) ) ∈ V
74 73 67 elmap ( ( 𝑥 𝐺 𝑦 ) ∈ ( ( ( 𝐹𝑥 ) ( Hom ‘ ( 𝐷cat 𝑅 ) ) ( 𝐹𝑦 ) ) ↑m ( 𝑥 𝐻 𝑦 ) ) ↔ ( 𝑥 𝐺 𝑦 ) : ( 𝑥 𝐻 𝑦 ) ⟶ ( ( 𝐹𝑥 ) ( Hom ‘ ( 𝐷cat 𝑅 ) ) ( 𝐹𝑦 ) ) )
75 72 74 bitrdi ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( 𝐺𝑧 ) ∈ ( ( ( 𝐹 ‘ ( 1st𝑧 ) ) ( Hom ‘ ( 𝐷cat 𝑅 ) ) ( 𝐹 ‘ ( 2nd𝑧 ) ) ) ↑m ( 𝐻𝑧 ) ) ↔ ( 𝑥 𝐺 𝑦 ) : ( 𝑥 𝐻 𝑦 ) ⟶ ( ( 𝐹𝑥 ) ( Hom ‘ ( 𝐷cat 𝑅 ) ) ( 𝐹𝑦 ) ) ) )
76 69 75 bibi12d ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( ( 𝐺𝑧 ) ∈ ( ( ( 𝐹 ‘ ( 1st𝑧 ) ) ( Hom ‘ 𝐷 ) ( 𝐹 ‘ ( 2nd𝑧 ) ) ) ↑m ( 𝐻𝑧 ) ) ↔ ( 𝐺𝑧 ) ∈ ( ( ( 𝐹 ‘ ( 1st𝑧 ) ) ( Hom ‘ ( 𝐷cat 𝑅 ) ) ( 𝐹 ‘ ( 2nd𝑧 ) ) ) ↑m ( 𝐻𝑧 ) ) ) ↔ ( ( 𝑥 𝐺 𝑦 ) : ( 𝑥 𝐻 𝑦 ) ⟶ ( ( 𝐹𝑥 ) ( Hom ‘ 𝐷 ) ( 𝐹𝑦 ) ) ↔ ( 𝑥 𝐺 𝑦 ) : ( 𝑥 𝐻 𝑦 ) ⟶ ( ( 𝐹𝑥 ) ( Hom ‘ ( 𝐷cat 𝑅 ) ) ( 𝐹𝑦 ) ) ) ) )
77 76 ralxp ( ∀ 𝑧 ∈ ( 𝐴 × 𝐴 ) ( ( 𝐺𝑧 ) ∈ ( ( ( 𝐹 ‘ ( 1st𝑧 ) ) ( Hom ‘ 𝐷 ) ( 𝐹 ‘ ( 2nd𝑧 ) ) ) ↑m ( 𝐻𝑧 ) ) ↔ ( 𝐺𝑧 ) ∈ ( ( ( 𝐹 ‘ ( 1st𝑧 ) ) ( Hom ‘ ( 𝐷cat 𝑅 ) ) ( 𝐹 ‘ ( 2nd𝑧 ) ) ) ↑m ( 𝐻𝑧 ) ) ) ↔ ∀ 𝑥𝐴𝑦𝐴 ( ( 𝑥 𝐺 𝑦 ) : ( 𝑥 𝐻 𝑦 ) ⟶ ( ( 𝐹𝑥 ) ( Hom ‘ 𝐷 ) ( 𝐹𝑦 ) ) ↔ ( 𝑥 𝐺 𝑦 ) : ( 𝑥 𝐻 𝑦 ) ⟶ ( ( 𝐹𝑥 ) ( Hom ‘ ( 𝐷cat 𝑅 ) ) ( 𝐹𝑦 ) ) ) )
78 50 77 sylibr ( ( 𝜑𝐶 ∈ Cat ) → ∀ 𝑧 ∈ ( 𝐴 × 𝐴 ) ( ( 𝐺𝑧 ) ∈ ( ( ( 𝐹 ‘ ( 1st𝑧 ) ) ( Hom ‘ 𝐷 ) ( 𝐹 ‘ ( 2nd𝑧 ) ) ) ↑m ( 𝐻𝑧 ) ) ↔ ( 𝐺𝑧 ) ∈ ( ( ( 𝐹 ‘ ( 1st𝑧 ) ) ( Hom ‘ ( 𝐷cat 𝑅 ) ) ( 𝐹 ‘ ( 2nd𝑧 ) ) ) ↑m ( 𝐻𝑧 ) ) ) )
79 ralbi ( ∀ 𝑧 ∈ ( 𝐴 × 𝐴 ) ( ( 𝐺𝑧 ) ∈ ( ( ( 𝐹 ‘ ( 1st𝑧 ) ) ( Hom ‘ 𝐷 ) ( 𝐹 ‘ ( 2nd𝑧 ) ) ) ↑m ( 𝐻𝑧 ) ) ↔ ( 𝐺𝑧 ) ∈ ( ( ( 𝐹 ‘ ( 1st𝑧 ) ) ( Hom ‘ ( 𝐷cat 𝑅 ) ) ( 𝐹 ‘ ( 2nd𝑧 ) ) ) ↑m ( 𝐻𝑧 ) ) ) → ( ∀ 𝑧 ∈ ( 𝐴 × 𝐴 ) ( 𝐺𝑧 ) ∈ ( ( ( 𝐹 ‘ ( 1st𝑧 ) ) ( Hom ‘ 𝐷 ) ( 𝐹 ‘ ( 2nd𝑧 ) ) ) ↑m ( 𝐻𝑧 ) ) ↔ ∀ 𝑧 ∈ ( 𝐴 × 𝐴 ) ( 𝐺𝑧 ) ∈ ( ( ( 𝐹 ‘ ( 1st𝑧 ) ) ( Hom ‘ ( 𝐷cat 𝑅 ) ) ( 𝐹 ‘ ( 2nd𝑧 ) ) ) ↑m ( 𝐻𝑧 ) ) ) )
80 78 79 syl ( ( 𝜑𝐶 ∈ Cat ) → ( ∀ 𝑧 ∈ ( 𝐴 × 𝐴 ) ( 𝐺𝑧 ) ∈ ( ( ( 𝐹 ‘ ( 1st𝑧 ) ) ( Hom ‘ 𝐷 ) ( 𝐹 ‘ ( 2nd𝑧 ) ) ) ↑m ( 𝐻𝑧 ) ) ↔ ∀ 𝑧 ∈ ( 𝐴 × 𝐴 ) ( 𝐺𝑧 ) ∈ ( ( ( 𝐹 ‘ ( 1st𝑧 ) ) ( Hom ‘ ( 𝐷cat 𝑅 ) ) ( 𝐹 ‘ ( 2nd𝑧 ) ) ) ↑m ( 𝐻𝑧 ) ) ) )
81 80 3anbi3d ( ( 𝜑𝐶 ∈ Cat ) → ( ( 𝐺 ∈ V ∧ 𝐺 Fn ( 𝐴 × 𝐴 ) ∧ ∀ 𝑧 ∈ ( 𝐴 × 𝐴 ) ( 𝐺𝑧 ) ∈ ( ( ( 𝐹 ‘ ( 1st𝑧 ) ) ( Hom ‘ 𝐷 ) ( 𝐹 ‘ ( 2nd𝑧 ) ) ) ↑m ( 𝐻𝑧 ) ) ) ↔ ( 𝐺 ∈ V ∧ 𝐺 Fn ( 𝐴 × 𝐴 ) ∧ ∀ 𝑧 ∈ ( 𝐴 × 𝐴 ) ( 𝐺𝑧 ) ∈ ( ( ( 𝐹 ‘ ( 1st𝑧 ) ) ( Hom ‘ ( 𝐷cat 𝑅 ) ) ( 𝐹 ‘ ( 2nd𝑧 ) ) ) ↑m ( 𝐻𝑧 ) ) ) ) )
82 elixp2 ( 𝐺X 𝑧 ∈ ( 𝐴 × 𝐴 ) ( ( ( 𝐹 ‘ ( 1st𝑧 ) ) ( Hom ‘ 𝐷 ) ( 𝐹 ‘ ( 2nd𝑧 ) ) ) ↑m ( 𝐻𝑧 ) ) ↔ ( 𝐺 ∈ V ∧ 𝐺 Fn ( 𝐴 × 𝐴 ) ∧ ∀ 𝑧 ∈ ( 𝐴 × 𝐴 ) ( 𝐺𝑧 ) ∈ ( ( ( 𝐹 ‘ ( 1st𝑧 ) ) ( Hom ‘ 𝐷 ) ( 𝐹 ‘ ( 2nd𝑧 ) ) ) ↑m ( 𝐻𝑧 ) ) ) )
83 elixp2 ( 𝐺X 𝑧 ∈ ( 𝐴 × 𝐴 ) ( ( ( 𝐹 ‘ ( 1st𝑧 ) ) ( Hom ‘ ( 𝐷cat 𝑅 ) ) ( 𝐹 ‘ ( 2nd𝑧 ) ) ) ↑m ( 𝐻𝑧 ) ) ↔ ( 𝐺 ∈ V ∧ 𝐺 Fn ( 𝐴 × 𝐴 ) ∧ ∀ 𝑧 ∈ ( 𝐴 × 𝐴 ) ( 𝐺𝑧 ) ∈ ( ( ( 𝐹 ‘ ( 1st𝑧 ) ) ( Hom ‘ ( 𝐷cat 𝑅 ) ) ( 𝐹 ‘ ( 2nd𝑧 ) ) ) ↑m ( 𝐻𝑧 ) ) ) )
84 81 82 83 3bitr4g ( ( 𝜑𝐶 ∈ Cat ) → ( 𝐺X 𝑧 ∈ ( 𝐴 × 𝐴 ) ( ( ( 𝐹 ‘ ( 1st𝑧 ) ) ( Hom ‘ 𝐷 ) ( 𝐹 ‘ ( 2nd𝑧 ) ) ) ↑m ( 𝐻𝑧 ) ) ↔ 𝐺X 𝑧 ∈ ( 𝐴 × 𝐴 ) ( ( ( 𝐹 ‘ ( 1st𝑧 ) ) ( Hom ‘ ( 𝐷cat 𝑅 ) ) ( 𝐹 ‘ ( 2nd𝑧 ) ) ) ↑m ( 𝐻𝑧 ) ) ) )
85 3 ad2antrr ( ( ( 𝜑𝐶 ∈ Cat ) ∧ 𝑥𝐴 ) → 𝑅 ∈ ( Subcat ‘ 𝐷 ) )
86 4 ad2antrr ( ( ( 𝜑𝐶 ∈ Cat ) ∧ 𝑥𝐴 ) → 𝑅 Fn ( 𝑆 × 𝑆 ) )
87 eqid ( Id ‘ 𝐷 ) = ( Id ‘ 𝐷 )
88 5 adantr ( ( 𝜑𝐶 ∈ Cat ) → 𝐹 : 𝐴𝑆 )
89 88 ffvelrnda ( ( ( 𝜑𝐶 ∈ Cat ) ∧ 𝑥𝐴 ) → ( 𝐹𝑥 ) ∈ 𝑆 )
90 20 85 86 87 89 subcid ( ( ( 𝜑𝐶 ∈ Cat ) ∧ 𝑥𝐴 ) → ( ( Id ‘ 𝐷 ) ‘ ( 𝐹𝑥 ) ) = ( ( Id ‘ ( 𝐷cat 𝑅 ) ) ‘ ( 𝐹𝑥 ) ) )
91 90 eqeq2d ( ( ( 𝜑𝐶 ∈ Cat ) ∧ 𝑥𝐴 ) → ( ( ( 𝑥 𝐺 𝑥 ) ‘ ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ) = ( ( Id ‘ 𝐷 ) ‘ ( 𝐹𝑥 ) ) ↔ ( ( 𝑥 𝐺 𝑥 ) ‘ ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ) = ( ( Id ‘ ( 𝐷cat 𝑅 ) ) ‘ ( 𝐹𝑥 ) ) ) )
92 eqid ( comp ‘ 𝐷 ) = ( comp ‘ 𝐷 )
93 20 17 22 4 18 92 rescco ( 𝜑 → ( comp ‘ 𝐷 ) = ( comp ‘ ( 𝐷cat 𝑅 ) ) )
94 93 ad2antrr ( ( ( 𝜑𝐶 ∈ Cat ) ∧ 𝑥𝐴 ) → ( comp ‘ 𝐷 ) = ( comp ‘ ( 𝐷cat 𝑅 ) ) )
95 94 oveqd ( ( ( 𝜑𝐶 ∈ Cat ) ∧ 𝑥𝐴 ) → ( ⟨ ( 𝐹𝑥 ) , ( 𝐹𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( 𝐹𝑧 ) ) = ( ⟨ ( 𝐹𝑥 ) , ( 𝐹𝑦 ) ⟩ ( comp ‘ ( 𝐷cat 𝑅 ) ) ( 𝐹𝑧 ) ) )
96 95 oveqd ( ( ( 𝜑𝐶 ∈ Cat ) ∧ 𝑥𝐴 ) → ( ( ( 𝑦 𝐺 𝑧 ) ‘ 𝑔 ) ( ⟨ ( 𝐹𝑥 ) , ( 𝐹𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( 𝐹𝑧 ) ) ( ( 𝑥 𝐺 𝑦 ) ‘ 𝑓 ) ) = ( ( ( 𝑦 𝐺 𝑧 ) ‘ 𝑔 ) ( ⟨ ( 𝐹𝑥 ) , ( 𝐹𝑦 ) ⟩ ( comp ‘ ( 𝐷cat 𝑅 ) ) ( 𝐹𝑧 ) ) ( ( 𝑥 𝐺 𝑦 ) ‘ 𝑓 ) ) )
97 96 eqeq2d ( ( ( 𝜑𝐶 ∈ Cat ) ∧ 𝑥𝐴 ) → ( ( ( 𝑥 𝐺 𝑧 ) ‘ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ) = ( ( ( 𝑦 𝐺 𝑧 ) ‘ 𝑔 ) ( ⟨ ( 𝐹𝑥 ) , ( 𝐹𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( 𝐹𝑧 ) ) ( ( 𝑥 𝐺 𝑦 ) ‘ 𝑓 ) ) ↔ ( ( 𝑥 𝐺 𝑧 ) ‘ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ) = ( ( ( 𝑦 𝐺 𝑧 ) ‘ 𝑔 ) ( ⟨ ( 𝐹𝑥 ) , ( 𝐹𝑦 ) ⟩ ( comp ‘ ( 𝐷cat 𝑅 ) ) ( 𝐹𝑧 ) ) ( ( 𝑥 𝐺 𝑦 ) ‘ 𝑓 ) ) ) )
98 97 2ralbidv ( ( ( 𝜑𝐶 ∈ Cat ) ∧ 𝑥𝐴 ) → ( ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ( ( 𝑥 𝐺 𝑧 ) ‘ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ) = ( ( ( 𝑦 𝐺 𝑧 ) ‘ 𝑔 ) ( ⟨ ( 𝐹𝑥 ) , ( 𝐹𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( 𝐹𝑧 ) ) ( ( 𝑥 𝐺 𝑦 ) ‘ 𝑓 ) ) ↔ ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ( ( 𝑥 𝐺 𝑧 ) ‘ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ) = ( ( ( 𝑦 𝐺 𝑧 ) ‘ 𝑔 ) ( ⟨ ( 𝐹𝑥 ) , ( 𝐹𝑦 ) ⟩ ( comp ‘ ( 𝐷cat 𝑅 ) ) ( 𝐹𝑧 ) ) ( ( 𝑥 𝐺 𝑦 ) ‘ 𝑓 ) ) ) )
99 98 2ralbidv ( ( ( 𝜑𝐶 ∈ Cat ) ∧ 𝑥𝐴 ) → ( ∀ 𝑦𝐴𝑧𝐴𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ( ( 𝑥 𝐺 𝑧 ) ‘ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ) = ( ( ( 𝑦 𝐺 𝑧 ) ‘ 𝑔 ) ( ⟨ ( 𝐹𝑥 ) , ( 𝐹𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( 𝐹𝑧 ) ) ( ( 𝑥 𝐺 𝑦 ) ‘ 𝑓 ) ) ↔ ∀ 𝑦𝐴𝑧𝐴𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ( ( 𝑥 𝐺 𝑧 ) ‘ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ) = ( ( ( 𝑦 𝐺 𝑧 ) ‘ 𝑔 ) ( ⟨ ( 𝐹𝑥 ) , ( 𝐹𝑦 ) ⟩ ( comp ‘ ( 𝐷cat 𝑅 ) ) ( 𝐹𝑧 ) ) ( ( 𝑥 𝐺 𝑦 ) ‘ 𝑓 ) ) ) )
100 91 99 anbi12d ( ( ( 𝜑𝐶 ∈ Cat ) ∧ 𝑥𝐴 ) → ( ( ( ( 𝑥 𝐺 𝑥 ) ‘ ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ) = ( ( Id ‘ 𝐷 ) ‘ ( 𝐹𝑥 ) ) ∧ ∀ 𝑦𝐴𝑧𝐴𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ( ( 𝑥 𝐺 𝑧 ) ‘ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ) = ( ( ( 𝑦 𝐺 𝑧 ) ‘ 𝑔 ) ( ⟨ ( 𝐹𝑥 ) , ( 𝐹𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( 𝐹𝑧 ) ) ( ( 𝑥 𝐺 𝑦 ) ‘ 𝑓 ) ) ) ↔ ( ( ( 𝑥 𝐺 𝑥 ) ‘ ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ) = ( ( Id ‘ ( 𝐷cat 𝑅 ) ) ‘ ( 𝐹𝑥 ) ) ∧ ∀ 𝑦𝐴𝑧𝐴𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ( ( 𝑥 𝐺 𝑧 ) ‘ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ) = ( ( ( 𝑦 𝐺 𝑧 ) ‘ 𝑔 ) ( ⟨ ( 𝐹𝑥 ) , ( 𝐹𝑦 ) ⟩ ( comp ‘ ( 𝐷cat 𝑅 ) ) ( 𝐹𝑧 ) ) ( ( 𝑥 𝐺 𝑦 ) ‘ 𝑓 ) ) ) ) )
101 100 ralbidva ( ( 𝜑𝐶 ∈ Cat ) → ( ∀ 𝑥𝐴 ( ( ( 𝑥 𝐺 𝑥 ) ‘ ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ) = ( ( Id ‘ 𝐷 ) ‘ ( 𝐹𝑥 ) ) ∧ ∀ 𝑦𝐴𝑧𝐴𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ( ( 𝑥 𝐺 𝑧 ) ‘ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ) = ( ( ( 𝑦 𝐺 𝑧 ) ‘ 𝑔 ) ( ⟨ ( 𝐹𝑥 ) , ( 𝐹𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( 𝐹𝑧 ) ) ( ( 𝑥 𝐺 𝑦 ) ‘ 𝑓 ) ) ) ↔ ∀ 𝑥𝐴 ( ( ( 𝑥 𝐺 𝑥 ) ‘ ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ) = ( ( Id ‘ ( 𝐷cat 𝑅 ) ) ‘ ( 𝐹𝑥 ) ) ∧ ∀ 𝑦𝐴𝑧𝐴𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ( ( 𝑥 𝐺 𝑧 ) ‘ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ) = ( ( ( 𝑦 𝐺 𝑧 ) ‘ 𝑔 ) ( ⟨ ( 𝐹𝑥 ) , ( 𝐹𝑦 ) ⟩ ( comp ‘ ( 𝐷cat 𝑅 ) ) ( 𝐹𝑧 ) ) ( ( 𝑥 𝐺 𝑦 ) ‘ 𝑓 ) ) ) ) )
102 27 84 101 3anbi123d ( ( 𝜑𝐶 ∈ Cat ) → ( ( 𝐹 : 𝐴 ⟶ ( Base ‘ 𝐷 ) ∧ 𝐺X 𝑧 ∈ ( 𝐴 × 𝐴 ) ( ( ( 𝐹 ‘ ( 1st𝑧 ) ) ( Hom ‘ 𝐷 ) ( 𝐹 ‘ ( 2nd𝑧 ) ) ) ↑m ( 𝐻𝑧 ) ) ∧ ∀ 𝑥𝐴 ( ( ( 𝑥 𝐺 𝑥 ) ‘ ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ) = ( ( Id ‘ 𝐷 ) ‘ ( 𝐹𝑥 ) ) ∧ ∀ 𝑦𝐴𝑧𝐴𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ( ( 𝑥 𝐺 𝑧 ) ‘ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ) = ( ( ( 𝑦 𝐺 𝑧 ) ‘ 𝑔 ) ( ⟨ ( 𝐹𝑥 ) , ( 𝐹𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( 𝐹𝑧 ) ) ( ( 𝑥 𝐺 𝑦 ) ‘ 𝑓 ) ) ) ) ↔ ( 𝐹 : 𝐴 ⟶ ( Base ‘ ( 𝐷cat 𝑅 ) ) ∧ 𝐺X 𝑧 ∈ ( 𝐴 × 𝐴 ) ( ( ( 𝐹 ‘ ( 1st𝑧 ) ) ( Hom ‘ ( 𝐷cat 𝑅 ) ) ( 𝐹 ‘ ( 2nd𝑧 ) ) ) ↑m ( 𝐻𝑧 ) ) ∧ ∀ 𝑥𝐴 ( ( ( 𝑥 𝐺 𝑥 ) ‘ ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ) = ( ( Id ‘ ( 𝐷cat 𝑅 ) ) ‘ ( 𝐹𝑥 ) ) ∧ ∀ 𝑦𝐴𝑧𝐴𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ( ( 𝑥 𝐺 𝑧 ) ‘ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ) = ( ( ( 𝑦 𝐺 𝑧 ) ‘ 𝑔 ) ( ⟨ ( 𝐹𝑥 ) , ( 𝐹𝑦 ) ⟩ ( comp ‘ ( 𝐷cat 𝑅 ) ) ( 𝐹𝑧 ) ) ( ( 𝑥 𝐺 𝑦 ) ‘ 𝑓 ) ) ) ) ) )
103 eqid ( Id ‘ 𝐶 ) = ( Id ‘ 𝐶 )
104 eqid ( comp ‘ 𝐶 ) = ( comp ‘ 𝐶 )
105 simpr ( ( 𝜑𝐶 ∈ Cat ) → 𝐶 ∈ Cat )
106 22 adantr ( ( 𝜑𝐶 ∈ Cat ) → 𝐷 ∈ Cat )
107 1 17 2 32 103 87 104 92 105 106 isfunc ( ( 𝜑𝐶 ∈ Cat ) → ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ↔ ( 𝐹 : 𝐴 ⟶ ( Base ‘ 𝐷 ) ∧ 𝐺X 𝑧 ∈ ( 𝐴 × 𝐴 ) ( ( ( 𝐹 ‘ ( 1st𝑧 ) ) ( Hom ‘ 𝐷 ) ( 𝐹 ‘ ( 2nd𝑧 ) ) ) ↑m ( 𝐻𝑧 ) ) ∧ ∀ 𝑥𝐴 ( ( ( 𝑥 𝐺 𝑥 ) ‘ ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ) = ( ( Id ‘ 𝐷 ) ‘ ( 𝐹𝑥 ) ) ∧ ∀ 𝑦𝐴𝑧𝐴𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ( ( 𝑥 𝐺 𝑧 ) ‘ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ) = ( ( ( 𝑦 𝐺 𝑧 ) ‘ 𝑔 ) ( ⟨ ( 𝐹𝑥 ) , ( 𝐹𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( 𝐹𝑧 ) ) ( ( 𝑥 𝐺 𝑦 ) ‘ 𝑓 ) ) ) ) ) )
108 eqid ( Base ‘ ( 𝐷cat 𝑅 ) ) = ( Base ‘ ( 𝐷cat 𝑅 ) )
109 eqid ( Hom ‘ ( 𝐷cat 𝑅 ) ) = ( Hom ‘ ( 𝐷cat 𝑅 ) )
110 eqid ( Id ‘ ( 𝐷cat 𝑅 ) ) = ( Id ‘ ( 𝐷cat 𝑅 ) )
111 eqid ( comp ‘ ( 𝐷cat 𝑅 ) ) = ( comp ‘ ( 𝐷cat 𝑅 ) )
112 20 3 subccat ( 𝜑 → ( 𝐷cat 𝑅 ) ∈ Cat )
113 112 adantr ( ( 𝜑𝐶 ∈ Cat ) → ( 𝐷cat 𝑅 ) ∈ Cat )
114 1 108 2 109 103 110 104 111 105 113 isfunc ( ( 𝜑𝐶 ∈ Cat ) → ( 𝐹 ( 𝐶 Func ( 𝐷cat 𝑅 ) ) 𝐺 ↔ ( 𝐹 : 𝐴 ⟶ ( Base ‘ ( 𝐷cat 𝑅 ) ) ∧ 𝐺X 𝑧 ∈ ( 𝐴 × 𝐴 ) ( ( ( 𝐹 ‘ ( 1st𝑧 ) ) ( Hom ‘ ( 𝐷cat 𝑅 ) ) ( 𝐹 ‘ ( 2nd𝑧 ) ) ) ↑m ( 𝐻𝑧 ) ) ∧ ∀ 𝑥𝐴 ( ( ( 𝑥 𝐺 𝑥 ) ‘ ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ) = ( ( Id ‘ ( 𝐷cat 𝑅 ) ) ‘ ( 𝐹𝑥 ) ) ∧ ∀ 𝑦𝐴𝑧𝐴𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ( ( 𝑥 𝐺 𝑧 ) ‘ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ) = ( ( ( 𝑦 𝐺 𝑧 ) ‘ 𝑔 ) ( ⟨ ( 𝐹𝑥 ) , ( 𝐹𝑦 ) ⟩ ( comp ‘ ( 𝐷cat 𝑅 ) ) ( 𝐹𝑧 ) ) ( ( 𝑥 𝐺 𝑦 ) ‘ 𝑓 ) ) ) ) ) )
115 102 107 114 3bitr4d ( ( 𝜑𝐶 ∈ Cat ) → ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺𝐹 ( 𝐶 Func ( 𝐷cat 𝑅 ) ) 𝐺 ) )
116 115 ex ( 𝜑 → ( 𝐶 ∈ Cat → ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺𝐹 ( 𝐶 Func ( 𝐷cat 𝑅 ) ) 𝐺 ) ) )
117 11 16 116 pm5.21ndd ( 𝜑 → ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺𝐹 ( 𝐶 Func ( 𝐷cat 𝑅 ) ) 𝐺 ) )