Metamath Proof Explorer

Theorem cofucl

Description: The composition of two functors is a functor. Proposition 3.23 of Adamek p. 33. (Contributed by Mario Carneiro, 3-Jan-2017)

Ref Expression
Hypotheses cofucl.f 
|- ( ph -> F e. ( C Func D ) )
cofucl.g 
|- ( ph -> G e. ( D Func E ) )
Assertion cofucl 
|- ( ph -> ( G o.func F ) e. ( C Func E ) )

Proof

Step Hyp Ref Expression
1 cofucl.f 
 |-  ( ph -> F e. ( C Func D ) )
2 cofucl.g 
 |-  ( ph -> G e. ( D Func E ) )
3 eqid 
 |-  ( Base ` C ) = ( Base ` C )
4 3 1 2 cofuval 
 |-  ( ph -> ( G o.func F ) = <. ( ( 1st ` G ) o. ( 1st ` F ) ) , ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> ( ( ( ( 1st ` F ) ` x ) ( 2nd ` G ) ( ( 1st ` F ) ` y ) ) o. ( x ( 2nd ` F ) y ) ) ) >. )
5 3 1 2 cofu1st 
 |-  ( ph -> ( 1st ` ( G o.func F ) ) = ( ( 1st ` G ) o. ( 1st ` F ) ) )
6 4 fveq2d 
 |-  ( ph -> ( 2nd ` ( G o.func F ) ) = ( 2nd ` <. ( ( 1st ` G ) o. ( 1st ` F ) ) , ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> ( ( ( ( 1st ` F ) ` x ) ( 2nd ` G ) ( ( 1st ` F ) ` y ) ) o. ( x ( 2nd ` F ) y ) ) ) >. ) )
7 fvex 
 |-  ( 1st ` G ) e. _V
8 fvex 
 |-  ( 1st ` F ) e. _V
9 7 8 coex 
 |-  ( ( 1st ` G ) o. ( 1st ` F ) ) e. _V
10 fvex 
 |-  ( Base ` C ) e. _V
11 10 10 mpoex 
 |-  ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> ( ( ( ( 1st ` F ) ` x ) ( 2nd ` G ) ( ( 1st ` F ) ` y ) ) o. ( x ( 2nd ` F ) y ) ) ) e. _V
12 9 11 op2nd 
 |-  ( 2nd ` <. ( ( 1st ` G ) o. ( 1st ` F ) ) , ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> ( ( ( ( 1st ` F ) ` x ) ( 2nd ` G ) ( ( 1st ` F ) ` y ) ) o. ( x ( 2nd ` F ) y ) ) ) >. ) = ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> ( ( ( ( 1st ` F ) ` x ) ( 2nd ` G ) ( ( 1st ` F ) ` y ) ) o. ( x ( 2nd ` F ) y ) ) )
13 6 12 eqtrdi 
 |-  ( ph -> ( 2nd ` ( G o.func F ) ) = ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> ( ( ( ( 1st ` F ) ` x ) ( 2nd ` G ) ( ( 1st ` F ) ` y ) ) o. ( x ( 2nd ` F ) y ) ) ) )
14 5 13 opeq12d 
 |-  ( ph -> <. ( 1st ` ( G o.func F ) ) , ( 2nd ` ( G o.func F ) ) >. = <. ( ( 1st ` G ) o. ( 1st ` F ) ) , ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> ( ( ( ( 1st ` F ) ` x ) ( 2nd ` G ) ( ( 1st ` F ) ` y ) ) o. ( x ( 2nd ` F ) y ) ) ) >. )
15 4 14 eqtr4d 
 |-  ( ph -> ( G o.func F ) = <. ( 1st ` ( G o.func F ) ) , ( 2nd ` ( G o.func F ) ) >. )
16 eqid 
 |-  ( Base ` D ) = ( Base ` D )
17 eqid 
 |-  ( Base ` E ) = ( Base ` E )
18 relfunc 
 |-  Rel ( D Func E )
19 1st2ndbr 
 |-  ( ( Rel ( D Func E ) /\ G e. ( D Func E ) ) -> ( 1st ` G ) ( D Func E ) ( 2nd ` G ) )
20 18 2 19 sylancr 
 |-  ( ph -> ( 1st ` G ) ( D Func E ) ( 2nd ` G ) )
21 16 17 20 funcf1 
 |-  ( ph -> ( 1st ` G ) : ( Base ` D ) --> ( Base ` E ) )
22 relfunc 
 |-  Rel ( C Func D )
23 1st2ndbr 
 |-  ( ( Rel ( C Func D ) /\ F e. ( C Func D ) ) -> ( 1st ` F ) ( C Func D ) ( 2nd ` F ) )
24 22 1 23 sylancr 
 |-  ( ph -> ( 1st ` F ) ( C Func D ) ( 2nd ` F ) )
25 3 16 24 funcf1 
 |-  ( ph -> ( 1st ` F ) : ( Base ` C ) --> ( Base ` D ) )
26 fco 
 |-  ( ( ( 1st ` G ) : ( Base ` D ) --> ( Base ` E ) /\ ( 1st ` F ) : ( Base ` C ) --> ( Base ` D ) ) -> ( ( 1st ` G ) o. ( 1st ` F ) ) : ( Base ` C ) --> ( Base ` E ) )
27 21 25 26 syl2anc 
 |-  ( ph -> ( ( 1st ` G ) o. ( 1st ` F ) ) : ( Base ` C ) --> ( Base ` E ) )
28 5 feq1d 
 |-  ( ph -> ( ( 1st ` ( G o.func F ) ) : ( Base ` C ) --> ( Base ` E ) <-> ( ( 1st ` G ) o. ( 1st ` F ) ) : ( Base ` C ) --> ( Base ` E ) ) )
29 27 28 mpbird 
 |-  ( ph -> ( 1st ` ( G o.func F ) ) : ( Base ` C ) --> ( Base ` E ) )
30 eqid 
 |-  ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> ( ( ( ( 1st ` F ) ` x ) ( 2nd ` G ) ( ( 1st ` F ) ` y ) ) o. ( x ( 2nd ` F ) y ) ) ) = ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> ( ( ( ( 1st ` F ) ` x ) ( 2nd ` G ) ( ( 1st ` F ) ` y ) ) o. ( x ( 2nd ` F ) y ) ) )
31 ovex 
 |-  ( ( ( 1st ` F ) ` x ) ( 2nd ` G ) ( ( 1st ` F ) ` y ) ) e. _V
32 ovex 
 |-  ( x ( 2nd ` F ) y ) e. _V
33 31 32 coex 
 |-  ( ( ( ( 1st ` F ) ` x ) ( 2nd ` G ) ( ( 1st ` F ) ` y ) ) o. ( x ( 2nd ` F ) y ) ) e. _V
34 30 33 fnmpoi 
 |-  ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> ( ( ( ( 1st ` F ) ` x ) ( 2nd ` G ) ( ( 1st ` F ) ` y ) ) o. ( x ( 2nd ` F ) y ) ) ) Fn ( ( Base ` C ) X. ( Base ` C ) )
35 13 fneq1d 
 |-  ( ph -> ( ( 2nd ` ( G o.func F ) ) Fn ( ( Base ` C ) X. ( Base ` C ) ) <-> ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> ( ( ( ( 1st ` F ) ` x ) ( 2nd ` G ) ( ( 1st ` F ) ` y ) ) o. ( x ( 2nd ` F ) y ) ) ) Fn ( ( Base ` C ) X. ( Base ` C ) ) ) )
36 34 35 mpbiri 
 |-  ( ph -> ( 2nd ` ( G o.func F ) ) Fn ( ( Base ` C ) X. ( Base ` C ) ) )
37 eqid 
 |-  ( Hom ` D ) = ( Hom ` D )
38 eqid 
 |-  ( Hom ` E ) = ( Hom ` E )
39 20 adantr 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ( 1st ` G ) ( D Func E ) ( 2nd ` G ) )
40 25 adantr 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ( 1st ` F ) : ( Base ` C ) --> ( Base ` D ) )
41 simprl 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> x e. ( Base ` C ) )
42 40 41 ffvelrnd 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ( ( 1st ` F ) ` x ) e. ( Base ` D ) )
43 simprr 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> y e. ( Base ` C ) )
44 40 43 ffvelrnd 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ( ( 1st ` F ) ` y ) e. ( Base ` D ) )
45 16 37 38 39 42 44 funcf2 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ( ( ( 1st ` F ) ` x ) ( 2nd ` G ) ( ( 1st ` F ) ` y ) ) : ( ( ( 1st ` F ) ` x ) ( Hom ` D ) ( ( 1st ` F ) ` y ) ) --> ( ( ( 1st ` G ) ` ( ( 1st ` F ) ` x ) ) ( Hom ` E ) ( ( 1st ` G ) ` ( ( 1st ` F ) ` y ) ) ) )
46 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
47 24 adantr 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ( 1st ` F ) ( C Func D ) ( 2nd ` F ) )
48 3 46 37 47 41 43 funcf2 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ( x ( 2nd ` F ) y ) : ( x ( Hom ` C ) y ) --> ( ( ( 1st ` F ) ` x ) ( Hom ` D ) ( ( 1st ` F ) ` y ) ) )
49 fco 
 |-  ( ( ( ( ( 1st ` F ) ` x ) ( 2nd ` G ) ( ( 1st ` F ) ` y ) ) : ( ( ( 1st ` F ) ` x ) ( Hom ` D ) ( ( 1st ` F ) ` y ) ) --> ( ( ( 1st ` G ) ` ( ( 1st ` F ) ` x ) ) ( Hom ` E ) ( ( 1st ` G ) ` ( ( 1st ` F ) ` y ) ) ) /\ ( x ( 2nd ` F ) y ) : ( x ( Hom ` C ) y ) --> ( ( ( 1st ` F ) ` x ) ( Hom ` D ) ( ( 1st ` F ) ` y ) ) ) -> ( ( ( ( 1st ` F ) ` x ) ( 2nd ` G ) ( ( 1st ` F ) ` y ) ) o. ( x ( 2nd ` F ) y ) ) : ( x ( Hom ` C ) y ) --> ( ( ( 1st ` G ) ` ( ( 1st ` F ) ` x ) ) ( Hom ` E ) ( ( 1st ` G ) ` ( ( 1st ` F ) ` y ) ) ) )
50 45 48 49 syl2anc 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ( ( ( ( 1st ` F ) ` x ) ( 2nd ` G ) ( ( 1st ` F ) ` y ) ) o. ( x ( 2nd ` F ) y ) ) : ( x ( Hom ` C ) y ) --> ( ( ( 1st ` G ) ` ( ( 1st ` F ) ` x ) ) ( Hom ` E ) ( ( 1st ` G ) ` ( ( 1st ` F ) ` y ) ) ) )
51 ovex 
 |-  ( ( ( 1st ` G ) ` ( ( 1st ` F ) ` x ) ) ( Hom ` E ) ( ( 1st ` G ) ` ( ( 1st ` F ) ` y ) ) ) e. _V
52 ovex 
 |-  ( x ( Hom ` C ) y ) e. _V
53 51 52 elmap 
 |-  ( ( ( ( ( 1st ` F ) ` x ) ( 2nd ` G ) ( ( 1st ` F ) ` y ) ) o. ( x ( 2nd ` F ) y ) ) e. ( ( ( ( 1st ` G ) ` ( ( 1st ` F ) ` x ) ) ( Hom ` E ) ( ( 1st ` G ) ` ( ( 1st ` F ) ` y ) ) ) ^m ( x ( Hom ` C ) y ) ) <-> ( ( ( ( 1st ` F ) ` x ) ( 2nd ` G ) ( ( 1st ` F ) ` y ) ) o. ( x ( 2nd ` F ) y ) ) : ( x ( Hom ` C ) y ) --> ( ( ( 1st ` G ) ` ( ( 1st ` F ) ` x ) ) ( Hom ` E ) ( ( 1st ` G ) ` ( ( 1st ` F ) ` y ) ) ) )
54 50 53 sylibr 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ( ( ( ( 1st ` F ) ` x ) ( 2nd ` G ) ( ( 1st ` F ) ` y ) ) o. ( x ( 2nd ` F ) y ) ) e. ( ( ( ( 1st ` G ) ` ( ( 1st ` F ) ` x ) ) ( Hom ` E ) ( ( 1st ` G ) ` ( ( 1st ` F ) ` y ) ) ) ^m ( x ( Hom ` C ) y ) ) )
55 1 adantr 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> F e. ( C Func D ) )
56 2 adantr 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> G e. ( D Func E ) )
57 3 55 56 41 43 cofu2nd 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ( x ( 2nd ` ( G o.func F ) ) y ) = ( ( ( ( 1st ` F ) ` x ) ( 2nd ` G ) ( ( 1st ` F ) ` y ) ) o. ( x ( 2nd ` F ) y ) ) )
58 3 55 56 41 cofu1 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ( ( 1st ` ( G o.func F ) ) ` x ) = ( ( 1st ` G ) ` ( ( 1st ` F ) ` x ) ) )
59 3 55 56 43 cofu1 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ( ( 1st ` ( G o.func F ) ) ` y ) = ( ( 1st ` G ) ` ( ( 1st ` F ) ` y ) ) )
60 58 59 oveq12d 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ( ( ( 1st ` ( G o.func F ) ) ` x ) ( Hom ` E ) ( ( 1st ` ( G o.func F ) ) ` y ) ) = ( ( ( 1st ` G ) ` ( ( 1st ` F ) ` x ) ) ( Hom ` E ) ( ( 1st ` G ) ` ( ( 1st ` F ) ` y ) ) ) )
61 60 oveq1d 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ( ( ( ( 1st ` ( G o.func F ) ) ` x ) ( Hom ` E ) ( ( 1st ` ( G o.func F ) ) ` y ) ) ^m ( x ( Hom ` C ) y ) ) = ( ( ( ( 1st ` G ) ` ( ( 1st ` F ) ` x ) ) ( Hom ` E ) ( ( 1st ` G ) ` ( ( 1st ` F ) ` y ) ) ) ^m ( x ( Hom ` C ) y ) ) )
62 54 57 61 3eltr4d 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ( x ( 2nd ` ( G o.func F ) ) y ) e. ( ( ( ( 1st ` ( G o.func F ) ) ` x ) ( Hom ` E ) ( ( 1st ` ( G o.func F ) ) ` y ) ) ^m ( x ( Hom ` C ) y ) ) )
63 62 ralrimivva 
 |-  ( ph -> A. x e. ( Base ` C ) A. y e. ( Base ` C ) ( x ( 2nd ` ( G o.func F ) ) y ) e. ( ( ( ( 1st ` ( G o.func F ) ) ` x ) ( Hom ` E ) ( ( 1st ` ( G o.func F ) ) ` y ) ) ^m ( x ( Hom ` C ) y ) ) )
64 fveq2 
 |-  ( z = <. x , y >. -> ( ( 2nd ` ( G o.func F ) ) ` z ) = ( ( 2nd ` ( G o.func F ) ) ` <. x , y >. ) )
65 df-ov 
 |-  ( x ( 2nd ` ( G o.func F ) ) y ) = ( ( 2nd ` ( G o.func F ) ) ` <. x , y >. )
66 64 65 eqtr4di 
 |-  ( z = <. x , y >. -> ( ( 2nd ` ( G o.func F ) ) ` z ) = ( x ( 2nd ` ( G o.func F ) ) y ) )
67 vex 
 |-  x e. _V
68 vex 
 |-  y e. _V
69 67 68 op1std 
 |-  ( z = <. x , y >. -> ( 1st ` z ) = x )
70 69 fveq2d 
 |-  ( z = <. x , y >. -> ( ( 1st ` ( G o.func F ) ) ` ( 1st ` z ) ) = ( ( 1st ` ( G o.func F ) ) ` x ) )
71 67 68 op2ndd 
 |-  ( z = <. x , y >. -> ( 2nd ` z ) = y )
72 71 fveq2d 
 |-  ( z = <. x , y >. -> ( ( 1st ` ( G o.func F ) ) ` ( 2nd ` z ) ) = ( ( 1st ` ( G o.func F ) ) ` y ) )
73 70 72 oveq12d 
 |-  ( z = <. x , y >. -> ( ( ( 1st ` ( G o.func F ) ) ` ( 1st ` z ) ) ( Hom ` E ) ( ( 1st ` ( G o.func F ) ) ` ( 2nd ` z ) ) ) = ( ( ( 1st ` ( G o.func F ) ) ` x ) ( Hom ` E ) ( ( 1st ` ( G o.func F ) ) ` y ) ) )
74 fveq2 
 |-  ( z = <. x , y >. -> ( ( Hom ` C ) ` z ) = ( ( Hom ` C ) ` <. x , y >. ) )
75 df-ov 
 |-  ( x ( Hom ` C ) y ) = ( ( Hom ` C ) ` <. x , y >. )
76 74 75 eqtr4di 
 |-  ( z = <. x , y >. -> ( ( Hom ` C ) ` z ) = ( x ( Hom ` C ) y ) )
77 73 76 oveq12d 
 |-  ( z = <. x , y >. -> ( ( ( ( 1st ` ( G o.func F ) ) ` ( 1st ` z ) ) ( Hom ` E ) ( ( 1st ` ( G o.func F ) ) ` ( 2nd ` z ) ) ) ^m ( ( Hom ` C ) ` z ) ) = ( ( ( ( 1st ` ( G o.func F ) ) ` x ) ( Hom ` E ) ( ( 1st ` ( G o.func F ) ) ` y ) ) ^m ( x ( Hom ` C ) y ) ) )
78 66 77 eleq12d 
 |-  ( z = <. x , y >. -> ( ( ( 2nd ` ( G o.func F ) ) ` z ) e. ( ( ( ( 1st ` ( G o.func F ) ) ` ( 1st ` z ) ) ( Hom ` E ) ( ( 1st ` ( G o.func F ) ) ` ( 2nd ` z ) ) ) ^m ( ( Hom ` C ) ` z ) ) <-> ( x ( 2nd ` ( G o.func F ) ) y ) e. ( ( ( ( 1st ` ( G o.func F ) ) ` x ) ( Hom ` E ) ( ( 1st ` ( G o.func F ) ) ` y ) ) ^m ( x ( Hom ` C ) y ) ) ) )
79 78 ralxp 
 |-  ( A. z e. ( ( Base ` C ) X. ( Base ` C ) ) ( ( 2nd ` ( G o.func F ) ) ` z ) e. ( ( ( ( 1st ` ( G o.func F ) ) ` ( 1st ` z ) ) ( Hom ` E ) ( ( 1st ` ( G o.func F ) ) ` ( 2nd ` z ) ) ) ^m ( ( Hom ` C ) ` z ) ) <-> A. x e. ( Base ` C ) A. y e. ( Base ` C ) ( x ( 2nd ` ( G o.func F ) ) y ) e. ( ( ( ( 1st ` ( G o.func F ) ) ` x ) ( Hom ` E ) ( ( 1st ` ( G o.func F ) ) ` y ) ) ^m ( x ( Hom ` C ) y ) ) )
80 63 79 sylibr 
 |-  ( ph -> A. z e. ( ( Base ` C ) X. ( Base ` C ) ) ( ( 2nd ` ( G o.func F ) ) ` z ) e. ( ( ( ( 1st ` ( G o.func F ) ) ` ( 1st ` z ) ) ( Hom ` E ) ( ( 1st ` ( G o.func F ) ) ` ( 2nd ` z ) ) ) ^m ( ( Hom ` C ) ` z ) ) )
81 fvex 
 |-  ( 2nd ` ( G o.func F ) ) e. _V
82 81 elixp 
 |-  ( ( 2nd ` ( G o.func F ) ) e. X_ z e. ( ( Base ` C ) X. ( Base ` C ) ) ( ( ( ( 1st ` ( G o.func F ) ) ` ( 1st ` z ) ) ( Hom ` E ) ( ( 1st ` ( G o.func F ) ) ` ( 2nd ` z ) ) ) ^m ( ( Hom ` C ) ` z ) ) <-> ( ( 2nd ` ( G o.func F ) ) Fn ( ( Base ` C ) X. ( Base ` C ) ) /\ A. z e. ( ( Base ` C ) X. ( Base ` C ) ) ( ( 2nd ` ( G o.func F ) ) ` z ) e. ( ( ( ( 1st ` ( G o.func F ) ) ` ( 1st ` z ) ) ( Hom ` E ) ( ( 1st ` ( G o.func F ) ) ` ( 2nd ` z ) ) ) ^m ( ( Hom ` C ) ` z ) ) ) )
83 36 80 82 sylanbrc 
 |-  ( ph -> ( 2nd ` ( G o.func F ) ) e. X_ z e. ( ( Base ` C ) X. ( Base ` C ) ) ( ( ( ( 1st ` ( G o.func F ) ) ` ( 1st ` z ) ) ( Hom ` E ) ( ( 1st ` ( G o.func F ) ) ` ( 2nd ` z ) ) ) ^m ( ( Hom ` C ) ` z ) ) )
84 eqid 
 |-  ( Id ` C ) = ( Id ` C )
85 eqid 
 |-  ( Id ` D ) = ( Id ` D )
86 24 adantr 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( 1st ` F ) ( C Func D ) ( 2nd ` F ) )
87 simpr 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> x e. ( Base ` C ) )
88 3 84 85 86 87 funcid 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( x ( 2nd ` F ) x ) ` ( ( Id ` C ) ` x ) ) = ( ( Id ` D ) ` ( ( 1st ` F ) ` x ) ) )
89 88 fveq2d 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( ( ( 1st ` F ) ` x ) ( 2nd ` G ) ( ( 1st ` F ) ` x ) ) ` ( ( x ( 2nd ` F ) x ) ` ( ( Id ` C ) ` x ) ) ) = ( ( ( ( 1st ` F ) ` x ) ( 2nd ` G ) ( ( 1st ` F ) ` x ) ) ` ( ( Id ` D ) ` ( ( 1st ` F ) ` x ) ) ) )
90 eqid 
 |-  ( Id ` E ) = ( Id ` E )
91 20 adantr 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( 1st ` G ) ( D Func E ) ( 2nd ` G ) )
92 25 ffvelrnda 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( 1st ` F ) ` x ) e. ( Base ` D ) )
93 16 85 90 91 92 funcid 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( ( ( 1st ` F ) ` x ) ( 2nd ` G ) ( ( 1st ` F ) ` x ) ) ` ( ( Id ` D ) ` ( ( 1st ` F ) ` x ) ) ) = ( ( Id ` E ) ` ( ( 1st ` G ) ` ( ( 1st ` F ) ` x ) ) ) )
94 89 93 eqtrd 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( ( ( 1st ` F ) ` x ) ( 2nd ` G ) ( ( 1st ` F ) ` x ) ) ` ( ( x ( 2nd ` F ) x ) ` ( ( Id ` C ) ` x ) ) ) = ( ( Id ` E ) ` ( ( 1st ` G ) ` ( ( 1st ` F ) ` x ) ) ) )
95 1 adantr 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> F e. ( C Func D ) )
96 2 adantr 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> G e. ( D Func E ) )
97 funcrcl 
 |-  ( F e. ( C Func D ) -> ( C e. Cat /\ D e. Cat ) )
98 1 97 syl 
 |-  ( ph -> ( C e. Cat /\ D e. Cat ) )
99 98 simpld 
 |-  ( ph -> C e. Cat )
100 99 adantr 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> C e. Cat )
101 3 46 84 100 87 catidcl 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( Id ` C ) ` x ) e. ( x ( Hom ` C ) x ) )
102 3 95 96 87 87 46 101 cofu2 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( x ( 2nd ` ( G o.func F ) ) x ) ` ( ( Id ` C ) ` x ) ) = ( ( ( ( 1st ` F ) ` x ) ( 2nd ` G ) ( ( 1st ` F ) ` x ) ) ` ( ( x ( 2nd ` F ) x ) ` ( ( Id ` C ) ` x ) ) ) )
103 3 95 96 87 cofu1 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( 1st ` ( G o.func F ) ) ` x ) = ( ( 1st ` G ) ` ( ( 1st ` F ) ` x ) ) )
104 103 fveq2d 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( Id ` E ) ` ( ( 1st ` ( G o.func F ) ) ` x ) ) = ( ( Id ` E ) ` ( ( 1st ` G ) ` ( ( 1st ` F ) ` x ) ) ) )
105 94 102 104 3eqtr4d 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( x ( 2nd ` ( G o.func F ) ) x ) ` ( ( Id ` C ) ` x ) ) = ( ( Id ` E ) ` ( ( 1st ` ( G o.func F ) ) ` x ) ) )
106 86 adantr 
 |-  ( ( ( ph /\ x e. ( Base ` C ) ) /\ ( ( y e. ( Base ` C ) /\ z e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) ) ) ) -> ( 1st ` F ) ( C Func D ) ( 2nd ` F ) )
107 simplr 
 |-  ( ( ( ph /\ x e. ( Base ` C ) ) /\ ( ( y e. ( Base ` C ) /\ z e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) ) ) ) -> x e. ( Base ` C ) )
108 simprlr 
 |-  ( ( ( ph /\ x e. ( Base ` C ) ) /\ ( ( y e. ( Base ` C ) /\ z e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) ) ) ) -> z e. ( Base ` C ) )
109 3 46 37 106 107 108 funcf2 
 |-  ( ( ( ph /\ x e. ( Base ` C ) ) /\ ( ( y e. ( Base ` C ) /\ z e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) ) ) ) -> ( x ( 2nd ` F ) z ) : ( x ( Hom ` C ) z ) --> ( ( ( 1st ` F ) ` x ) ( Hom ` D ) ( ( 1st ` F ) ` z ) ) )
110 eqid 
 |-  ( comp ` C ) = ( comp ` C )
111 100 adantr 
 |-  ( ( ( ph /\ x e. ( Base ` C ) ) /\ ( ( y e. ( Base ` C ) /\ z e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) ) ) ) -> C e. Cat )
112 simprll 
 |-  ( ( ( ph /\ x e. ( Base ` C ) ) /\ ( ( y e. ( Base ` C ) /\ z e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) ) ) ) -> y e. ( Base ` C ) )
113 simprrl 
 |-  ( ( ( ph /\ x e. ( Base ` C ) ) /\ ( ( y e. ( Base ` C ) /\ z e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) ) ) ) -> f e. ( x ( Hom ` C ) y ) )
114 simprrr 
 |-  ( ( ( ph /\ x e. ( Base ` C ) ) /\ ( ( y e. ( Base ` C ) /\ z e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) ) ) ) -> g e. ( y ( Hom ` C ) z ) )
115 3 46 110 111 107 112 108 113 114 catcocl 
 |-  ( ( ( ph /\ x e. ( Base ` C ) ) /\ ( ( y e. ( Base ` C ) /\ z e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) ) ) ) -> ( g ( <. x , y >. ( comp ` C ) z ) f ) e. ( x ( Hom ` C ) z ) )
116 fvco3 
 |-  ( ( ( x ( 2nd ` F ) z ) : ( x ( Hom ` C ) z ) --> ( ( ( 1st ` F ) ` x ) ( Hom ` D ) ( ( 1st ` F ) ` z ) ) /\ ( g ( <. x , y >. ( comp ` C ) z ) f ) e. ( x ( Hom ` C ) z ) ) -> ( ( ( ( ( 1st ` F ) ` x ) ( 2nd ` G ) ( ( 1st ` F ) ` z ) ) o. ( x ( 2nd ` F ) z ) ) ` ( g ( <. x , y >. ( comp ` C ) z ) f ) ) = ( ( ( ( 1st ` F ) ` x ) ( 2nd ` G ) ( ( 1st ` F ) ` z ) ) ` ( ( x ( 2nd ` F ) z ) ` ( g ( <. x , y >. ( comp ` C ) z ) f ) ) ) )
117 109 115 116 syl2anc 
 |-  ( ( ( ph /\ x e. ( Base ` C ) ) /\ ( ( y e. ( Base ` C ) /\ z e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) ) ) ) -> ( ( ( ( ( 1st ` F ) ` x ) ( 2nd ` G ) ( ( 1st ` F ) ` z ) ) o. ( x ( 2nd ` F ) z ) ) ` ( g ( <. x , y >. ( comp ` C ) z ) f ) ) = ( ( ( ( 1st ` F ) ` x ) ( 2nd ` G ) ( ( 1st ` F ) ` z ) ) ` ( ( x ( 2nd ` F ) z ) ` ( g ( <. x , y >. ( comp ` C ) z ) f ) ) ) )
118 eqid 
 |-  ( comp ` D ) = ( comp ` D )
119 3 46 110 118 106 107 112 108 113 114 funcco 
 |-  ( ( ( ph /\ x e. ( Base ` C ) ) /\ ( ( y e. ( Base ` C ) /\ z e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) ) ) ) -> ( ( x ( 2nd ` F ) z ) ` ( g ( <. x , y >. ( comp ` C ) z ) f ) ) = ( ( ( y ( 2nd ` F ) z ) ` g ) ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` F ) ` y ) >. ( comp ` D ) ( ( 1st ` F ) ` z ) ) ( ( x ( 2nd ` F ) y ) ` f ) ) )
120 119 fveq2d 
 |-  ( ( ( ph /\ x e. ( Base ` C ) ) /\ ( ( y e. ( Base ` C ) /\ z e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) ) ) ) -> ( ( ( ( 1st ` F ) ` x ) ( 2nd ` G ) ( ( 1st ` F ) ` z ) ) ` ( ( x ( 2nd ` F ) z ) ` ( g ( <. x , y >. ( comp ` C ) z ) f ) ) ) = ( ( ( ( 1st ` F ) ` x ) ( 2nd ` G ) ( ( 1st ` F ) ` z ) ) ` ( ( ( y ( 2nd ` F ) z ) ` g ) ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` F ) ` y ) >. ( comp ` D ) ( ( 1st ` F ) ` z ) ) ( ( x ( 2nd ` F ) y ) ` f ) ) ) )
121 eqid 
 |-  ( comp ` E ) = ( comp ` E )
122 91 adantr 
 |-  ( ( ( ph /\ x e. ( Base ` C ) ) /\ ( ( y e. ( Base ` C ) /\ z e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) ) ) ) -> ( 1st ` G ) ( D Func E ) ( 2nd ` G ) )
123 92 adantr 
 |-  ( ( ( ph /\ x e. ( Base ` C ) ) /\ ( ( y e. ( Base ` C ) /\ z e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) ) ) ) -> ( ( 1st ` F ) ` x ) e. ( Base ` D ) )
124 25 adantr 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( 1st ` F ) : ( Base ` C ) --> ( Base ` D ) )
125 124 adantr 
 |-  ( ( ( ph /\ x e. ( Base ` C ) ) /\ ( ( y e. ( Base ` C ) /\ z e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) ) ) ) -> ( 1st ` F ) : ( Base ` C ) --> ( Base ` D ) )
126 125 112 ffvelrnd 
 |-  ( ( ( ph /\ x e. ( Base ` C ) ) /\ ( ( y e. ( Base ` C ) /\ z e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) ) ) ) -> ( ( 1st ` F ) ` y ) e. ( Base ` D ) )
127 125 108 ffvelrnd 
 |-  ( ( ( ph /\ x e. ( Base ` C ) ) /\ ( ( y e. ( Base ` C ) /\ z e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) ) ) ) -> ( ( 1st ` F ) ` z ) e. ( Base ` D ) )
128 3 46 37 106 107 112 funcf2 
 |-  ( ( ( ph /\ x e. ( Base ` C ) ) /\ ( ( y e. ( Base ` C ) /\ z e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) ) ) ) -> ( x ( 2nd ` F ) y ) : ( x ( Hom ` C ) y ) --> ( ( ( 1st ` F ) ` x ) ( Hom ` D ) ( ( 1st ` F ) ` y ) ) )
129 128 113 ffvelrnd 
 |-  ( ( ( ph /\ x e. ( Base ` C ) ) /\ ( ( y e. ( Base ` C ) /\ z e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) ) ) ) -> ( ( x ( 2nd ` F ) y ) ` f ) e. ( ( ( 1st ` F ) ` x ) ( Hom ` D ) ( ( 1st ` F ) ` y ) ) )
130 3 46 37 106 112 108 funcf2 
 |-  ( ( ( ph /\ x e. ( Base ` C ) ) /\ ( ( y e. ( Base ` C ) /\ z e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) ) ) ) -> ( y ( 2nd ` F ) z ) : ( y ( Hom ` C ) z ) --> ( ( ( 1st ` F ) ` y ) ( Hom ` D ) ( ( 1st ` F ) ` z ) ) )
131 130 114 ffvelrnd 
 |-  ( ( ( ph /\ x e. ( Base ` C ) ) /\ ( ( y e. ( Base ` C ) /\ z e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) ) ) ) -> ( ( y ( 2nd ` F ) z ) ` g ) e. ( ( ( 1st ` F ) ` y ) ( Hom ` D ) ( ( 1st ` F ) ` z ) ) )
132 16 37 118 121 122 123 126 127 129 131 funcco 
 |-  ( ( ( ph /\ x e. ( Base ` C ) ) /\ ( ( y e. ( Base ` C ) /\ z e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) ) ) ) -> ( ( ( ( 1st ` F ) ` x ) ( 2nd ` G ) ( ( 1st ` F ) ` z ) ) ` ( ( ( y ( 2nd ` F ) z ) ` g ) ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` F ) ` y ) >. ( comp ` D ) ( ( 1st ` F ) ` z ) ) ( ( x ( 2nd ` F ) y ) ` f ) ) ) = ( ( ( ( ( 1st ` F ) ` y ) ( 2nd ` G ) ( ( 1st ` F ) ` z ) ) ` ( ( y ( 2nd ` F ) z ) ` g ) ) ( <. ( ( 1st ` G ) ` ( ( 1st ` F ) ` x ) ) , ( ( 1st ` G ) ` ( ( 1st ` F ) ` y ) ) >. ( comp ` E ) ( ( 1st ` G ) ` ( ( 1st ` F ) ` z ) ) ) ( ( ( ( 1st ` F ) ` x ) ( 2nd ` G ) ( ( 1st ` F ) ` y ) ) ` ( ( x ( 2nd ` F ) y ) ` f ) ) ) )
133 117 120 132 3eqtrd 
 |-  ( ( ( ph /\ x e. ( Base ` C ) ) /\ ( ( y e. ( Base ` C ) /\ z e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) ) ) ) -> ( ( ( ( ( 1st ` F ) ` x ) ( 2nd ` G ) ( ( 1st ` F ) ` z ) ) o. ( x ( 2nd ` F ) z ) ) ` ( g ( <. x , y >. ( comp ` C ) z ) f ) ) = ( ( ( ( ( 1st ` F ) ` y ) ( 2nd ` G ) ( ( 1st ` F ) ` z ) ) ` ( ( y ( 2nd ` F ) z ) ` g ) ) ( <. ( ( 1st ` G ) ` ( ( 1st ` F ) ` x ) ) , ( ( 1st ` G ) ` ( ( 1st ` F ) ` y ) ) >. ( comp ` E ) ( ( 1st ` G ) ` ( ( 1st ` F ) ` z ) ) ) ( ( ( ( 1st ` F ) ` x ) ( 2nd ` G ) ( ( 1st ` F ) ` y ) ) ` ( ( x ( 2nd ` F ) y ) ` f ) ) ) )
134 95 adantr 
 |-  ( ( ( ph /\ x e. ( Base ` C ) ) /\ ( ( y e. ( Base ` C ) /\ z e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) ) ) ) -> F e. ( C Func D ) )
135 96 adantr 
 |-  ( ( ( ph /\ x e. ( Base ` C ) ) /\ ( ( y e. ( Base ` C ) /\ z e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) ) ) ) -> G e. ( D Func E ) )
136 3 134 135 107 108 cofu2nd 
 |-  ( ( ( ph /\ x e. ( Base ` C ) ) /\ ( ( y e. ( Base ` C ) /\ z e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) ) ) ) -> ( x ( 2nd ` ( G o.func F ) ) z ) = ( ( ( ( 1st ` F ) ` x ) ( 2nd ` G ) ( ( 1st ` F ) ` z ) ) o. ( x ( 2nd ` F ) z ) ) )
137 136 fveq1d 
 |-  ( ( ( ph /\ x e. ( Base ` C ) ) /\ ( ( y e. ( Base ` C ) /\ z e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) ) ) ) -> ( ( x ( 2nd ` ( G o.func F ) ) z ) ` ( g ( <. x , y >. ( comp ` C ) z ) f ) ) = ( ( ( ( ( 1st ` F ) ` x ) ( 2nd ` G ) ( ( 1st ` F ) ` z ) ) o. ( x ( 2nd ` F ) z ) ) ` ( g ( <. x , y >. ( comp ` C ) z ) f ) ) )
138 103 adantr 
 |-  ( ( ( ph /\ x e. ( Base ` C ) ) /\ ( ( y e. ( Base ` C ) /\ z e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) ) ) ) -> ( ( 1st ` ( G o.func F ) ) ` x ) = ( ( 1st ` G ) ` ( ( 1st ` F ) ` x ) ) )
139 3 134 135 112 cofu1 
 |-  ( ( ( ph /\ x e. ( Base ` C ) ) /\ ( ( y e. ( Base ` C ) /\ z e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) ) ) ) -> ( ( 1st ` ( G o.func F ) ) ` y ) = ( ( 1st ` G ) ` ( ( 1st ` F ) ` y ) ) )
140 138 139 opeq12d 
 |-  ( ( ( ph /\ x e. ( Base ` C ) ) /\ ( ( y e. ( Base ` C ) /\ z e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) ) ) ) -> <. ( ( 1st ` ( G o.func F ) ) ` x ) , ( ( 1st ` ( G o.func F ) ) ` y ) >. = <. ( ( 1st ` G ) ` ( ( 1st ` F ) ` x ) ) , ( ( 1st ` G ) ` ( ( 1st ` F ) ` y ) ) >. )
141 3 134 135 108 cofu1 
 |-  ( ( ( ph /\ x e. ( Base ` C ) ) /\ ( ( y e. ( Base ` C ) /\ z e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) ) ) ) -> ( ( 1st ` ( G o.func F ) ) ` z ) = ( ( 1st ` G ) ` ( ( 1st ` F ) ` z ) ) )
142 140 141 oveq12d 
 |-  ( ( ( ph /\ x e. ( Base ` C ) ) /\ ( ( y e. ( Base ` C ) /\ z e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) ) ) ) -> ( <. ( ( 1st ` ( G o.func F ) ) ` x ) , ( ( 1st ` ( G o.func F ) ) ` y ) >. ( comp ` E ) ( ( 1st ` ( G o.func F ) ) ` z ) ) = ( <. ( ( 1st ` G ) ` ( ( 1st ` F ) ` x ) ) , ( ( 1st ` G ) ` ( ( 1st ` F ) ` y ) ) >. ( comp ` E ) ( ( 1st ` G ) ` ( ( 1st ` F ) ` z ) ) ) )
143 3 134 135 112 108 46 114 cofu2 
 |-  ( ( ( ph /\ x e. ( Base ` C ) ) /\ ( ( y e. ( Base ` C ) /\ z e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) ) ) ) -> ( ( y ( 2nd ` ( G o.func F ) ) z ) ` g ) = ( ( ( ( 1st ` F ) ` y ) ( 2nd ` G ) ( ( 1st ` F ) ` z ) ) ` ( ( y ( 2nd ` F ) z ) ` g ) ) )
144 3 134 135 107 112 46 113 cofu2 
 |-  ( ( ( ph /\ x e. ( Base ` C ) ) /\ ( ( y e. ( Base ` C ) /\ z e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) ) ) ) -> ( ( x ( 2nd ` ( G o.func F ) ) y ) ` f ) = ( ( ( ( 1st ` F ) ` x ) ( 2nd ` G ) ( ( 1st ` F ) ` y ) ) ` ( ( x ( 2nd ` F ) y ) ` f ) ) )
145 142 143 144 oveq123d 
 |-  ( ( ( ph /\ x e. ( Base ` C ) ) /\ ( ( y e. ( Base ` C ) /\ z e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) ) ) ) -> ( ( ( y ( 2nd ` ( G o.func F ) ) z ) ` g ) ( <. ( ( 1st ` ( G o.func F ) ) ` x ) , ( ( 1st ` ( G o.func F ) ) ` y ) >. ( comp ` E ) ( ( 1st ` ( G o.func F ) ) ` z ) ) ( ( x ( 2nd ` ( G o.func F ) ) y ) ` f ) ) = ( ( ( ( ( 1st ` F ) ` y ) ( 2nd ` G ) ( ( 1st ` F ) ` z ) ) ` ( ( y ( 2nd ` F ) z ) ` g ) ) ( <. ( ( 1st ` G ) ` ( ( 1st ` F ) ` x ) ) , ( ( 1st ` G ) ` ( ( 1st ` F ) ` y ) ) >. ( comp ` E ) ( ( 1st ` G ) ` ( ( 1st ` F ) ` z ) ) ) ( ( ( ( 1st ` F ) ` x ) ( 2nd ` G ) ( ( 1st ` F ) ` y ) ) ` ( ( x ( 2nd ` F ) y ) ` f ) ) ) )
146 133 137 145 3eqtr4d 
 |-  ( ( ( ph /\ x e. ( Base ` C ) ) /\ ( ( y e. ( Base ` C ) /\ z e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) ) ) ) -> ( ( x ( 2nd ` ( G o.func F ) ) z ) ` ( g ( <. x , y >. ( comp ` C ) z ) f ) ) = ( ( ( y ( 2nd ` ( G o.func F ) ) z ) ` g ) ( <. ( ( 1st ` ( G o.func F ) ) ` x ) , ( ( 1st ` ( G o.func F ) ) ` y ) >. ( comp ` E ) ( ( 1st ` ( G o.func F ) ) ` z ) ) ( ( x ( 2nd ` ( G o.func F ) ) y ) ` f ) ) )
147 146 anassrs 
 |-  ( ( ( ( ph /\ x e. ( Base ` C ) ) /\ ( y e. ( Base ` C ) /\ z e. ( Base ` C ) ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) ) ) -> ( ( x ( 2nd ` ( G o.func F ) ) z ) ` ( g ( <. x , y >. ( comp ` C ) z ) f ) ) = ( ( ( y ( 2nd ` ( G o.func F ) ) z ) ` g ) ( <. ( ( 1st ` ( G o.func F ) ) ` x ) , ( ( 1st ` ( G o.func F ) ) ` y ) >. ( comp ` E ) ( ( 1st ` ( G o.func F ) ) ` z ) ) ( ( x ( 2nd ` ( G o.func F ) ) y ) ` f ) ) )
148 147 ralrimivva 
 |-  ( ( ( ph /\ x e. ( Base ` C ) ) /\ ( y e. ( Base ` C ) /\ z e. ( Base ` C ) ) ) -> A. f e. ( x ( Hom ` C ) y ) A. g e. ( y ( Hom ` C ) z ) ( ( x ( 2nd ` ( G o.func F ) ) z ) ` ( g ( <. x , y >. ( comp ` C ) z ) f ) ) = ( ( ( y ( 2nd ` ( G o.func F ) ) z ) ` g ) ( <. ( ( 1st ` ( G o.func F ) ) ` x ) , ( ( 1st ` ( G o.func F ) ) ` y ) >. ( comp ` E ) ( ( 1st ` ( G o.func F ) ) ` z ) ) ( ( x ( 2nd ` ( G o.func F ) ) y ) ` f ) ) )
149 148 ralrimivva 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> A. y e. ( Base ` C ) A. z e. ( Base ` C ) A. f e. ( x ( Hom ` C ) y ) A. g e. ( y ( Hom ` C ) z ) ( ( x ( 2nd ` ( G o.func F ) ) z ) ` ( g ( <. x , y >. ( comp ` C ) z ) f ) ) = ( ( ( y ( 2nd ` ( G o.func F ) ) z ) ` g ) ( <. ( ( 1st ` ( G o.func F ) ) ` x ) , ( ( 1st ` ( G o.func F ) ) ` y ) >. ( comp ` E ) ( ( 1st ` ( G o.func F ) ) ` z ) ) ( ( x ( 2nd ` ( G o.func F ) ) y ) ` f ) ) )
150 105 149 jca 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( ( x ( 2nd ` ( G o.func F ) ) x ) ` ( ( Id ` C ) ` x ) ) = ( ( Id ` E ) ` ( ( 1st ` ( G o.func F ) ) ` x ) ) /\ A. y e. ( Base ` C ) A. z e. ( Base ` C ) A. f e. ( x ( Hom ` C ) y ) A. g e. ( y ( Hom ` C ) z ) ( ( x ( 2nd ` ( G o.func F ) ) z ) ` ( g ( <. x , y >. ( comp ` C ) z ) f ) ) = ( ( ( y ( 2nd ` ( G o.func F ) ) z ) ` g ) ( <. ( ( 1st ` ( G o.func F ) ) ` x ) , ( ( 1st ` ( G o.func F ) ) ` y ) >. ( comp ` E ) ( ( 1st ` ( G o.func F ) ) ` z ) ) ( ( x ( 2nd ` ( G o.func F ) ) y ) ` f ) ) ) )
151 150 ralrimiva 
 |-  ( ph -> A. x e. ( Base ` C ) ( ( ( x ( 2nd ` ( G o.func F ) ) x ) ` ( ( Id ` C ) ` x ) ) = ( ( Id ` E ) ` ( ( 1st ` ( G o.func F ) ) ` x ) ) /\ A. y e. ( Base ` C ) A. z e. ( Base ` C ) A. f e. ( x ( Hom ` C ) y ) A. g e. ( y ( Hom ` C ) z ) ( ( x ( 2nd ` ( G o.func F ) ) z ) ` ( g ( <. x , y >. ( comp ` C ) z ) f ) ) = ( ( ( y ( 2nd ` ( G o.func F ) ) z ) ` g ) ( <. ( ( 1st ` ( G o.func F ) ) ` x ) , ( ( 1st ` ( G o.func F ) ) ` y ) >. ( comp ` E ) ( ( 1st ` ( G o.func F ) ) ` z ) ) ( ( x ( 2nd ` ( G o.func F ) ) y ) ` f ) ) ) )
152 funcrcl 
 |-  ( G e. ( D Func E ) -> ( D e. Cat /\ E e. Cat ) )
153 2 152 syl 
 |-  ( ph -> ( D e. Cat /\ E e. Cat ) )
154 153 simprd 
 |-  ( ph -> E e. Cat )
155 3 17 46 38 84 90 110 121 99 154 isfunc 
 |-  ( ph -> ( ( 1st ` ( G o.func F ) ) ( C Func E ) ( 2nd ` ( G o.func F ) ) <-> ( ( 1st ` ( G o.func F ) ) : ( Base ` C ) --> ( Base ` E ) /\ ( 2nd ` ( G o.func F ) ) e. X_ z e. ( ( Base ` C ) X. ( Base ` C ) ) ( ( ( ( 1st ` ( G o.func F ) ) ` ( 1st ` z ) ) ( Hom ` E ) ( ( 1st ` ( G o.func F ) ) ` ( 2nd ` z ) ) ) ^m ( ( Hom ` C ) ` z ) ) /\ A. x e. ( Base ` C ) ( ( ( x ( 2nd ` ( G o.func F ) ) x ) ` ( ( Id ` C ) ` x ) ) = ( ( Id ` E ) ` ( ( 1st ` ( G o.func F ) ) ` x ) ) /\ A. y e. ( Base ` C ) A. z e. ( Base ` C ) A. f e. ( x ( Hom ` C ) y ) A. g e. ( y ( Hom ` C ) z ) ( ( x ( 2nd ` ( G o.func F ) ) z ) ` ( g ( <. x , y >. ( comp ` C ) z ) f ) ) = ( ( ( y ( 2nd ` ( G o.func F ) ) z ) ` g ) ( <. ( ( 1st ` ( G o.func F ) ) ` x ) , ( ( 1st ` ( G o.func F ) ) ` y ) >. ( comp ` E ) ( ( 1st ` ( G o.func F ) ) ` z ) ) ( ( x ( 2nd ` ( G o.func F ) ) y ) ` f ) ) ) ) ) )
156 29 83 151 155 mpbir3and 
 |-  ( ph -> ( 1st ` ( G o.func F ) ) ( C Func E ) ( 2nd ` ( G o.func F ) ) )
157 df-br 
 |-  ( ( 1st ` ( G o.func F ) ) ( C Func E ) ( 2nd ` ( G o.func F ) ) <-> <. ( 1st ` ( G o.func F ) ) , ( 2nd ` ( G o.func F ) ) >. e. ( C Func E ) )
158 156 157 sylib 
 |-  ( ph -> <. ( 1st ` ( G o.func F ) ) , ( 2nd ` ( G o.func F ) ) >. e. ( C Func E ) )
159 15 158 eqeltrd 
 |-  ( ph -> ( G o.func F ) e. ( C Func E ) )