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 
|- A = ( Base ` C )
funcres2b.h 
|- H = ( Hom ` C )
funcres2b.r 
|- ( ph -> R e. ( Subcat ` D ) )
funcres2b.s 
|- ( ph -> R Fn ( S X. S ) )
funcres2b.1 
|- ( ph -> F : A --> S )
funcres2b.2 
|- ( ( ph /\ ( x e. A /\ y e. A ) ) -> ( x G y ) : Y --> ( ( F ` x ) R ( F ` y ) ) )
Assertion funcres2b 
|- ( ph -> ( F ( C Func D ) G <-> F ( C Func ( D |`cat R ) ) G ) )

Proof

Step Hyp Ref Expression
1 funcres2b.a 
 |-  A = ( Base ` C )
2 funcres2b.h 
 |-  H = ( Hom ` C )
3 funcres2b.r 
 |-  ( ph -> R e. ( Subcat ` D ) )
4 funcres2b.s 
 |-  ( ph -> R Fn ( S X. S ) )
5 funcres2b.1 
 |-  ( ph -> F : A --> S )
6 funcres2b.2 
 |-  ( ( ph /\ ( x e. A /\ y e. A ) ) -> ( x G y ) : Y --> ( ( F ` x ) R ( F ` y ) ) )
7 df-br 
 |-  ( F ( C Func D ) G <-> <. F , G >. e. ( C Func D ) )
8 funcrcl 
 |-  ( <. F , G >. e. ( C Func D ) -> ( C e. Cat /\ D e. Cat ) )
9 7 8 sylbi 
 |-  ( F ( C Func D ) G -> ( C e. Cat /\ D e. Cat ) )
10 9 simpld 
 |-  ( F ( C Func D ) G -> C e. Cat )
11 10 a1i 
 |-  ( ph -> ( F ( C Func D ) G -> C e. Cat ) )
12 df-br 
 |-  ( F ( C Func ( D |`cat R ) ) G <-> <. F , G >. e. ( C Func ( D |`cat R ) ) )
13 funcrcl 
 |-  ( <. F , G >. e. ( C Func ( D |`cat R ) ) -> ( C e. Cat /\ ( D |`cat R ) e. Cat ) )
14 12 13 sylbi 
 |-  ( F ( C Func ( D |`cat R ) ) G -> ( C e. Cat /\ ( D |`cat R ) e. Cat ) )
15 14 simpld 
 |-  ( F ( C Func ( D |`cat R ) ) G -> C e. Cat )
16 15 a1i 
 |-  ( ph -> ( F ( C Func ( D |`cat R ) ) G -> C e. Cat ) )
17 eqid 
 |-  ( Base ` D ) = ( Base ` D )
18 3 4 17 subcss1 
 |-  ( ph -> S C_ ( Base ` D ) )
19 5 18 fssd 
 |-  ( ph -> F : A --> ( Base ` D ) )
20 eqid 
 |-  ( D |`cat R ) = ( D |`cat R )
21 subcrcl 
 |-  ( R e. ( Subcat ` D ) -> D e. Cat )
22 3 21 syl 
 |-  ( ph -> D e. Cat )
23 20 17 22 4 18 rescbas 
 |-  ( ph -> S = ( Base ` ( D |`cat R ) ) )
24 23 feq3d 
 |-  ( ph -> ( F : A --> S <-> F : A --> ( Base ` ( D |`cat R ) ) ) )
25 5 24 mpbid 
 |-  ( ph -> F : A --> ( Base ` ( D |`cat R ) ) )
26 19 25 2thd 
 |-  ( ph -> ( F : A --> ( Base ` D ) <-> F : A --> ( Base ` ( D |`cat R ) ) ) )
27 26 adantr 
 |-  ( ( ph /\ C e. Cat ) -> ( F : A --> ( Base ` D ) <-> F : A --> ( Base ` ( D |`cat R ) ) ) )
28 6 adantlr 
 |-  ( ( ( ph /\ C e. Cat ) /\ ( x e. A /\ y e. A ) ) -> ( x G y ) : Y --> ( ( F ` x ) R ( F ` y ) ) )
29 28 frnd 
 |-  ( ( ( ph /\ C e. Cat ) /\ ( x e. A /\ y e. A ) ) -> ran ( x G y ) C_ ( ( F ` x ) R ( F ` y ) ) )
30 3 ad2antrr 
 |-  ( ( ( ph /\ C e. Cat ) /\ ( x e. A /\ y e. A ) ) -> R e. ( Subcat ` D ) )
31 4 ad2antrr 
 |-  ( ( ( ph /\ C e. Cat ) /\ ( x e. A /\ y e. A ) ) -> R Fn ( S X. S ) )
32 eqid 
 |-  ( Hom ` D ) = ( Hom ` D )
33 5 ad2antrr 
 |-  ( ( ( ph /\ C e. Cat ) /\ ( x e. A /\ y e. A ) ) -> F : A --> S )
34 simprl 
 |-  ( ( ( ph /\ C e. Cat ) /\ ( x e. A /\ y e. A ) ) -> x e. A )
35 33 34 ffvelrnd 
 |-  ( ( ( ph /\ C e. Cat ) /\ ( x e. A /\ y e. A ) ) -> ( F ` x ) e. S )
36 simprr 
 |-  ( ( ( ph /\ C e. Cat ) /\ ( x e. A /\ y e. A ) ) -> y e. A )
37 33 36 ffvelrnd 
 |-  ( ( ( ph /\ C e. Cat ) /\ ( x e. A /\ y e. A ) ) -> ( F ` y ) e. S )
38 30 31 32 35 37 subcss2 
 |-  ( ( ( ph /\ C e. Cat ) /\ ( x e. A /\ y e. A ) ) -> ( ( F ` x ) R ( F ` y ) ) C_ ( ( F ` x ) ( Hom ` D ) ( F ` y ) ) )
39 29 38 sstrd 
 |-  ( ( ( ph /\ C e. Cat ) /\ ( x e. A /\ y e. A ) ) -> ran ( x G y ) C_ ( ( F ` x ) ( Hom ` D ) ( F ` y ) ) )
40 39 29 2thd 
 |-  ( ( ( ph /\ C e. Cat ) /\ ( x e. A /\ y e. A ) ) -> ( ran ( x G y ) C_ ( ( F ` x ) ( Hom ` D ) ( F ` y ) ) <-> ran ( x G y ) C_ ( ( F ` x ) R ( F ` y ) ) ) )
41 40 anbi2d 
 |-  ( ( ( ph /\ C e. Cat ) /\ ( x e. A /\ y e. A ) ) -> ( ( ( x G y ) Fn ( x H y ) /\ ran ( x G y ) C_ ( ( F ` x ) ( Hom ` D ) ( F ` y ) ) ) <-> ( ( x G y ) Fn ( x H y ) /\ ran ( x G y ) C_ ( ( F ` x ) R ( F ` y ) ) ) ) )
42 df-f 
 |-  ( ( x G y ) : ( x H y ) --> ( ( F ` x ) ( Hom ` D ) ( F ` y ) ) <-> ( ( x G y ) Fn ( x H y ) /\ ran ( x G y ) C_ ( ( F ` x ) ( Hom ` D ) ( F ` y ) ) ) )
43 df-f 
 |-  ( ( x G y ) : ( x H y ) --> ( ( F ` x ) R ( F ` y ) ) <-> ( ( x G y ) Fn ( x H y ) /\ ran ( x G y ) C_ ( ( F ` x ) R ( F ` y ) ) ) )
44 41 42 43 3bitr4g 
 |-  ( ( ( ph /\ C e. Cat ) /\ ( x e. A /\ y e. A ) ) -> ( ( x G y ) : ( x H y ) --> ( ( F ` x ) ( Hom ` D ) ( F ` y ) ) <-> ( x G y ) : ( x H y ) --> ( ( F ` x ) R ( F ` y ) ) ) )
45 20 17 22 4 18 reschom 
 |-  ( ph -> R = ( Hom ` ( D |`cat R ) ) )
46 45 ad2antrr 
 |-  ( ( ( ph /\ C e. Cat ) /\ ( x e. A /\ y e. A ) ) -> R = ( Hom ` ( D |`cat R ) ) )
47 46 oveqd 
 |-  ( ( ( ph /\ C e. Cat ) /\ ( x e. A /\ y e. A ) ) -> ( ( F ` x ) R ( F ` y ) ) = ( ( F ` x ) ( Hom ` ( D |`cat R ) ) ( F ` y ) ) )
48 47 feq3d 
 |-  ( ( ( ph /\ C e. Cat ) /\ ( x e. A /\ y e. A ) ) -> ( ( x G y ) : ( x H y ) --> ( ( F ` x ) R ( F ` y ) ) <-> ( x G y ) : ( x H y ) --> ( ( F ` x ) ( Hom ` ( D |`cat R ) ) ( F ` y ) ) ) )
49 44 48 bitrd 
 |-  ( ( ( ph /\ C e. Cat ) /\ ( x e. A /\ y e. A ) ) -> ( ( x G y ) : ( x H y ) --> ( ( F ` x ) ( Hom ` D ) ( F ` y ) ) <-> ( x G y ) : ( x H y ) --> ( ( F ` x ) ( Hom ` ( D |`cat R ) ) ( F ` y ) ) ) )
50 49 ralrimivva 
 |-  ( ( ph /\ C e. Cat ) -> A. x e. A A. y e. A ( ( x G y ) : ( x H y ) --> ( ( F ` x ) ( Hom ` D ) ( F ` y ) ) <-> ( x G y ) : ( x H y ) --> ( ( F ` x ) ( Hom ` ( D |`cat R ) ) ( F ` y ) ) ) )
51 fveq2 
 |-  ( z = <. x , y >. -> ( G ` z ) = ( G ` <. x , y >. ) )
52 df-ov 
 |-  ( x G y ) = ( G ` <. x , y >. )
53 51 52 eqtr4di 
 |-  ( z = <. x , y >. -> ( G ` z ) = ( x G y ) )
54 vex 
 |-  x e. _V
55 vex 
 |-  y e. _V
56 54 55 op1std 
 |-  ( z = <. x , y >. -> ( 1st ` z ) = x )
57 56 fveq2d 
 |-  ( z = <. x , y >. -> ( F ` ( 1st ` z ) ) = ( F ` x ) )
58 54 55 op2ndd 
 |-  ( z = <. x , y >. -> ( 2nd ` z ) = y )
59 58 fveq2d 
 |-  ( z = <. x , y >. -> ( F ` ( 2nd ` z ) ) = ( F ` y ) )
60 57 59 oveq12d 
 |-  ( z = <. x , y >. -> ( ( F ` ( 1st ` z ) ) ( Hom ` D ) ( F ` ( 2nd ` z ) ) ) = ( ( F ` x ) ( Hom ` D ) ( F ` y ) ) )
61 fveq2 
 |-  ( z = <. x , y >. -> ( H ` z ) = ( H ` <. x , y >. ) )
62 df-ov 
 |-  ( x H y ) = ( H ` <. x , y >. )
63 61 62 eqtr4di 
 |-  ( z = <. x , y >. -> ( H ` z ) = ( x H y ) )
64 60 63 oveq12d 
 |-  ( z = <. x , y >. -> ( ( ( F ` ( 1st ` z ) ) ( Hom ` D ) ( F ` ( 2nd ` z ) ) ) ^m ( H ` z ) ) = ( ( ( F ` x ) ( Hom ` D ) ( F ` y ) ) ^m ( x H y ) ) )
65 53 64 eleq12d 
 |-  ( z = <. x , y >. -> ( ( G ` z ) e. ( ( ( F ` ( 1st ` z ) ) ( Hom ` D ) ( F ` ( 2nd ` z ) ) ) ^m ( H ` z ) ) <-> ( x G y ) e. ( ( ( F ` x ) ( Hom ` D ) ( F ` y ) ) ^m ( x H y ) ) ) )
66 ovex 
 |-  ( ( F ` x ) ( Hom ` D ) ( F ` y ) ) e. _V
67 ovex 
 |-  ( x H y ) e. _V
68 66 67 elmap 
 |-  ( ( x G y ) e. ( ( ( F ` x ) ( Hom ` D ) ( F ` y ) ) ^m ( x H y ) ) <-> ( x G y ) : ( x H y ) --> ( ( F ` x ) ( Hom ` D ) ( F ` y ) ) )
69 65 68 bitrdi 
 |-  ( z = <. x , y >. -> ( ( G ` z ) e. ( ( ( F ` ( 1st ` z ) ) ( Hom ` D ) ( F ` ( 2nd ` z ) ) ) ^m ( H ` z ) ) <-> ( x G y ) : ( x H y ) --> ( ( F ` x ) ( Hom ` D ) ( F ` y ) ) ) )
70 57 59 oveq12d 
 |-  ( z = <. x , y >. -> ( ( F ` ( 1st ` z ) ) ( Hom ` ( D |`cat R ) ) ( F ` ( 2nd ` z ) ) ) = ( ( F ` x ) ( Hom ` ( D |`cat R ) ) ( F ` y ) ) )
71 70 63 oveq12d 
 |-  ( z = <. x , y >. -> ( ( ( F ` ( 1st ` z ) ) ( Hom ` ( D |`cat R ) ) ( F ` ( 2nd ` z ) ) ) ^m ( H ` z ) ) = ( ( ( F ` x ) ( Hom ` ( D |`cat R ) ) ( F ` y ) ) ^m ( x H y ) ) )
72 53 71 eleq12d 
 |-  ( z = <. x , y >. -> ( ( G ` z ) e. ( ( ( F ` ( 1st ` z ) ) ( Hom ` ( D |`cat R ) ) ( F ` ( 2nd ` z ) ) ) ^m ( H ` z ) ) <-> ( x G y ) e. ( ( ( F ` x ) ( Hom ` ( D |`cat R ) ) ( F ` y ) ) ^m ( x H y ) ) ) )
73 ovex 
 |-  ( ( F ` x ) ( Hom ` ( D |`cat R ) ) ( F ` y ) ) e. _V
74 73 67 elmap 
 |-  ( ( x G y ) e. ( ( ( F ` x ) ( Hom ` ( D |`cat R ) ) ( F ` y ) ) ^m ( x H y ) ) <-> ( x G y ) : ( x H y ) --> ( ( F ` x ) ( Hom ` ( D |`cat R ) ) ( F ` y ) ) )
75 72 74 bitrdi 
 |-  ( z = <. x , y >. -> ( ( G ` z ) e. ( ( ( F ` ( 1st ` z ) ) ( Hom ` ( D |`cat R ) ) ( F ` ( 2nd ` z ) ) ) ^m ( H ` z ) ) <-> ( x G y ) : ( x H y ) --> ( ( F ` x ) ( Hom ` ( D |`cat R ) ) ( F ` y ) ) ) )
76 69 75 bibi12d 
 |-  ( z = <. x , y >. -> ( ( ( G ` z ) e. ( ( ( F ` ( 1st ` z ) ) ( Hom ` D ) ( F ` ( 2nd ` z ) ) ) ^m ( H ` z ) ) <-> ( G ` z ) e. ( ( ( F ` ( 1st ` z ) ) ( Hom ` ( D |`cat R ) ) ( F ` ( 2nd ` z ) ) ) ^m ( H ` z ) ) ) <-> ( ( x G y ) : ( x H y ) --> ( ( F ` x ) ( Hom ` D ) ( F ` y ) ) <-> ( x G y ) : ( x H y ) --> ( ( F ` x ) ( Hom ` ( D |`cat R ) ) ( F ` y ) ) ) ) )
77 76 ralxp 
 |-  ( A. z e. ( A X. A ) ( ( G ` z ) e. ( ( ( F ` ( 1st ` z ) ) ( Hom ` D ) ( F ` ( 2nd ` z ) ) ) ^m ( H ` z ) ) <-> ( G ` z ) e. ( ( ( F ` ( 1st ` z ) ) ( Hom ` ( D |`cat R ) ) ( F ` ( 2nd ` z ) ) ) ^m ( H ` z ) ) ) <-> A. x e. A A. y e. A ( ( x G y ) : ( x H y ) --> ( ( F ` x ) ( Hom ` D ) ( F ` y ) ) <-> ( x G y ) : ( x H y ) --> ( ( F ` x ) ( Hom ` ( D |`cat R ) ) ( F ` y ) ) ) )
78 50 77 sylibr 
 |-  ( ( ph /\ C e. Cat ) -> A. z e. ( A X. A ) ( ( G ` z ) e. ( ( ( F ` ( 1st ` z ) ) ( Hom ` D ) ( F ` ( 2nd ` z ) ) ) ^m ( H ` z ) ) <-> ( G ` z ) e. ( ( ( F ` ( 1st ` z ) ) ( Hom ` ( D |`cat R ) ) ( F ` ( 2nd ` z ) ) ) ^m ( H ` z ) ) ) )
79 ralbi 
 |-  ( A. z e. ( A X. A ) ( ( G ` z ) e. ( ( ( F ` ( 1st ` z ) ) ( Hom ` D ) ( F ` ( 2nd ` z ) ) ) ^m ( H ` z ) ) <-> ( G ` z ) e. ( ( ( F ` ( 1st ` z ) ) ( Hom ` ( D |`cat R ) ) ( F ` ( 2nd ` z ) ) ) ^m ( H ` z ) ) ) -> ( A. z e. ( A X. A ) ( G ` z ) e. ( ( ( F ` ( 1st ` z ) ) ( Hom ` D ) ( F ` ( 2nd ` z ) ) ) ^m ( H ` z ) ) <-> A. z e. ( A X. A ) ( G ` z ) e. ( ( ( F ` ( 1st ` z ) ) ( Hom ` ( D |`cat R ) ) ( F ` ( 2nd ` z ) ) ) ^m ( H ` z ) ) ) )
80 78 79 syl 
 |-  ( ( ph /\ C e. Cat ) -> ( A. z e. ( A X. A ) ( G ` z ) e. ( ( ( F ` ( 1st ` z ) ) ( Hom ` D ) ( F ` ( 2nd ` z ) ) ) ^m ( H ` z ) ) <-> A. z e. ( A X. A ) ( G ` z ) e. ( ( ( F ` ( 1st ` z ) ) ( Hom ` ( D |`cat R ) ) ( F ` ( 2nd ` z ) ) ) ^m ( H ` z ) ) ) )
81 80 3anbi3d 
 |-  ( ( ph /\ C e. Cat ) -> ( ( G e. _V /\ G Fn ( A X. A ) /\ A. z e. ( A X. A ) ( G ` z ) e. ( ( ( F ` ( 1st ` z ) ) ( Hom ` D ) ( F ` ( 2nd ` z ) ) ) ^m ( H ` z ) ) ) <-> ( G e. _V /\ G Fn ( A X. A ) /\ A. z e. ( A X. A ) ( G ` z ) e. ( ( ( F ` ( 1st ` z ) ) ( Hom ` ( D |`cat R ) ) ( F ` ( 2nd ` z ) ) ) ^m ( H ` z ) ) ) ) )
82 elixp2 
 |-  ( G e. X_ z e. ( A X. A ) ( ( ( F ` ( 1st ` z ) ) ( Hom ` D ) ( F ` ( 2nd ` z ) ) ) ^m ( H ` z ) ) <-> ( G e. _V /\ G Fn ( A X. A ) /\ A. z e. ( A X. A ) ( G ` z ) e. ( ( ( F ` ( 1st ` z ) ) ( Hom ` D ) ( F ` ( 2nd ` z ) ) ) ^m ( H ` z ) ) ) )
83 elixp2 
 |-  ( G e. X_ z e. ( A X. A ) ( ( ( F ` ( 1st ` z ) ) ( Hom ` ( D |`cat R ) ) ( F ` ( 2nd ` z ) ) ) ^m ( H ` z ) ) <-> ( G e. _V /\ G Fn ( A X. A ) /\ A. z e. ( A X. A ) ( G ` z ) e. ( ( ( F ` ( 1st ` z ) ) ( Hom ` ( D |`cat R ) ) ( F ` ( 2nd ` z ) ) ) ^m ( H ` z ) ) ) )
84 81 82 83 3bitr4g 
 |-  ( ( ph /\ C e. Cat ) -> ( G e. X_ z e. ( A X. A ) ( ( ( F ` ( 1st ` z ) ) ( Hom ` D ) ( F ` ( 2nd ` z ) ) ) ^m ( H ` z ) ) <-> G e. X_ z e. ( A X. A ) ( ( ( F ` ( 1st ` z ) ) ( Hom ` ( D |`cat R ) ) ( F ` ( 2nd ` z ) ) ) ^m ( H ` z ) ) ) )
85 3 ad2antrr 
 |-  ( ( ( ph /\ C e. Cat ) /\ x e. A ) -> R e. ( Subcat ` D ) )
86 4 ad2antrr 
 |-  ( ( ( ph /\ C e. Cat ) /\ x e. A ) -> R Fn ( S X. S ) )
87 eqid 
 |-  ( Id ` D ) = ( Id ` D )
88 5 adantr 
 |-  ( ( ph /\ C e. Cat ) -> F : A --> S )
89 88 ffvelrnda 
 |-  ( ( ( ph /\ C e. Cat ) /\ x e. A ) -> ( F ` x ) e. S )
90 20 85 86 87 89 subcid 
 |-  ( ( ( ph /\ C e. Cat ) /\ x e. A ) -> ( ( Id ` D ) ` ( F ` x ) ) = ( ( Id ` ( D |`cat R ) ) ` ( F ` x ) ) )
91 90 eqeq2d 
 |-  ( ( ( ph /\ C e. Cat ) /\ x e. A ) -> ( ( ( x G x ) ` ( ( Id ` C ) ` x ) ) = ( ( Id ` D ) ` ( F ` x ) ) <-> ( ( x G x ) ` ( ( Id ` C ) ` x ) ) = ( ( Id ` ( D |`cat R ) ) ` ( F ` x ) ) ) )
92 eqid 
 |-  ( comp ` D ) = ( comp ` D )
93 20 17 22 4 18 92 rescco 
 |-  ( ph -> ( comp ` D ) = ( comp ` ( D |`cat R ) ) )
94 93 ad2antrr 
 |-  ( ( ( ph /\ C e. Cat ) /\ x e. A ) -> ( comp ` D ) = ( comp ` ( D |`cat R ) ) )
95 94 oveqd 
 |-  ( ( ( ph /\ C e. Cat ) /\ x e. A ) -> ( <. ( F ` x ) , ( F ` y ) >. ( comp ` D ) ( F ` z ) ) = ( <. ( F ` x ) , ( F ` y ) >. ( comp ` ( D |`cat R ) ) ( F ` z ) ) )
96 95 oveqd 
 |-  ( ( ( ph /\ C e. Cat ) /\ x e. A ) -> ( ( ( y G z ) ` g ) ( <. ( F ` x ) , ( F ` y ) >. ( comp ` D ) ( F ` z ) ) ( ( x G y ) ` f ) ) = ( ( ( y G z ) ` g ) ( <. ( F ` x ) , ( F ` y ) >. ( comp ` ( D |`cat R ) ) ( F ` z ) ) ( ( x G y ) ` f ) ) )
97 96 eqeq2d 
 |-  ( ( ( ph /\ C e. Cat ) /\ x e. A ) -> ( ( ( x G z ) ` ( g ( <. x , y >. ( comp ` C ) z ) f ) ) = ( ( ( y G z ) ` g ) ( <. ( F ` x ) , ( F ` y ) >. ( comp ` D ) ( F ` z ) ) ( ( x G y ) ` f ) ) <-> ( ( x G z ) ` ( g ( <. x , y >. ( comp ` C ) z ) f ) ) = ( ( ( y G z ) ` g ) ( <. ( F ` x ) , ( F ` y ) >. ( comp ` ( D |`cat R ) ) ( F ` z ) ) ( ( x G y ) ` f ) ) ) )
98 97 2ralbidv 
 |-  ( ( ( ph /\ C e. Cat ) /\ x e. A ) -> ( A. f e. ( x H y ) A. g e. ( y H z ) ( ( x G z ) ` ( g ( <. x , y >. ( comp ` C ) z ) f ) ) = ( ( ( y G z ) ` g ) ( <. ( F ` x ) , ( F ` y ) >. ( comp ` D ) ( F ` z ) ) ( ( x G y ) ` f ) ) <-> A. f e. ( x H y ) A. g e. ( y H z ) ( ( x G z ) ` ( g ( <. x , y >. ( comp ` C ) z ) f ) ) = ( ( ( y G z ) ` g ) ( <. ( F ` x ) , ( F ` y ) >. ( comp ` ( D |`cat R ) ) ( F ` z ) ) ( ( x G y ) ` f ) ) ) )
99 98 2ralbidv 
 |-  ( ( ( ph /\ C e. Cat ) /\ x e. A ) -> ( A. y e. A A. z e. A A. f e. ( x H y ) A. g e. ( y H z ) ( ( x G z ) ` ( g ( <. x , y >. ( comp ` C ) z ) f ) ) = ( ( ( y G z ) ` g ) ( <. ( F ` x ) , ( F ` y ) >. ( comp ` D ) ( F ` z ) ) ( ( x G y ) ` f ) ) <-> A. y e. A A. z e. A A. f e. ( x H y ) A. g e. ( y H z ) ( ( x G z ) ` ( g ( <. x , y >. ( comp ` C ) z ) f ) ) = ( ( ( y G z ) ` g ) ( <. ( F ` x ) , ( F ` y ) >. ( comp ` ( D |`cat R ) ) ( F ` z ) ) ( ( x G y ) ` f ) ) ) )
100 91 99 anbi12d 
 |-  ( ( ( ph /\ C e. Cat ) /\ x e. A ) -> ( ( ( ( x G x ) ` ( ( Id ` C ) ` x ) ) = ( ( Id ` D ) ` ( F ` x ) ) /\ A. y e. A A. z e. A A. f e. ( x H y ) A. g e. ( y H z ) ( ( x G z ) ` ( g ( <. x , y >. ( comp ` C ) z ) f ) ) = ( ( ( y G z ) ` g ) ( <. ( F ` x ) , ( F ` y ) >. ( comp ` D ) ( F ` z ) ) ( ( x G y ) ` f ) ) ) <-> ( ( ( x G x ) ` ( ( Id ` C ) ` x ) ) = ( ( Id ` ( D |`cat R ) ) ` ( F ` x ) ) /\ A. y e. A A. z e. A A. f e. ( x H y ) A. g e. ( y H z ) ( ( x G z ) ` ( g ( <. x , y >. ( comp ` C ) z ) f ) ) = ( ( ( y G z ) ` g ) ( <. ( F ` x ) , ( F ` y ) >. ( comp ` ( D |`cat R ) ) ( F ` z ) ) ( ( x G y ) ` f ) ) ) ) )
101 100 ralbidva 
 |-  ( ( ph /\ C e. Cat ) -> ( A. x e. A ( ( ( x G x ) ` ( ( Id ` C ) ` x ) ) = ( ( Id ` D ) ` ( F ` x ) ) /\ A. y e. A A. z e. A A. f e. ( x H y ) A. g e. ( y H z ) ( ( x G z ) ` ( g ( <. x , y >. ( comp ` C ) z ) f ) ) = ( ( ( y G z ) ` g ) ( <. ( F ` x ) , ( F ` y ) >. ( comp ` D ) ( F ` z ) ) ( ( x G y ) ` f ) ) ) <-> A. x e. A ( ( ( x G x ) ` ( ( Id ` C ) ` x ) ) = ( ( Id ` ( D |`cat R ) ) ` ( F ` x ) ) /\ A. y e. A A. z e. A A. f e. ( x H y ) A. g e. ( y H z ) ( ( x G z ) ` ( g ( <. x , y >. ( comp ` C ) z ) f ) ) = ( ( ( y G z ) ` g ) ( <. ( F ` x ) , ( F ` y ) >. ( comp ` ( D |`cat R ) ) ( F ` z ) ) ( ( x G y ) ` f ) ) ) ) )
102 27 84 101 3anbi123d 
 |-  ( ( ph /\ C e. Cat ) -> ( ( F : A --> ( Base ` D ) /\ G e. X_ z e. ( A X. A ) ( ( ( F ` ( 1st ` z ) ) ( Hom ` D ) ( F ` ( 2nd ` z ) ) ) ^m ( H ` z ) ) /\ A. x e. A ( ( ( x G x ) ` ( ( Id ` C ) ` x ) ) = ( ( Id ` D ) ` ( F ` x ) ) /\ A. y e. A A. z e. A A. f e. ( x H y ) A. g e. ( y H z ) ( ( x G z ) ` ( g ( <. x , y >. ( comp ` C ) z ) f ) ) = ( ( ( y G z ) ` g ) ( <. ( F ` x ) , ( F ` y ) >. ( comp ` D ) ( F ` z ) ) ( ( x G y ) ` f ) ) ) ) <-> ( F : A --> ( Base ` ( D |`cat R ) ) /\ G e. X_ z e. ( A X. A ) ( ( ( F ` ( 1st ` z ) ) ( Hom ` ( D |`cat R ) ) ( F ` ( 2nd ` z ) ) ) ^m ( H ` z ) ) /\ A. x e. A ( ( ( x G x ) ` ( ( Id ` C ) ` x ) ) = ( ( Id ` ( D |`cat R ) ) ` ( F ` x ) ) /\ A. y e. A A. z e. A A. f e. ( x H y ) A. g e. ( y H z ) ( ( x G z ) ` ( g ( <. x , y >. ( comp ` C ) z ) f ) ) = ( ( ( y G z ) ` g ) ( <. ( F ` x ) , ( F ` y ) >. ( comp ` ( D |`cat R ) ) ( F ` z ) ) ( ( x G y ) ` f ) ) ) ) ) )
103 eqid 
 |-  ( Id ` C ) = ( Id ` C )
104 eqid 
 |-  ( comp ` C ) = ( comp ` C )
105 simpr 
 |-  ( ( ph /\ C e. Cat ) -> C e. Cat )
106 22 adantr 
 |-  ( ( ph /\ C e. Cat ) -> D e. Cat )
107 1 17 2 32 103 87 104 92 105 106 isfunc 
 |-  ( ( ph /\ C e. Cat ) -> ( F ( C Func D ) G <-> ( F : A --> ( Base ` D ) /\ G e. X_ z e. ( A X. A ) ( ( ( F ` ( 1st ` z ) ) ( Hom ` D ) ( F ` ( 2nd ` z ) ) ) ^m ( H ` z ) ) /\ A. x e. A ( ( ( x G x ) ` ( ( Id ` C ) ` x ) ) = ( ( Id ` D ) ` ( F ` x ) ) /\ A. y e. A A. z e. A A. f e. ( x H y ) A. g e. ( y H z ) ( ( x G z ) ` ( g ( <. x , y >. ( comp ` C ) z ) f ) ) = ( ( ( y G z ) ` g ) ( <. ( F ` x ) , ( F ` y ) >. ( comp ` D ) ( F ` z ) ) ( ( x G y ) ` f ) ) ) ) ) )
108 eqid 
 |-  ( Base ` ( D |`cat R ) ) = ( Base ` ( D |`cat R ) )
109 eqid 
 |-  ( Hom ` ( D |`cat R ) ) = ( Hom ` ( D |`cat R ) )
110 eqid 
 |-  ( Id ` ( D |`cat R ) ) = ( Id ` ( D |`cat R ) )
111 eqid 
 |-  ( comp ` ( D |`cat R ) ) = ( comp ` ( D |`cat R ) )
112 20 3 subccat 
 |-  ( ph -> ( D |`cat R ) e. Cat )
113 112 adantr 
 |-  ( ( ph /\ C e. Cat ) -> ( D |`cat R ) e. Cat )
114 1 108 2 109 103 110 104 111 105 113 isfunc 
 |-  ( ( ph /\ C e. Cat ) -> ( F ( C Func ( D |`cat R ) ) G <-> ( F : A --> ( Base ` ( D |`cat R ) ) /\ G e. X_ z e. ( A X. A ) ( ( ( F ` ( 1st ` z ) ) ( Hom ` ( D |`cat R ) ) ( F ` ( 2nd ` z ) ) ) ^m ( H ` z ) ) /\ A. x e. A ( ( ( x G x ) ` ( ( Id ` C ) ` x ) ) = ( ( Id ` ( D |`cat R ) ) ` ( F ` x ) ) /\ A. y e. A A. z e. A A. f e. ( x H y ) A. g e. ( y H z ) ( ( x G z ) ` ( g ( <. x , y >. ( comp ` C ) z ) f ) ) = ( ( ( y G z ) ` g ) ( <. ( F ` x ) , ( F ` y ) >. ( comp ` ( D |`cat R ) ) ( F ` z ) ) ( ( x G y ) ` f ) ) ) ) ) )
115 102 107 114 3bitr4d 
 |-  ( ( ph /\ C e. Cat ) -> ( F ( C Func D ) G <-> F ( C Func ( D |`cat R ) ) G ) )
116 115 ex 
 |-  ( ph -> ( C e. Cat -> ( F ( C Func D ) G <-> F ( C Func ( D |`cat R ) ) G ) ) )
117 11 16 116 pm5.21ndd 
 |-  ( ph -> ( F ( C Func D ) G <-> F ( C Func ( D |`cat R ) ) G ) )