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 𝑅 ) ) 𝐺 ) )