Metamath Proof Explorer

Theorem curfcl

Description: The curry functor of a functor F : C X. D --> E is a functor curryF ( F ) : C --> ( D --> E ) . (Contributed by Mario Carneiro, 13-Jan-2017)

Ref Expression
Hypotheses curfcl.g 
|- G = ( <. C , D >. curryF F )
curfcl.q 
|- Q = ( D FuncCat E )
curfcl.c 
|- ( ph -> C e. Cat )
curfcl.d 
|- ( ph -> D e. Cat )
curfcl.f 
|- ( ph -> F e. ( ( C Xc. D ) Func E ) )
Assertion curfcl 
|- ( ph -> G e. ( C Func Q ) )

Proof

Step Hyp Ref Expression
1 curfcl.g 
 |-  G = ( <. C , D >. curryF F )
2 curfcl.q 
 |-  Q = ( D FuncCat E )
3 curfcl.c 
 |-  ( ph -> C e. Cat )
4 curfcl.d 
 |-  ( ph -> D e. Cat )
5 curfcl.f 
 |-  ( ph -> F e. ( ( C Xc. D ) Func E ) )
6 eqid 
 |-  ( Base ` C ) = ( Base ` C )
7 eqid 
 |-  ( Base ` D ) = ( Base ` D )
8 eqid 
 |-  ( Hom ` D ) = ( Hom ` D )
9 eqid 
 |-  ( Id ` C ) = ( Id ` C )
10 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
11 eqid 
 |-  ( Id ` D ) = ( Id ` D )
12 1 6 3 4 5 7 8 9 10 11 curfval 
 |-  ( ph -> G = <. ( x e. ( Base ` C ) |-> <. ( y e. ( Base ` D ) |-> ( x ( 1st ` F ) y ) ) , ( y e. ( Base ` D ) , z e. ( Base ` D ) |-> ( g e. ( y ( Hom ` D ) z ) |-> ( ( ( Id ` C ) ` x ) ( <. x , y >. ( 2nd ` F ) <. x , z >. ) g ) ) ) >. ) , ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> ( g e. ( x ( Hom ` C ) y ) |-> ( z e. ( Base ` D ) |-> ( g ( <. x , z >. ( 2nd ` F ) <. y , z >. ) ( ( Id ` D ) ` z ) ) ) ) ) >. )
13 fvex 
 |-  ( Base ` C ) e. _V
14 13 mptex 
 |-  ( x e. ( Base ` C ) |-> <. ( y e. ( Base ` D ) |-> ( x ( 1st ` F ) y ) ) , ( y e. ( Base ` D ) , z e. ( Base ` D ) |-> ( g e. ( y ( Hom ` D ) z ) |-> ( ( ( Id ` C ) ` x ) ( <. x , y >. ( 2nd ` F ) <. x , z >. ) g ) ) ) >. ) e. _V
15 13 13 mpoex 
 |-  ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> ( g e. ( x ( Hom ` C ) y ) |-> ( z e. ( Base ` D ) |-> ( g ( <. x , z >. ( 2nd ` F ) <. y , z >. ) ( ( Id ` D ) ` z ) ) ) ) ) e. _V
16 14 15 op1std 
 |-  ( G = <. ( x e. ( Base ` C ) |-> <. ( y e. ( Base ` D ) |-> ( x ( 1st ` F ) y ) ) , ( y e. ( Base ` D ) , z e. ( Base ` D ) |-> ( g e. ( y ( Hom ` D ) z ) |-> ( ( ( Id ` C ) ` x ) ( <. x , y >. ( 2nd ` F ) <. x , z >. ) g ) ) ) >. ) , ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> ( g e. ( x ( Hom ` C ) y ) |-> ( z e. ( Base ` D ) |-> ( g ( <. x , z >. ( 2nd ` F ) <. y , z >. ) ( ( Id ` D ) ` z ) ) ) ) ) >. -> ( 1st ` G ) = ( x e. ( Base ` C ) |-> <. ( y e. ( Base ` D ) |-> ( x ( 1st ` F ) y ) ) , ( y e. ( Base ` D ) , z e. ( Base ` D ) |-> ( g e. ( y ( Hom ` D ) z ) |-> ( ( ( Id ` C ) ` x ) ( <. x , y >. ( 2nd ` F ) <. x , z >. ) g ) ) ) >. ) )
17 12 16 syl 
 |-  ( ph -> ( 1st ` G ) = ( x e. ( Base ` C ) |-> <. ( y e. ( Base ` D ) |-> ( x ( 1st ` F ) y ) ) , ( y e. ( Base ` D ) , z e. ( Base ` D ) |-> ( g e. ( y ( Hom ` D ) z ) |-> ( ( ( Id ` C ) ` x ) ( <. x , y >. ( 2nd ` F ) <. x , z >. ) g ) ) ) >. ) )
18 14 15 op2ndd 
 |-  ( G = <. ( x e. ( Base ` C ) |-> <. ( y e. ( Base ` D ) |-> ( x ( 1st ` F ) y ) ) , ( y e. ( Base ` D ) , z e. ( Base ` D ) |-> ( g e. ( y ( Hom ` D ) z ) |-> ( ( ( Id ` C ) ` x ) ( <. x , y >. ( 2nd ` F ) <. x , z >. ) g ) ) ) >. ) , ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> ( g e. ( x ( Hom ` C ) y ) |-> ( z e. ( Base ` D ) |-> ( g ( <. x , z >. ( 2nd ` F ) <. y , z >. ) ( ( Id ` D ) ` z ) ) ) ) ) >. -> ( 2nd ` G ) = ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> ( g e. ( x ( Hom ` C ) y ) |-> ( z e. ( Base ` D ) |-> ( g ( <. x , z >. ( 2nd ` F ) <. y , z >. ) ( ( Id ` D ) ` z ) ) ) ) ) )
19 12 18 syl 
 |-  ( ph -> ( 2nd ` G ) = ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> ( g e. ( x ( Hom ` C ) y ) |-> ( z e. ( Base ` D ) |-> ( g ( <. x , z >. ( 2nd ` F ) <. y , z >. ) ( ( Id ` D ) ` z ) ) ) ) ) )
20 17 19 opeq12d 
 |-  ( ph -> <. ( 1st ` G ) , ( 2nd ` G ) >. = <. ( x e. ( Base ` C ) |-> <. ( y e. ( Base ` D ) |-> ( x ( 1st ` F ) y ) ) , ( y e. ( Base ` D ) , z e. ( Base ` D ) |-> ( g e. ( y ( Hom ` D ) z ) |-> ( ( ( Id ` C ) ` x ) ( <. x , y >. ( 2nd ` F ) <. x , z >. ) g ) ) ) >. ) , ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> ( g e. ( x ( Hom ` C ) y ) |-> ( z e. ( Base ` D ) |-> ( g ( <. x , z >. ( 2nd ` F ) <. y , z >. ) ( ( Id ` D ) ` z ) ) ) ) ) >. )
21 12 20 eqtr4d 
 |-  ( ph -> G = <. ( 1st ` G ) , ( 2nd ` G ) >. )
22 2 fucbas 
 |-  ( D Func E ) = ( Base ` Q )
23 eqid 
 |-  ( D Nat E ) = ( D Nat E )
24 2 23 fuchom 
 |-  ( D Nat E ) = ( Hom ` Q )
25 eqid 
 |-  ( Id ` Q ) = ( Id ` Q )
26 eqid 
 |-  ( comp ` C ) = ( comp ` C )
27 eqid 
 |-  ( comp ` Q ) = ( comp ` Q )
28 funcrcl 
 |-  ( F e. ( ( C Xc. D ) Func E ) -> ( ( C Xc. D ) e. Cat /\ E e. Cat ) )
29 5 28 syl 
 |-  ( ph -> ( ( C Xc. D ) e. Cat /\ E e. Cat ) )
30 29 simprd 
 |-  ( ph -> E e. Cat )
31 2 4 30 fuccat 
 |-  ( ph -> Q e. Cat )
32 opex 
 |-  <. ( y e. ( Base ` D ) |-> ( x ( 1st ` F ) y ) ) , ( y e. ( Base ` D ) , z e. ( Base ` D ) |-> ( g e. ( y ( Hom ` D ) z ) |-> ( ( ( Id ` C ) ` x ) ( <. x , y >. ( 2nd ` F ) <. x , z >. ) g ) ) ) >. e. _V
33 32 a1i 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> <. ( y e. ( Base ` D ) |-> ( x ( 1st ` F ) y ) ) , ( y e. ( Base ` D ) , z e. ( Base ` D ) |-> ( g e. ( y ( Hom ` D ) z ) |-> ( ( ( Id ` C ) ` x ) ( <. x , y >. ( 2nd ` F ) <. x , z >. ) g ) ) ) >. e. _V )
34 3 adantr 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> C e. Cat )
35 4 adantr 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> D e. Cat )
36 5 adantr 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> F e. ( ( C Xc. D ) Func E ) )
37 simpr 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> x e. ( Base ` C ) )
38 eqid 
 |-  ( ( 1st ` G ) ` x ) = ( ( 1st ` G ) ` x )
39 1 6 34 35 36 7 37 38 curf1cl 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( 1st ` G ) ` x ) e. ( D Func E ) )
40 33 17 39 fmpt2d 
 |-  ( ph -> ( 1st ` G ) : ( Base ` C ) --> ( D Func E ) )
41 eqid 
 |-  ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> ( g e. ( x ( Hom ` C ) y ) |-> ( z e. ( Base ` D ) |-> ( g ( <. x , z >. ( 2nd ` F ) <. y , z >. ) ( ( Id ` D ) ` z ) ) ) ) ) = ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> ( g e. ( x ( Hom ` C ) y ) |-> ( z e. ( Base ` D ) |-> ( g ( <. x , z >. ( 2nd ` F ) <. y , z >. ) ( ( Id ` D ) ` z ) ) ) ) )
42 ovex 
 |-  ( x ( Hom ` C ) y ) e. _V
43 42 mptex 
 |-  ( g e. ( x ( Hom ` C ) y ) |-> ( z e. ( Base ` D ) |-> ( g ( <. x , z >. ( 2nd ` F ) <. y , z >. ) ( ( Id ` D ) ` z ) ) ) ) e. _V
44 41 43 fnmpoi 
 |-  ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> ( g e. ( x ( Hom ` C ) y ) |-> ( z e. ( Base ` D ) |-> ( g ( <. x , z >. ( 2nd ` F ) <. y , z >. ) ( ( Id ` D ) ` z ) ) ) ) ) Fn ( ( Base ` C ) X. ( Base ` C ) )
45 19 fneq1d 
 |-  ( ph -> ( ( 2nd ` G ) Fn ( ( Base ` C ) X. ( Base ` C ) ) <-> ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> ( g e. ( x ( Hom ` C ) y ) |-> ( z e. ( Base ` D ) |-> ( g ( <. x , z >. ( 2nd ` F ) <. y , z >. ) ( ( Id ` D ) ` z ) ) ) ) ) Fn ( ( Base ` C ) X. ( Base ` C ) ) ) )
46 44 45 mpbiri 
 |-  ( ph -> ( 2nd ` G ) Fn ( ( Base ` C ) X. ( Base ` C ) ) )
47 fvex 
 |-  ( Base ` D ) e. _V
48 47 mptex 
 |-  ( z e. ( Base ` D ) |-> ( g ( <. x , z >. ( 2nd ` F ) <. y , z >. ) ( ( Id ` D ) ` z ) ) ) e. _V
49 48 a1i 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ g e. ( x ( Hom ` C ) y ) ) -> ( z e. ( Base ` D ) |-> ( g ( <. x , z >. ( 2nd ` F ) <. y , z >. ) ( ( Id ` D ) ` z ) ) ) e. _V )
50 19 oveqd 
 |-  ( ph -> ( x ( 2nd ` G ) y ) = ( x ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> ( g e. ( x ( Hom ` C ) y ) |-> ( z e. ( Base ` D ) |-> ( g ( <. x , z >. ( 2nd ` F ) <. y , z >. ) ( ( Id ` D ) ` z ) ) ) ) ) y ) )
51 41 ovmpt4g 
 |-  ( ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ ( g e. ( x ( Hom ` C ) y ) |-> ( z e. ( Base ` D ) |-> ( g ( <. x , z >. ( 2nd ` F ) <. y , z >. ) ( ( Id ` D ) ` z ) ) ) ) e. _V ) -> ( x ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> ( g e. ( x ( Hom ` C ) y ) |-> ( z e. ( Base ` D ) |-> ( g ( <. x , z >. ( 2nd ` F ) <. y , z >. ) ( ( Id ` D ) ` z ) ) ) ) ) y ) = ( g e. ( x ( Hom ` C ) y ) |-> ( z e. ( Base ` D ) |-> ( g ( <. x , z >. ( 2nd ` F ) <. y , z >. ) ( ( Id ` D ) ` z ) ) ) ) )
52 43 51 mp3an3 
 |-  ( ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) -> ( x ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> ( g e. ( x ( Hom ` C ) y ) |-> ( z e. ( Base ` D ) |-> ( g ( <. x , z >. ( 2nd ` F ) <. y , z >. ) ( ( Id ` D ) ` z ) ) ) ) ) y ) = ( g e. ( x ( Hom ` C ) y ) |-> ( z e. ( Base ` D ) |-> ( g ( <. x , z >. ( 2nd ` F ) <. y , z >. ) ( ( Id ` D ) ` z ) ) ) ) )
53 50 52 sylan9eq 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ( x ( 2nd ` G ) y ) = ( g e. ( x ( Hom ` C ) y ) |-> ( z e. ( Base ` D ) |-> ( g ( <. x , z >. ( 2nd ` F ) <. y , z >. ) ( ( Id ` D ) ` z ) ) ) ) )
54 3 ad2antrr 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ g e. ( x ( Hom ` C ) y ) ) -> C e. Cat )
55 4 ad2antrr 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ g e. ( x ( Hom ` C ) y ) ) -> D e. Cat )
56 5 ad2antrr 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ g e. ( x ( Hom ` C ) y ) ) -> F e. ( ( C Xc. D ) Func E ) )
57 simplrl 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ g e. ( x ( Hom ` C ) y ) ) -> x e. ( Base ` C ) )
58 simplrr 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ g e. ( x ( Hom ` C ) y ) ) -> y e. ( Base ` C ) )
59 simpr 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ g e. ( x ( Hom ` C ) y ) ) -> g e. ( x ( Hom ` C ) y ) )
60 eqid 
 |-  ( ( x ( 2nd ` G ) y ) ` g ) = ( ( x ( 2nd ` G ) y ) ` g )
61 1 6 54 55 56 7 10 11 57 58 59 60 23 curf2cl 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ g e. ( x ( Hom ` C ) y ) ) -> ( ( x ( 2nd ` G ) y ) ` g ) e. ( ( ( 1st ` G ) ` x ) ( D Nat E ) ( ( 1st ` G ) ` y ) ) )
62 49 53 61 fmpt2d 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ( x ( 2nd ` G ) y ) : ( x ( Hom ` C ) y ) --> ( ( ( 1st ` G ) ` x ) ( D Nat E ) ( ( 1st ` G ) ` y ) ) )
63 eqid 
 |-  ( C Xc. D ) = ( C Xc. D )
64 63 6 7 xpcbas 
 |-  ( ( Base ` C ) X. ( Base ` D ) ) = ( Base ` ( C Xc. D ) )
65 eqid 
 |-  ( Id ` ( C Xc. D ) ) = ( Id ` ( C Xc. D ) )
66 eqid 
 |-  ( Id ` E ) = ( Id ` E )
67 relfunc 
 |-  Rel ( ( C Xc. D ) Func E )
68 1st2ndbr 
 |-  ( ( Rel ( ( C Xc. D ) Func E ) /\ F e. ( ( C Xc. D ) Func E ) ) -> ( 1st ` F ) ( ( C Xc. D ) Func E ) ( 2nd ` F ) )
69 67 5 68 sylancr 
 |-  ( ph -> ( 1st ` F ) ( ( C Xc. D ) Func E ) ( 2nd ` F ) )
70 69 ad2antrr 
 |-  ( ( ( ph /\ x e. ( Base ` C ) ) /\ y e. ( Base ` D ) ) -> ( 1st ` F ) ( ( C Xc. D ) Func E ) ( 2nd ` F ) )
71 opelxpi 
 |-  ( ( x e. ( Base ` C ) /\ y e. ( Base ` D ) ) -> <. x , y >. e. ( ( Base ` C ) X. ( Base ` D ) ) )
72 71 adantll 
 |-  ( ( ( ph /\ x e. ( Base ` C ) ) /\ y e. ( Base ` D ) ) -> <. x , y >. e. ( ( Base ` C ) X. ( Base ` D ) ) )
73 64 65 66 70 72 funcid 
 |-  ( ( ( ph /\ x e. ( Base ` C ) ) /\ y e. ( Base ` D ) ) -> ( ( <. x , y >. ( 2nd ` F ) <. x , y >. ) ` ( ( Id ` ( C Xc. D ) ) ` <. x , y >. ) ) = ( ( Id ` E ) ` ( ( 1st ` F ) ` <. x , y >. ) ) )
74 3 ad2antrr 
 |-  ( ( ( ph /\ x e. ( Base ` C ) ) /\ y e. ( Base ` D ) ) -> C e. Cat )
75 4 ad2antrr 
 |-  ( ( ( ph /\ x e. ( Base ` C ) ) /\ y e. ( Base ` D ) ) -> D e. Cat )
76 37 adantr 
 |-  ( ( ( ph /\ x e. ( Base ` C ) ) /\ y e. ( Base ` D ) ) -> x e. ( Base ` C ) )
77 simpr 
 |-  ( ( ( ph /\ x e. ( Base ` C ) ) /\ y e. ( Base ` D ) ) -> y e. ( Base ` D ) )
78 63 74 75 6 7 9 11 65 76 77 xpcid 
 |-  ( ( ( ph /\ x e. ( Base ` C ) ) /\ y e. ( Base ` D ) ) -> ( ( Id ` ( C Xc. D ) ) ` <. x , y >. ) = <. ( ( Id ` C ) ` x ) , ( ( Id ` D ) ` y ) >. )
79 78 fveq2d 
 |-  ( ( ( ph /\ x e. ( Base ` C ) ) /\ y e. ( Base ` D ) ) -> ( ( <. x , y >. ( 2nd ` F ) <. x , y >. ) ` ( ( Id ` ( C Xc. D ) ) ` <. x , y >. ) ) = ( ( <. x , y >. ( 2nd ` F ) <. x , y >. ) ` <. ( ( Id ` C ) ` x ) , ( ( Id ` D ) ` y ) >. ) )
80 df-ov 
 |-  ( ( ( Id ` C ) ` x ) ( <. x , y >. ( 2nd ` F ) <. x , y >. ) ( ( Id ` D ) ` y ) ) = ( ( <. x , y >. ( 2nd ` F ) <. x , y >. ) ` <. ( ( Id ` C ) ` x ) , ( ( Id ` D ) ` y ) >. )
81 79 80 eqtr4di 
 |-  ( ( ( ph /\ x e. ( Base ` C ) ) /\ y e. ( Base ` D ) ) -> ( ( <. x , y >. ( 2nd ` F ) <. x , y >. ) ` ( ( Id ` ( C Xc. D ) ) ` <. x , y >. ) ) = ( ( ( Id ` C ) ` x ) ( <. x , y >. ( 2nd ` F ) <. x , y >. ) ( ( Id ` D ) ` y ) ) )
82 5 ad2antrr 
 |-  ( ( ( ph /\ x e. ( Base ` C ) ) /\ y e. ( Base ` D ) ) -> F e. ( ( C Xc. D ) Func E ) )
83 1 6 74 75 82 7 76 38 77 curf11 
 |-  ( ( ( ph /\ x e. ( Base ` C ) ) /\ y e. ( Base ` D ) ) -> ( ( 1st ` ( ( 1st ` G ) ` x ) ) ` y ) = ( x ( 1st ` F ) y ) )
84 df-ov 
 |-  ( x ( 1st ` F ) y ) = ( ( 1st ` F ) ` <. x , y >. )
85 83 84 eqtr2di 
 |-  ( ( ( ph /\ x e. ( Base ` C ) ) /\ y e. ( Base ` D ) ) -> ( ( 1st ` F ) ` <. x , y >. ) = ( ( 1st ` ( ( 1st ` G ) ` x ) ) ` y ) )
86 85 fveq2d 
 |-  ( ( ( ph /\ x e. ( Base ` C ) ) /\ y e. ( Base ` D ) ) -> ( ( Id ` E ) ` ( ( 1st ` F ) ` <. x , y >. ) ) = ( ( Id ` E ) ` ( ( 1st ` ( ( 1st ` G ) ` x ) ) ` y ) ) )
87 73 81 86 3eqtr3d 
 |-  ( ( ( ph /\ x e. ( Base ` C ) ) /\ y e. ( Base ` D ) ) -> ( ( ( Id ` C ) ` x ) ( <. x , y >. ( 2nd ` F ) <. x , y >. ) ( ( Id ` D ) ` y ) ) = ( ( Id ` E ) ` ( ( 1st ` ( ( 1st ` G ) ` x ) ) ` y ) ) )
88 87 mpteq2dva 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( y e. ( Base ` D ) |-> ( ( ( Id ` C ) ` x ) ( <. x , y >. ( 2nd ` F ) <. x , y >. ) ( ( Id ` D ) ` y ) ) ) = ( y e. ( Base ` D ) |-> ( ( Id ` E ) ` ( ( 1st ` ( ( 1st ` G ) ` x ) ) ` y ) ) ) )
89 30 adantr 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> E e. Cat )
90 eqid 
 |-  ( Base ` E ) = ( Base ` E )
91 90 66 cidfn 
 |-  ( E e. Cat -> ( Id ` E ) Fn ( Base ` E ) )
92 89 91 syl 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( Id ` E ) Fn ( Base ` E ) )
93 dffn2 
 |-  ( ( Id ` E ) Fn ( Base ` E ) <-> ( Id ` E ) : ( Base ` E ) --> _V )
94 92 93 sylib 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( Id ` E ) : ( Base ` E ) --> _V )
95 relfunc 
 |-  Rel ( D Func E )
96 1st2ndbr 
 |-  ( ( Rel ( D Func E ) /\ ( ( 1st ` G ) ` x ) e. ( D Func E ) ) -> ( 1st ` ( ( 1st ` G ) ` x ) ) ( D Func E ) ( 2nd ` ( ( 1st ` G ) ` x ) ) )
97 95 39 96 sylancr 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( 1st ` ( ( 1st ` G ) ` x ) ) ( D Func E ) ( 2nd ` ( ( 1st ` G ) ` x ) ) )
98 7 90 97 funcf1 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( 1st ` ( ( 1st ` G ) ` x ) ) : ( Base ` D ) --> ( Base ` E ) )
99 fcompt 
 |-  ( ( ( Id ` E ) : ( Base ` E ) --> _V /\ ( 1st ` ( ( 1st ` G ) ` x ) ) : ( Base ` D ) --> ( Base ` E ) ) -> ( ( Id ` E ) o. ( 1st ` ( ( 1st ` G ) ` x ) ) ) = ( y e. ( Base ` D ) |-> ( ( Id ` E ) ` ( ( 1st ` ( ( 1st ` G ) ` x ) ) ` y ) ) ) )
100 94 98 99 syl2anc 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( Id ` E ) o. ( 1st ` ( ( 1st ` G ) ` x ) ) ) = ( y e. ( Base ` D ) |-> ( ( Id ` E ) ` ( ( 1st ` ( ( 1st ` G ) ` x ) ) ` y ) ) ) )
101 88 100 eqtr4d 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( y e. ( Base ` D ) |-> ( ( ( Id ` C ) ` x ) ( <. x , y >. ( 2nd ` F ) <. x , y >. ) ( ( Id ` D ) ` y ) ) ) = ( ( Id ` E ) o. ( 1st ` ( ( 1st ` G ) ` x ) ) ) )
102 6 10 9 34 37 catidcl 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( Id ` C ) ` x ) e. ( x ( Hom ` C ) x ) )
103 eqid 
 |-  ( ( x ( 2nd ` G ) x ) ` ( ( Id ` C ) ` x ) ) = ( ( x ( 2nd ` G ) x ) ` ( ( Id ` C ) ` x ) )
104 1 6 34 35 36 7 10 11 37 37 102 103 curf2 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( x ( 2nd ` G ) x ) ` ( ( Id ` C ) ` x ) ) = ( y e. ( Base ` D ) |-> ( ( ( Id ` C ) ` x ) ( <. x , y >. ( 2nd ` F ) <. x , y >. ) ( ( Id ` D ) ` y ) ) ) )
105 2 25 66 39 fucid 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( Id ` Q ) ` ( ( 1st ` G ) ` x ) ) = ( ( Id ` E ) o. ( 1st ` ( ( 1st ` G ) ` x ) ) ) )
106 101 104 105 3eqtr4d 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( x ( 2nd ` G ) x ) ` ( ( Id ` C ) ` x ) ) = ( ( Id ` Q ) ` ( ( 1st ` G ) ` x ) ) )
107 3 3ad2ant1 
 |-  ( ( 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 )
108 107 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 ) ) ) /\ w e. ( Base ` D ) ) -> C e. Cat )
109 4 3ad2ant1 
 |-  ( ( 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 ) ) ) -> D e. Cat )
110 109 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 ) ) ) /\ w e. ( Base ` D ) ) -> D e. Cat )
111 5 3ad2ant1 
 |-  ( ( 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 Xc. D ) Func E ) )
112 111 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 ) ) ) /\ w e. ( Base ` D ) ) -> F e. ( ( C Xc. D ) Func E ) )
113 simp21 
 |-  ( ( 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 ) )
114 113 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 ) ) ) /\ w e. ( Base ` D ) ) -> x e. ( Base ` C ) )
115 simpr 
 |-  ( ( ( 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 ) ) ) /\ w e. ( Base ` D ) ) -> w e. ( Base ` D ) )
116 1 6 108 110 112 7 114 38 115 curf11 
 |-  ( ( ( 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 ) ) ) /\ w e. ( Base ` D ) ) -> ( ( 1st ` ( ( 1st ` G ) ` x ) ) ` w ) = ( x ( 1st ` F ) w ) )
117 df-ov 
 |-  ( x ( 1st ` F ) w ) = ( ( 1st ` F ) ` <. x , w >. )
118 116 117 eqtrdi 
 |-  ( ( ( 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 ) ) ) /\ w e. ( Base ` D ) ) -> ( ( 1st ` ( ( 1st ` G ) ` x ) ) ` w ) = ( ( 1st ` F ) ` <. x , w >. ) )
119 simp22 
 |-  ( ( 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 ) )
120 119 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 ) ) ) /\ w e. ( Base ` D ) ) -> y e. ( Base ` C ) )
121 eqid 
 |-  ( ( 1st ` G ) ` y ) = ( ( 1st ` G ) ` y )
122 1 6 108 110 112 7 120 121 115 curf11 
 |-  ( ( ( 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 ) ) ) /\ w e. ( Base ` D ) ) -> ( ( 1st ` ( ( 1st ` G ) ` y ) ) ` w ) = ( y ( 1st ` F ) w ) )
123 df-ov 
 |-  ( y ( 1st ` F ) w ) = ( ( 1st ` F ) ` <. y , w >. )
124 122 123 eqtrdi 
 |-  ( ( ( 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 ) ) ) /\ w e. ( Base ` D ) ) -> ( ( 1st ` ( ( 1st ` G ) ` y ) ) ` w ) = ( ( 1st ` F ) ` <. y , w >. ) )
125 118 124 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 ) ) ) /\ w e. ( Base ` D ) ) -> <. ( ( 1st ` ( ( 1st ` G ) ` x ) ) ` w ) , ( ( 1st ` ( ( 1st ` G ) ` y ) ) ` w ) >. = <. ( ( 1st ` F ) ` <. x , w >. ) , ( ( 1st ` F ) ` <. y , w >. ) >. )
126 simp23 
 |-  ( ( 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 ) )
127 126 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 ) ) ) /\ w e. ( Base ` D ) ) -> z e. ( Base ` C ) )
128 eqid 
 |-  ( ( 1st ` G ) ` z ) = ( ( 1st ` G ) ` z )
129 1 6 108 110 112 7 127 128 115 curf11 
 |-  ( ( ( 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 ) ) ) /\ w e. ( Base ` D ) ) -> ( ( 1st ` ( ( 1st ` G ) ` z ) ) ` w ) = ( z ( 1st ` F ) w ) )
130 df-ov 
 |-  ( z ( 1st ` F ) w ) = ( ( 1st ` F ) ` <. z , w >. )
131 129 130 eqtrdi 
 |-  ( ( ( 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 ) ) ) /\ w e. ( Base ` D ) ) -> ( ( 1st ` ( ( 1st ` G ) ` z ) ) ` w ) = ( ( 1st ` F ) ` <. z , w >. ) )
132 125 131 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 ) ) ) /\ w e. ( Base ` D ) ) -> ( <. ( ( 1st ` ( ( 1st ` G ) ` x ) ) ` w ) , ( ( 1st ` ( ( 1st ` G ) ` y ) ) ` w ) >. ( comp ` E ) ( ( 1st ` ( ( 1st ` G ) ` z ) ) ` w ) ) = ( <. ( ( 1st ` F ) ` <. x , w >. ) , ( ( 1st ` F ) ` <. y , w >. ) >. ( comp ` E ) ( ( 1st ` F ) ` <. z , w >. ) ) )
133 simp3r 
 |-  ( ( 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 ) )
134 133 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 ) ) ) /\ w e. ( Base ` D ) ) -> g e. ( y ( Hom ` C ) z ) )
135 eqid 
 |-  ( ( y ( 2nd ` G ) z ) ` g ) = ( ( y ( 2nd ` G ) z ) ` g )
136 1 6 108 110 112 7 10 11 120 127 134 135 115 curf2val 
 |-  ( ( ( 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 ) ) ) /\ w e. ( Base ` D ) ) -> ( ( ( y ( 2nd ` G ) z ) ` g ) ` w ) = ( g ( <. y , w >. ( 2nd ` F ) <. z , w >. ) ( ( Id ` D ) ` w ) ) )
137 df-ov 
 |-  ( g ( <. y , w >. ( 2nd ` F ) <. z , w >. ) ( ( Id ` D ) ` w ) ) = ( ( <. y , w >. ( 2nd ` F ) <. z , w >. ) ` <. g , ( ( Id ` D ) ` w ) >. )
138 136 137 eqtrdi 
 |-  ( ( ( 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 ) ) ) /\ w e. ( Base ` D ) ) -> ( ( ( y ( 2nd ` G ) z ) ` g ) ` w ) = ( ( <. y , w >. ( 2nd ` F ) <. z , w >. ) ` <. g , ( ( Id ` D ) ` w ) >. ) )
139 simp3l 
 |-  ( ( 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 ) )
140 139 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 ) ) ) /\ w e. ( Base ` D ) ) -> f e. ( x ( Hom ` C ) y ) )
141 eqid 
 |-  ( ( x ( 2nd ` G ) y ) ` f ) = ( ( x ( 2nd ` G ) y ) ` f )
142 1 6 108 110 112 7 10 11 114 120 140 141 115 curf2val 
 |-  ( ( ( 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 ) ) ) /\ w e. ( Base ` D ) ) -> ( ( ( x ( 2nd ` G ) y ) ` f ) ` w ) = ( f ( <. x , w >. ( 2nd ` F ) <. y , w >. ) ( ( Id ` D ) ` w ) ) )
143 df-ov 
 |-  ( f ( <. x , w >. ( 2nd ` F ) <. y , w >. ) ( ( Id ` D ) ` w ) ) = ( ( <. x , w >. ( 2nd ` F ) <. y , w >. ) ` <. f , ( ( Id ` D ) ` w ) >. )
144 142 143 eqtrdi 
 |-  ( ( ( 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 ) ) ) /\ w e. ( Base ` D ) ) -> ( ( ( x ( 2nd ` G ) y ) ` f ) ` w ) = ( ( <. x , w >. ( 2nd ` F ) <. y , w >. ) ` <. f , ( ( Id ` D ) ` w ) >. ) )
145 132 138 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 ) ) ) /\ w e. ( Base ` D ) ) -> ( ( ( ( y ( 2nd ` G ) z ) ` g ) ` w ) ( <. ( ( 1st ` ( ( 1st ` G ) ` x ) ) ` w ) , ( ( 1st ` ( ( 1st ` G ) ` y ) ) ` w ) >. ( comp ` E ) ( ( 1st ` ( ( 1st ` G ) ` z ) ) ` w ) ) ( ( ( x ( 2nd ` G ) y ) ` f ) ` w ) ) = ( ( ( <. y , w >. ( 2nd ` F ) <. z , w >. ) ` <. g , ( ( Id ` D ) ` w ) >. ) ( <. ( ( 1st ` F ) ` <. x , w >. ) , ( ( 1st ` F ) ` <. y , w >. ) >. ( comp ` E ) ( ( 1st ` F ) ` <. z , w >. ) ) ( ( <. x , w >. ( 2nd ` F ) <. y , w >. ) ` <. f , ( ( Id ` D ) ` w ) >. ) ) )
146 eqid 
 |-  ( Hom ` ( C Xc. D ) ) = ( Hom ` ( C Xc. D ) )
147 eqid 
 |-  ( comp ` ( C Xc. D ) ) = ( comp ` ( C Xc. D ) )
148 eqid 
 |-  ( comp ` E ) = ( comp ` E )
149 67 112 68 sylancr 
 |-  ( ( ( 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 ) ) ) /\ w e. ( Base ` D ) ) -> ( 1st ` F ) ( ( C Xc. D ) Func E ) ( 2nd ` F ) )
150 opelxpi 
 |-  ( ( x e. ( Base ` C ) /\ w e. ( Base ` D ) ) -> <. x , w >. e. ( ( Base ` C ) X. ( Base ` D ) ) )
151 113 150 sylan 
 |-  ( ( ( 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 ) ) ) /\ w e. ( Base ` D ) ) -> <. x , w >. e. ( ( Base ` C ) X. ( Base ` D ) ) )
152 opelxpi 
 |-  ( ( y e. ( Base ` C ) /\ w e. ( Base ` D ) ) -> <. y , w >. e. ( ( Base ` C ) X. ( Base ` D ) ) )
153 119 152 sylan 
 |-  ( ( ( 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 ) ) ) /\ w e. ( Base ` D ) ) -> <. y , w >. e. ( ( Base ` C ) X. ( Base ` D ) ) )
154 opelxpi 
 |-  ( ( z e. ( Base ` C ) /\ w e. ( Base ` D ) ) -> <. z , w >. e. ( ( Base ` C ) X. ( Base ` D ) ) )
155 126 154 sylan 
 |-  ( ( ( 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 ) ) ) /\ w e. ( Base ` D ) ) -> <. z , w >. e. ( ( Base ` C ) X. ( Base ` D ) ) )
156 7 8 11 110 115 catidcl 
 |-  ( ( ( 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 ) ) ) /\ w e. ( Base ` D ) ) -> ( ( Id ` D ) ` w ) e. ( w ( Hom ` D ) w ) )
157 140 156 opelxpd 
 |-  ( ( ( 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 ) ) ) /\ w e. ( Base ` D ) ) -> <. f , ( ( Id ` D ) ` w ) >. e. ( ( x ( Hom ` C ) y ) X. ( w ( Hom ` D ) w ) ) )
158 63 6 7 10 8 114 115 120 115 146 xpchom2 
 |-  ( ( ( 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 ) ) ) /\ w e. ( Base ` D ) ) -> ( <. x , w >. ( Hom ` ( C Xc. D ) ) <. y , w >. ) = ( ( x ( Hom ` C ) y ) X. ( w ( Hom ` D ) w ) ) )
159 157 158 eleqtrrd 
 |-  ( ( ( 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 ) ) ) /\ w e. ( Base ` D ) ) -> <. f , ( ( Id ` D ) ` w ) >. e. ( <. x , w >. ( Hom ` ( C Xc. D ) ) <. y , w >. ) )
160 134 156 opelxpd 
 |-  ( ( ( 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 ) ) ) /\ w e. ( Base ` D ) ) -> <. g , ( ( Id ` D ) ` w ) >. e. ( ( y ( Hom ` C ) z ) X. ( w ( Hom ` D ) w ) ) )
161 63 6 7 10 8 120 115 127 115 146 xpchom2 
 |-  ( ( ( 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 ) ) ) /\ w e. ( Base ` D ) ) -> ( <. y , w >. ( Hom ` ( C Xc. D ) ) <. z , w >. ) = ( ( y ( Hom ` C ) z ) X. ( w ( Hom ` D ) w ) ) )
162 160 161 eleqtrrd 
 |-  ( ( ( 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 ) ) ) /\ w e. ( Base ` D ) ) -> <. g , ( ( Id ` D ) ` w ) >. e. ( <. y , w >. ( Hom ` ( C Xc. D ) ) <. z , w >. ) )
163 64 146 147 148 149 151 153 155 159 162 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 ) ) ) /\ w e. ( Base ` D ) ) -> ( ( <. x , w >. ( 2nd ` F ) <. z , w >. ) ` ( <. g , ( ( Id ` D ) ` w ) >. ( <. <. x , w >. , <. y , w >. >. ( comp ` ( C Xc. D ) ) <. z , w >. ) <. f , ( ( Id ` D ) ` w ) >. ) ) = ( ( ( <. y , w >. ( 2nd ` F ) <. z , w >. ) ` <. g , ( ( Id ` D ) ` w ) >. ) ( <. ( ( 1st ` F ) ` <. x , w >. ) , ( ( 1st ` F ) ` <. y , w >. ) >. ( comp ` E ) ( ( 1st ` F ) ` <. z , w >. ) ) ( ( <. x , w >. ( 2nd ` F ) <. y , w >. ) ` <. f , ( ( Id ` D ) ` w ) >. ) ) )
164 eqid 
 |-  ( comp ` D ) = ( comp ` D )
165 63 6 7 10 8 114 115 120 115 26 164 147 127 115 140 156 134 156 xpcco2 
 |-  ( ( ( 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 ) ) ) /\ w e. ( Base ` D ) ) -> ( <. g , ( ( Id ` D ) ` w ) >. ( <. <. x , w >. , <. y , w >. >. ( comp ` ( C Xc. D ) ) <. z , w >. ) <. f , ( ( Id ` D ) ` w ) >. ) = <. ( g ( <. x , y >. ( comp ` C ) z ) f ) , ( ( ( Id ` D ) ` w ) ( <. w , w >. ( comp ` D ) w ) ( ( Id ` D ) ` w ) ) >. )
166 7 8 11 110 115 164 115 156 catlid 
 |-  ( ( ( 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 ) ) ) /\ w e. ( Base ` D ) ) -> ( ( ( Id ` D ) ` w ) ( <. w , w >. ( comp ` D ) w ) ( ( Id ` D ) ` w ) ) = ( ( Id ` D ) ` w ) )
167 166 opeq2d 
 |-  ( ( ( 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 ) ) ) /\ w e. ( Base ` D ) ) -> <. ( g ( <. x , y >. ( comp ` C ) z ) f ) , ( ( ( Id ` D ) ` w ) ( <. w , w >. ( comp ` D ) w ) ( ( Id ` D ) ` w ) ) >. = <. ( g ( <. x , y >. ( comp ` C ) z ) f ) , ( ( Id ` D ) ` w ) >. )
168 165 167 eqtrd 
 |-  ( ( ( 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 ) ) ) /\ w e. ( Base ` D ) ) -> ( <. g , ( ( Id ` D ) ` w ) >. ( <. <. x , w >. , <. y , w >. >. ( comp ` ( C Xc. D ) ) <. z , w >. ) <. f , ( ( Id ` D ) ` w ) >. ) = <. ( g ( <. x , y >. ( comp ` C ) z ) f ) , ( ( Id ` D ) ` w ) >. )
169 168 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 ) ) ) /\ w e. ( Base ` D ) ) -> ( ( <. x , w >. ( 2nd ` F ) <. z , w >. ) ` ( <. g , ( ( Id ` D ) ` w ) >. ( <. <. x , w >. , <. y , w >. >. ( comp ` ( C Xc. D ) ) <. z , w >. ) <. f , ( ( Id ` D ) ` w ) >. ) ) = ( ( <. x , w >. ( 2nd ` F ) <. z , w >. ) ` <. ( g ( <. x , y >. ( comp ` C ) z ) f ) , ( ( Id ` D ) ` w ) >. ) )
170 df-ov 
 |-  ( ( g ( <. x , y >. ( comp ` C ) z ) f ) ( <. x , w >. ( 2nd ` F ) <. z , w >. ) ( ( Id ` D ) ` w ) ) = ( ( <. x , w >. ( 2nd ` F ) <. z , w >. ) ` <. ( g ( <. x , y >. ( comp ` C ) z ) f ) , ( ( Id ` D ) ` w ) >. )
171 169 170 eqtr4di 
 |-  ( ( ( 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 ) ) ) /\ w e. ( Base ` D ) ) -> ( ( <. x , w >. ( 2nd ` F ) <. z , w >. ) ` ( <. g , ( ( Id ` D ) ` w ) >. ( <. <. x , w >. , <. y , w >. >. ( comp ` ( C Xc. D ) ) <. z , w >. ) <. f , ( ( Id ` D ) ` w ) >. ) ) = ( ( g ( <. x , y >. ( comp ` C ) z ) f ) ( <. x , w >. ( 2nd ` F ) <. z , w >. ) ( ( Id ` D ) ` w ) ) )
172 145 163 171 3eqtr2rd 
 |-  ( ( ( 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 ) ) ) /\ w e. ( Base ` D ) ) -> ( ( g ( <. x , y >. ( comp ` C ) z ) f ) ( <. x , w >. ( 2nd ` F ) <. z , w >. ) ( ( Id ` D ) ` w ) ) = ( ( ( ( y ( 2nd ` G ) z ) ` g ) ` w ) ( <. ( ( 1st ` ( ( 1st ` G ) ` x ) ) ` w ) , ( ( 1st ` ( ( 1st ` G ) ` y ) ) ` w ) >. ( comp ` E ) ( ( 1st ` ( ( 1st ` G ) ` z ) ) ` w ) ) ( ( ( x ( 2nd ` G ) y ) ` f ) ` w ) ) )
173 172 mpteq2dva 
 |-  ( ( 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 ) ) ) -> ( w e. ( Base ` D ) |-> ( ( g ( <. x , y >. ( comp ` C ) z ) f ) ( <. x , w >. ( 2nd ` F ) <. z , w >. ) ( ( Id ` D ) ` w ) ) ) = ( w e. ( Base ` D ) |-> ( ( ( ( y ( 2nd ` G ) z ) ` g ) ` w ) ( <. ( ( 1st ` ( ( 1st ` G ) ` x ) ) ` w ) , ( ( 1st ` ( ( 1st ` G ) ` y ) ) ` w ) >. ( comp ` E ) ( ( 1st ` ( ( 1st ` G ) ` z ) ) ` w ) ) ( ( ( x ( 2nd ` G ) y ) ` f ) ` w ) ) ) )
174 6 10 26 107 113 119 126 139 133 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 ) )
175 eqid 
 |-  ( ( x ( 2nd ` G ) z ) ` ( g ( <. x , y >. ( comp ` C ) z ) f ) ) = ( ( x ( 2nd ` G ) z ) ` ( g ( <. x , y >. ( comp ` C ) z ) f ) )
176 1 6 107 109 111 7 10 11 113 126 174 175 curf2 
 |-  ( ( 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 ) z ) ` ( g ( <. x , y >. ( comp ` C ) z ) f ) ) = ( w e. ( Base ` D ) |-> ( ( g ( <. x , y >. ( comp ` C ) z ) f ) ( <. x , w >. ( 2nd ` F ) <. z , w >. ) ( ( Id ` D ) ` w ) ) ) )
177 1 6 107 109 111 7 10 11 113 119 139 141 23 curf2cl 
 |-  ( ( 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 ) y ) ` f ) e. ( ( ( 1st ` G ) ` x ) ( D Nat E ) ( ( 1st ` G ) ` y ) ) )
178 1 6 107 109 111 7 10 11 119 126 133 135 23 curf2cl 
 |-  ( ( 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 ) z ) ` g ) e. ( ( ( 1st ` G ) ` y ) ( D Nat E ) ( ( 1st ` G ) ` z ) ) )
179 2 23 7 148 27 177 178 fucco 
 |-  ( ( 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 ) z ) ` g ) ( <. ( ( 1st ` G ) ` x ) , ( ( 1st ` G ) ` y ) >. ( comp ` Q ) ( ( 1st ` G ) ` z ) ) ( ( x ( 2nd ` G ) y ) ` f ) ) = ( w e. ( Base ` D ) |-> ( ( ( ( y ( 2nd ` G ) z ) ` g ) ` w ) ( <. ( ( 1st ` ( ( 1st ` G ) ` x ) ) ` w ) , ( ( 1st ` ( ( 1st ` G ) ` y ) ) ` w ) >. ( comp ` E ) ( ( 1st ` ( ( 1st ` G ) ` z ) ) ` w ) ) ( ( ( x ( 2nd ` G ) y ) ` f ) ` w ) ) ) )
180 173 176 179 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 ) z ) ` ( g ( <. x , y >. ( comp ` C ) z ) f ) ) = ( ( ( y ( 2nd ` G ) z ) ` g ) ( <. ( ( 1st ` G ) ` x ) , ( ( 1st ` G ) ` y ) >. ( comp ` Q ) ( ( 1st ` G ) ` z ) ) ( ( x ( 2nd ` G ) y ) ` f ) ) )
181 6 22 10 24 9 25 26 27 3 31 40 46 62 106 180 isfuncd 
 |-  ( ph -> ( 1st ` G ) ( C Func Q ) ( 2nd ` G ) )
182 df-br 
 |-  ( ( 1st ` G ) ( C Func Q ) ( 2nd ` G ) <-> <. ( 1st ` G ) , ( 2nd ` G ) >. e. ( C Func Q ) )
183 181 182 sylib 
 |-  ( ph -> <. ( 1st ` G ) , ( 2nd ` G ) >. e. ( C Func Q ) )
184 21 183 eqeltrd 
 |-  ( ph -> G e. ( C Func Q ) )