Metamath Proof Explorer

Theorem curfuncf

Description: Cancellation of curry with uncurry. (Contributed by Mario Carneiro, 13-Jan-2017)

Ref Expression
Hypotheses uncfval.g 
|- F = ( <" C D E "> uncurryF G )
uncfval.c 
|- ( ph -> D e. Cat )
uncfval.d 
|- ( ph -> E e. Cat )
uncfval.f 
|- ( ph -> G e. ( C Func ( D FuncCat E ) ) )
Assertion curfuncf 
|- ( ph -> ( <. C , D >. curryF F ) = G )

Proof

Step Hyp Ref Expression
1 uncfval.g 
 |-  F = ( <" C D E "> uncurryF G )
2 uncfval.c 
 |-  ( ph -> D e. Cat )
3 uncfval.d 
 |-  ( ph -> E e. Cat )
4 uncfval.f 
 |-  ( ph -> G e. ( C Func ( D FuncCat E ) ) )
5 2 ad2antrr 
 |-  ( ( ( ph /\ x e. ( Base ` C ) ) /\ y e. ( Base ` D ) ) -> D e. Cat )
6 3 ad2antrr 
 |-  ( ( ( ph /\ x e. ( Base ` C ) ) /\ y e. ( Base ` D ) ) -> E e. Cat )
7 4 ad2antrr 
 |-  ( ( ( ph /\ x e. ( Base ` C ) ) /\ y e. ( Base ` D ) ) -> G e. ( C Func ( D FuncCat E ) ) )
8 eqid 
 |-  ( Base ` C ) = ( Base ` C )
9 eqid 
 |-  ( Base ` D ) = ( Base ` D )
10 simplr 
 |-  ( ( ( ph /\ x e. ( Base ` C ) ) /\ y e. ( Base ` D ) ) -> x e. ( Base ` C ) )
11 simpr 
 |-  ( ( ( ph /\ x e. ( Base ` C ) ) /\ y e. ( Base ` D ) ) -> y e. ( Base ` D ) )
12 1 5 6 7 8 9 10 11 uncf1 
 |-  ( ( ( ph /\ x e. ( Base ` C ) ) /\ y e. ( Base ` D ) ) -> ( x ( 1st ` F ) y ) = ( ( 1st ` ( ( 1st ` G ) ` x ) ) ` y ) )
13 12 mpteq2dva 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( y e. ( Base ` D ) |-> ( x ( 1st ` F ) y ) ) = ( y e. ( Base ` D ) |-> ( ( 1st ` ( ( 1st ` G ) ` x ) ) ` y ) ) )
14 eqid 
 |-  ( Base ` E ) = ( Base ` E )
15 relfunc 
 |-  Rel ( D Func E )
16 eqid 
 |-  ( D FuncCat E ) = ( D FuncCat E )
17 16 fucbas 
 |-  ( D Func E ) = ( Base ` ( D FuncCat E ) )
18 relfunc 
 |-  Rel ( C Func ( D FuncCat E ) )
19 1st2ndbr 
 |-  ( ( Rel ( C Func ( D FuncCat E ) ) /\ G e. ( C Func ( D FuncCat E ) ) ) -> ( 1st ` G ) ( C Func ( D FuncCat E ) ) ( 2nd ` G ) )
20 18 4 19 sylancr 
 |-  ( ph -> ( 1st ` G ) ( C Func ( D FuncCat E ) ) ( 2nd ` G ) )
21 8 17 20 funcf1 
 |-  ( ph -> ( 1st ` G ) : ( Base ` C ) --> ( D Func E ) )
22 21 ffvelrnda 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( 1st ` G ) ` x ) e. ( D Func E ) )
23 1st2ndbr 
 |-  ( ( Rel ( D Func E ) /\ ( ( 1st ` G ) ` x ) e. ( D Func E ) ) -> ( 1st ` ( ( 1st ` G ) ` x ) ) ( D Func E ) ( 2nd ` ( ( 1st ` G ) ` x ) ) )
24 15 22 23 sylancr 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( 1st ` ( ( 1st ` G ) ` x ) ) ( D Func E ) ( 2nd ` ( ( 1st ` G ) ` x ) ) )
25 9 14 24 funcf1 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( 1st ` ( ( 1st ` G ) ` x ) ) : ( Base ` D ) --> ( Base ` E ) )
26 25 feqmptd 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( 1st ` ( ( 1st ` G ) ` x ) ) = ( y e. ( Base ` D ) |-> ( ( 1st ` ( ( 1st ` G ) ` x ) ) ` y ) ) )
27 13 26 eqtr4d 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( y e. ( Base ` D ) |-> ( x ( 1st ` F ) y ) ) = ( 1st ` ( ( 1st ` G ) ` x ) ) )
28 2 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. ( Base ` C ) ) /\ ( y e. ( Base ` D ) /\ z e. ( Base ` D ) ) ) /\ g e. ( y ( Hom ` D ) z ) ) -> D e. Cat )
29 3 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. ( Base ` C ) ) /\ ( y e. ( Base ` D ) /\ z e. ( Base ` D ) ) ) /\ g e. ( y ( Hom ` D ) z ) ) -> E e. Cat )
30 4 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. ( Base ` C ) ) /\ ( y e. ( Base ` D ) /\ z e. ( Base ` D ) ) ) /\ g e. ( y ( Hom ` D ) z ) ) -> G e. ( C Func ( D FuncCat E ) ) )
31 simpllr 
 |-  ( ( ( ( ph /\ x e. ( Base ` C ) ) /\ ( y e. ( Base ` D ) /\ z e. ( Base ` D ) ) ) /\ g e. ( y ( Hom ` D ) z ) ) -> x e. ( Base ` C ) )
32 simplrl 
 |-  ( ( ( ( ph /\ x e. ( Base ` C ) ) /\ ( y e. ( Base ` D ) /\ z e. ( Base ` D ) ) ) /\ g e. ( y ( Hom ` D ) z ) ) -> y e. ( Base ` D ) )
33 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
34 eqid 
 |-  ( Hom ` D ) = ( Hom ` D )
35 simprr 
 |-  ( ( ( ph /\ x e. ( Base ` C ) ) /\ ( y e. ( Base ` D ) /\ z e. ( Base ` D ) ) ) -> z e. ( Base ` D ) )
36 35 adantr 
 |-  ( ( ( ( ph /\ x e. ( Base ` C ) ) /\ ( y e. ( Base ` D ) /\ z e. ( Base ` D ) ) ) /\ g e. ( y ( Hom ` D ) z ) ) -> z e. ( Base ` D ) )
37 eqid 
 |-  ( Id ` C ) = ( Id ` C )
38 funcrcl 
 |-  ( G e. ( C Func ( D FuncCat E ) ) -> ( C e. Cat /\ ( D FuncCat E ) e. Cat ) )
39 4 38 syl 
 |-  ( ph -> ( C e. Cat /\ ( D FuncCat E ) e. Cat ) )
40 39 simpld 
 |-  ( ph -> C e. Cat )
41 40 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. ( Base ` C ) ) /\ ( y e. ( Base ` D ) /\ z e. ( Base ` D ) ) ) /\ g e. ( y ( Hom ` D ) z ) ) -> C e. Cat )
42 8 33 37 41 31 catidcl 
 |-  ( ( ( ( ph /\ x e. ( Base ` C ) ) /\ ( y e. ( Base ` D ) /\ z e. ( Base ` D ) ) ) /\ g e. ( y ( Hom ` D ) z ) ) -> ( ( Id ` C ) ` x ) e. ( x ( Hom ` C ) x ) )
43 simpr 
 |-  ( ( ( ( ph /\ x e. ( Base ` C ) ) /\ ( y e. ( Base ` D ) /\ z e. ( Base ` D ) ) ) /\ g e. ( y ( Hom ` D ) z ) ) -> g e. ( y ( Hom ` D ) z ) )
44 1 28 29 30 8 9 31 32 33 34 31 36 42 43 uncf2 
 |-  ( ( ( ( ph /\ x e. ( Base ` C ) ) /\ ( 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 ( 2nd ` G ) x ) ` ( ( Id ` C ) ` x ) ) ` z ) ( <. ( ( 1st ` ( ( 1st ` G ) ` x ) ) ` y ) , ( ( 1st ` ( ( 1st ` G ) ` x ) ) ` z ) >. ( comp ` E ) ( ( 1st ` ( ( 1st ` G ) ` x ) ) ` z ) ) ( ( y ( 2nd ` ( ( 1st ` G ) ` x ) ) z ) ` g ) ) )
45 eqid 
 |-  ( Id ` ( D FuncCat E ) ) = ( Id ` ( D FuncCat E ) )
46 20 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. ( Base ` C ) ) /\ ( y e. ( Base ` D ) /\ z e. ( Base ` D ) ) ) /\ g e. ( y ( Hom ` D ) z ) ) -> ( 1st ` G ) ( C Func ( D FuncCat E ) ) ( 2nd ` G ) )
47 8 37 45 46 31 funcid 
 |-  ( ( ( ( ph /\ x e. ( Base ` C ) ) /\ ( y e. ( Base ` D ) /\ z e. ( Base ` D ) ) ) /\ g e. ( y ( Hom ` D ) z ) ) -> ( ( x ( 2nd ` G ) x ) ` ( ( Id ` C ) ` x ) ) = ( ( Id ` ( D FuncCat E ) ) ` ( ( 1st ` G ) ` x ) ) )
48 eqid 
 |-  ( Id ` E ) = ( Id ` E )
49 22 ad2antrr 
 |-  ( ( ( ( ph /\ x e. ( Base ` C ) ) /\ ( y e. ( Base ` D ) /\ z e. ( Base ` D ) ) ) /\ g e. ( y ( Hom ` D ) z ) ) -> ( ( 1st ` G ) ` x ) e. ( D Func E ) )
50 16 45 48 49 fucid 
 |-  ( ( ( ( ph /\ x e. ( Base ` C ) ) /\ ( y e. ( Base ` D ) /\ z e. ( Base ` D ) ) ) /\ g e. ( y ( Hom ` D ) z ) ) -> ( ( Id ` ( D FuncCat E ) ) ` ( ( 1st ` G ) ` x ) ) = ( ( Id ` E ) o. ( 1st ` ( ( 1st ` G ) ` x ) ) ) )
51 47 50 eqtrd 
 |-  ( ( ( ( ph /\ x e. ( Base ` C ) ) /\ ( y e. ( Base ` D ) /\ z e. ( Base ` D ) ) ) /\ g e. ( y ( Hom ` D ) z ) ) -> ( ( x ( 2nd ` G ) x ) ` ( ( Id ` C ) ` x ) ) = ( ( Id ` E ) o. ( 1st ` ( ( 1st ` G ) ` x ) ) ) )
52 51 fveq1d 
 |-  ( ( ( ( ph /\ x e. ( Base ` C ) ) /\ ( y e. ( Base ` D ) /\ z e. ( Base ` D ) ) ) /\ g e. ( y ( Hom ` D ) z ) ) -> ( ( ( x ( 2nd ` G ) x ) ` ( ( Id ` C ) ` x ) ) ` z ) = ( ( ( Id ` E ) o. ( 1st ` ( ( 1st ` G ) ` x ) ) ) ` z ) )
53 25 ad2antrr 
 |-  ( ( ( ( ph /\ x e. ( Base ` C ) ) /\ ( y e. ( Base ` D ) /\ z e. ( Base ` D ) ) ) /\ g e. ( y ( Hom ` D ) z ) ) -> ( 1st ` ( ( 1st ` G ) ` x ) ) : ( Base ` D ) --> ( Base ` E ) )
54 fvco3 
 |-  ( ( ( 1st ` ( ( 1st ` G ) ` x ) ) : ( Base ` D ) --> ( Base ` E ) /\ z e. ( Base ` D ) ) -> ( ( ( Id ` E ) o. ( 1st ` ( ( 1st ` G ) ` x ) ) ) ` z ) = ( ( Id ` E ) ` ( ( 1st ` ( ( 1st ` G ) ` x ) ) ` z ) ) )
55 53 36 54 syl2anc 
 |-  ( ( ( ( ph /\ x e. ( Base ` C ) ) /\ ( y e. ( Base ` D ) /\ z e. ( Base ` D ) ) ) /\ g e. ( y ( Hom ` D ) z ) ) -> ( ( ( Id ` E ) o. ( 1st ` ( ( 1st ` G ) ` x ) ) ) ` z ) = ( ( Id ` E ) ` ( ( 1st ` ( ( 1st ` G ) ` x ) ) ` z ) ) )
56 52 55 eqtrd 
 |-  ( ( ( ( ph /\ x e. ( Base ` C ) ) /\ ( y e. ( Base ` D ) /\ z e. ( Base ` D ) ) ) /\ g e. ( y ( Hom ` D ) z ) ) -> ( ( ( x ( 2nd ` G ) x ) ` ( ( Id ` C ) ` x ) ) ` z ) = ( ( Id ` E ) ` ( ( 1st ` ( ( 1st ` G ) ` x ) ) ` z ) ) )
57 56 oveq1d 
 |-  ( ( ( ( ph /\ x e. ( Base ` C ) ) /\ ( y e. ( Base ` D ) /\ z e. ( Base ` D ) ) ) /\ g e. ( y ( Hom ` D ) z ) ) -> ( ( ( ( x ( 2nd ` G ) x ) ` ( ( Id ` C ) ` x ) ) ` z ) ( <. ( ( 1st ` ( ( 1st ` G ) ` x ) ) ` y ) , ( ( 1st ` ( ( 1st ` G ) ` x ) ) ` z ) >. ( comp ` E ) ( ( 1st ` ( ( 1st ` G ) ` x ) ) ` z ) ) ( ( y ( 2nd ` ( ( 1st ` G ) ` x ) ) z ) ` g ) ) = ( ( ( Id ` E ) ` ( ( 1st ` ( ( 1st ` G ) ` x ) ) ` z ) ) ( <. ( ( 1st ` ( ( 1st ` G ) ` x ) ) ` y ) , ( ( 1st ` ( ( 1st ` G ) ` x ) ) ` z ) >. ( comp ` E ) ( ( 1st ` ( ( 1st ` G ) ` x ) ) ` z ) ) ( ( y ( 2nd ` ( ( 1st ` G ) ` x ) ) z ) ` g ) ) )
58 eqid 
 |-  ( Hom ` E ) = ( Hom ` E )
59 53 32 ffvelrnd 
 |-  ( ( ( ( ph /\ x e. ( Base ` C ) ) /\ ( y e. ( Base ` D ) /\ z e. ( Base ` D ) ) ) /\ g e. ( y ( Hom ` D ) z ) ) -> ( ( 1st ` ( ( 1st ` G ) ` x ) ) ` y ) e. ( Base ` E ) )
60 eqid 
 |-  ( comp ` E ) = ( comp ` E )
61 53 36 ffvelrnd 
 |-  ( ( ( ( ph /\ x e. ( Base ` C ) ) /\ ( y e. ( Base ` D ) /\ z e. ( Base ` D ) ) ) /\ g e. ( y ( Hom ` D ) z ) ) -> ( ( 1st ` ( ( 1st ` G ) ` x ) ) ` z ) e. ( Base ` E ) )
62 24 adantr 
 |-  ( ( ( ph /\ x e. ( Base ` C ) ) /\ ( y e. ( Base ` D ) /\ z e. ( Base ` D ) ) ) -> ( 1st ` ( ( 1st ` G ) ` x ) ) ( D Func E ) ( 2nd ` ( ( 1st ` G ) ` x ) ) )
63 simprl 
 |-  ( ( ( ph /\ x e. ( Base ` C ) ) /\ ( y e. ( Base ` D ) /\ z e. ( Base ` D ) ) ) -> y e. ( Base ` D ) )
64 9 34 58 62 63 35 funcf2 
 |-  ( ( ( ph /\ x e. ( Base ` C ) ) /\ ( y e. ( Base ` D ) /\ z e. ( Base ` D ) ) ) -> ( y ( 2nd ` ( ( 1st ` G ) ` x ) ) z ) : ( y ( Hom ` D ) z ) --> ( ( ( 1st ` ( ( 1st ` G ) ` x ) ) ` y ) ( Hom ` E ) ( ( 1st ` ( ( 1st ` G ) ` x ) ) ` z ) ) )
65 64 ffvelrnda 
 |-  ( ( ( ( ph /\ x e. ( Base ` C ) ) /\ ( y e. ( Base ` D ) /\ z e. ( Base ` D ) ) ) /\ g e. ( y ( Hom ` D ) z ) ) -> ( ( y ( 2nd ` ( ( 1st ` G ) ` x ) ) z ) ` g ) e. ( ( ( 1st ` ( ( 1st ` G ) ` x ) ) ` y ) ( Hom ` E ) ( ( 1st ` ( ( 1st ` G ) ` x ) ) ` z ) ) )
66 14 58 48 29 59 60 61 65 catlid 
 |-  ( ( ( ( ph /\ x e. ( Base ` C ) ) /\ ( y e. ( Base ` D ) /\ z e. ( Base ` D ) ) ) /\ g e. ( y ( Hom ` D ) z ) ) -> ( ( ( Id ` E ) ` ( ( 1st ` ( ( 1st ` G ) ` x ) ) ` z ) ) ( <. ( ( 1st ` ( ( 1st ` G ) ` x ) ) ` y ) , ( ( 1st ` ( ( 1st ` G ) ` x ) ) ` z ) >. ( comp ` E ) ( ( 1st ` ( ( 1st ` G ) ` x ) ) ` z ) ) ( ( y ( 2nd ` ( ( 1st ` G ) ` x ) ) z ) ` g ) ) = ( ( y ( 2nd ` ( ( 1st ` G ) ` x ) ) z ) ` g ) )
67 44 57 66 3eqtrd 
 |-  ( ( ( ( ph /\ x e. ( Base ` C ) ) /\ ( y e. ( Base ` D ) /\ z e. ( Base ` D ) ) ) /\ g e. ( y ( Hom ` D ) z ) ) -> ( ( ( Id ` C ) ` x ) ( <. x , y >. ( 2nd ` F ) <. x , z >. ) g ) = ( ( y ( 2nd ` ( ( 1st ` G ) ` x ) ) z ) ` g ) )
68 67 mpteq2dva 
 |-  ( ( ( ph /\ x e. ( Base ` C ) ) /\ ( y e. ( Base ` D ) /\ z e. ( Base ` D ) ) ) -> ( g e. ( y ( Hom ` D ) z ) |-> ( ( ( Id ` C ) ` x ) ( <. x , y >. ( 2nd ` F ) <. x , z >. ) g ) ) = ( g e. ( y ( Hom ` D ) z ) |-> ( ( y ( 2nd ` ( ( 1st ` G ) ` x ) ) z ) ` g ) ) )
69 64 feqmptd 
 |-  ( ( ( ph /\ x e. ( Base ` C ) ) /\ ( y e. ( Base ` D ) /\ z e. ( Base ` D ) ) ) -> ( y ( 2nd ` ( ( 1st ` G ) ` x ) ) z ) = ( g e. ( y ( Hom ` D ) z ) |-> ( ( y ( 2nd ` ( ( 1st ` G ) ` x ) ) z ) ` g ) ) )
70 68 69 eqtr4d 
 |-  ( ( ( ph /\ x e. ( Base ` C ) ) /\ ( y e. ( Base ` D ) /\ z e. ( Base ` D ) ) ) -> ( g e. ( y ( Hom ` D ) z ) |-> ( ( ( Id ` C ) ` x ) ( <. x , y >. ( 2nd ` F ) <. x , z >. ) g ) ) = ( y ( 2nd ` ( ( 1st ` G ) ` x ) ) z ) )
71 70 3impb 
 |-  ( ( ( ph /\ x e. ( Base ` C ) ) /\ y e. ( Base ` D ) /\ z e. ( Base ` D ) ) -> ( g e. ( y ( Hom ` D ) z ) |-> ( ( ( Id ` C ) ` x ) ( <. x , y >. ( 2nd ` F ) <. x , z >. ) g ) ) = ( y ( 2nd ` ( ( 1st ` G ) ` x ) ) z ) )
72 71 mpoeq3dva 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( y e. ( Base ` D ) , z e. ( Base ` D ) |-> ( g e. ( y ( Hom ` D ) z ) |-> ( ( ( Id ` C ) ` x ) ( <. x , y >. ( 2nd ` F ) <. x , z >. ) g ) ) ) = ( y e. ( Base ` D ) , z e. ( Base ` D ) |-> ( y ( 2nd ` ( ( 1st ` G ) ` x ) ) z ) ) )
73 9 24 funcfn2 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( 2nd ` ( ( 1st ` G ) ` x ) ) Fn ( ( Base ` D ) X. ( Base ` D ) ) )
74 fnov 
 |-  ( ( 2nd ` ( ( 1st ` G ) ` x ) ) Fn ( ( Base ` D ) X. ( Base ` D ) ) <-> ( 2nd ` ( ( 1st ` G ) ` x ) ) = ( y e. ( Base ` D ) , z e. ( Base ` D ) |-> ( y ( 2nd ` ( ( 1st ` G ) ` x ) ) z ) ) )
75 73 74 sylib 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( 2nd ` ( ( 1st ` G ) ` x ) ) = ( y e. ( Base ` D ) , z e. ( Base ` D ) |-> ( y ( 2nd ` ( ( 1st ` G ) ` x ) ) z ) ) )
76 72 75 eqtr4d 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( y e. ( Base ` D ) , z e. ( Base ` D ) |-> ( g e. ( y ( Hom ` D ) z ) |-> ( ( ( Id ` C ) ` x ) ( <. x , y >. ( 2nd ` F ) <. x , z >. ) g ) ) ) = ( 2nd ` ( ( 1st ` G ) ` x ) ) )
77 27 76 opeq12d 
 |-  ( ( 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 ) ) ) >. = <. ( 1st ` ( ( 1st ` G ) ` x ) ) , ( 2nd ` ( ( 1st ` G ) ` x ) ) >. )
78 1st2nd 
 |-  ( ( Rel ( D Func E ) /\ ( ( 1st ` G ) ` x ) e. ( D Func E ) ) -> ( ( 1st ` G ) ` x ) = <. ( 1st ` ( ( 1st ` G ) ` x ) ) , ( 2nd ` ( ( 1st ` G ) ` x ) ) >. )
79 15 22 78 sylancr 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( 1st ` G ) ` x ) = <. ( 1st ` ( ( 1st ` G ) ` x ) ) , ( 2nd ` ( ( 1st ` G ) ` x ) ) >. )
80 77 79 eqtr4d 
 |-  ( ( 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 ) ) ) >. = ( ( 1st ` G ) ` x ) )
81 80 mpteq2dva 
 |-  ( 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 ) ) ) >. ) = ( x e. ( Base ` C ) |-> ( ( 1st ` G ) ` x ) ) )
82 21 feqmptd 
 |-  ( ph -> ( 1st ` G ) = ( x e. ( Base ` C ) |-> ( ( 1st ` G ) ` x ) ) )
83 81 82 eqtr4d 
 |-  ( 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 ) ) ) >. ) = ( 1st ` G ) )
84 2 ad3antrrr 
 |-  ( ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ g e. ( x ( Hom ` C ) y ) ) /\ z e. ( Base ` D ) ) -> D e. Cat )
85 3 ad3antrrr 
 |-  ( ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ g e. ( x ( Hom ` C ) y ) ) /\ z e. ( Base ` D ) ) -> E e. Cat )
86 4 ad3antrrr 
 |-  ( ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ g e. ( x ( Hom ` C ) y ) ) /\ z e. ( Base ` D ) ) -> G e. ( C Func ( D FuncCat E ) ) )
87 simprl 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> x e. ( Base ` C ) )
88 87 ad2antrr 
 |-  ( ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ g e. ( x ( Hom ` C ) y ) ) /\ z e. ( Base ` D ) ) -> x e. ( Base ` C ) )
89 simpr 
 |-  ( ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ g e. ( x ( Hom ` C ) y ) ) /\ z e. ( Base ` D ) ) -> z e. ( Base ` D ) )
90 simprr 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> y e. ( Base ` C ) )
91 90 ad2antrr 
 |-  ( ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ g e. ( x ( Hom ` C ) y ) ) /\ z e. ( Base ` D ) ) -> y e. ( Base ` C ) )
92 simplr 
 |-  ( ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ g e. ( x ( Hom ` C ) y ) ) /\ z e. ( Base ` D ) ) -> g e. ( x ( Hom ` C ) y ) )
93 eqid 
 |-  ( Id ` D ) = ( Id ` D )
94 9 34 93 84 89 catidcl 
 |-  ( ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ g e. ( x ( Hom ` C ) y ) ) /\ z e. ( Base ` D ) ) -> ( ( Id ` D ) ` z ) e. ( z ( Hom ` D ) z ) )
95 1 84 85 86 8 9 88 89 33 34 91 89 92 94 uncf2 
 |-  ( ( ( ( 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 ) ) = ( ( ( ( x ( 2nd ` G ) y ) ` g ) ` z ) ( <. ( ( 1st ` ( ( 1st ` G ) ` x ) ) ` z ) , ( ( 1st ` ( ( 1st ` G ) ` x ) ) ` z ) >. ( comp ` E ) ( ( 1st ` ( ( 1st ` G ) ` y ) ) ` z ) ) ( ( z ( 2nd ` ( ( 1st ` G ) ` x ) ) z ) ` ( ( Id ` D ) ` z ) ) ) )
96 22 adantrr 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ( ( 1st ` G ) ` x ) e. ( D Func E ) )
97 96 adantr 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ g e. ( x ( Hom ` C ) y ) ) -> ( ( 1st ` G ) ` x ) e. ( D Func E ) )
98 15 97 23 sylancr 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ g e. ( x ( Hom ` C ) y ) ) -> ( 1st ` ( ( 1st ` G ) ` x ) ) ( D Func E ) ( 2nd ` ( ( 1st ` G ) ` x ) ) )
99 98 adantr 
 |-  ( ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ g e. ( x ( Hom ` C ) y ) ) /\ z e. ( Base ` D ) ) -> ( 1st ` ( ( 1st ` G ) ` x ) ) ( D Func E ) ( 2nd ` ( ( 1st ` G ) ` x ) ) )
100 9 93 48 99 89 funcid 
 |-  ( ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ g e. ( x ( Hom ` C ) y ) ) /\ z e. ( Base ` D ) ) -> ( ( z ( 2nd ` ( ( 1st ` G ) ` x ) ) z ) ` ( ( Id ` D ) ` z ) ) = ( ( Id ` E ) ` ( ( 1st ` ( ( 1st ` G ) ` x ) ) ` z ) ) )
101 100 oveq2d 
 |-  ( ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ g e. ( x ( Hom ` C ) y ) ) /\ z e. ( Base ` D ) ) -> ( ( ( ( x ( 2nd ` G ) y ) ` g ) ` z ) ( <. ( ( 1st ` ( ( 1st ` G ) ` x ) ) ` z ) , ( ( 1st ` ( ( 1st ` G ) ` x ) ) ` z ) >. ( comp ` E ) ( ( 1st ` ( ( 1st ` G ) ` y ) ) ` z ) ) ( ( z ( 2nd ` ( ( 1st ` G ) ` x ) ) z ) ` ( ( Id ` D ) ` z ) ) ) = ( ( ( ( x ( 2nd ` G ) y ) ` g ) ` z ) ( <. ( ( 1st ` ( ( 1st ` G ) ` x ) ) ` z ) , ( ( 1st ` ( ( 1st ` G ) ` x ) ) ` z ) >. ( comp ` E ) ( ( 1st ` ( ( 1st ` G ) ` y ) ) ` z ) ) ( ( Id ` E ) ` ( ( 1st ` ( ( 1st ` G ) ` x ) ) ` z ) ) ) )
102 9 14 98 funcf1 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ g e. ( x ( Hom ` C ) y ) ) -> ( 1st ` ( ( 1st ` G ) ` x ) ) : ( Base ` D ) --> ( Base ` E ) )
103 102 ffvelrnda 
 |-  ( ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ g e. ( x ( Hom ` C ) y ) ) /\ z e. ( Base ` D ) ) -> ( ( 1st ` ( ( 1st ` G ) ` x ) ) ` z ) e. ( Base ` E ) )
104 21 ffvelrnda 
 |-  ( ( ph /\ y e. ( Base ` C ) ) -> ( ( 1st ` G ) ` y ) e. ( D Func E ) )
105 104 adantrl 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ( ( 1st ` G ) ` y ) e. ( D Func E ) )
106 105 adantr 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ g e. ( x ( Hom ` C ) y ) ) -> ( ( 1st ` G ) ` y ) e. ( D Func E ) )
107 1st2ndbr 
 |-  ( ( Rel ( D Func E ) /\ ( ( 1st ` G ) ` y ) e. ( D Func E ) ) -> ( 1st ` ( ( 1st ` G ) ` y ) ) ( D Func E ) ( 2nd ` ( ( 1st ` G ) ` y ) ) )
108 15 106 107 sylancr 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ g e. ( x ( Hom ` C ) y ) ) -> ( 1st ` ( ( 1st ` G ) ` y ) ) ( D Func E ) ( 2nd ` ( ( 1st ` G ) ` y ) ) )
109 9 14 108 funcf1 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ g e. ( x ( Hom ` C ) y ) ) -> ( 1st ` ( ( 1st ` G ) ` y ) ) : ( Base ` D ) --> ( Base ` E ) )
110 109 ffvelrnda 
 |-  ( ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ g e. ( x ( Hom ` C ) y ) ) /\ z e. ( Base ` D ) ) -> ( ( 1st ` ( ( 1st ` G ) ` y ) ) ` z ) e. ( Base ` E ) )
111 eqid 
 |-  ( D Nat E ) = ( D Nat E )
112 16 111 fuchom 
 |-  ( D Nat E ) = ( Hom ` ( D FuncCat E ) )
113 20 ad3antrrr 
 |-  ( ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ g e. ( x ( Hom ` C ) y ) ) /\ z e. ( Base ` D ) ) -> ( 1st ` G ) ( C Func ( D FuncCat E ) ) ( 2nd ` G ) )
114 8 33 112 113 88 91 funcf2 
 |-  ( ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ g e. ( x ( Hom ` C ) y ) ) /\ z e. ( Base ` D ) ) -> ( x ( 2nd ` G ) y ) : ( x ( Hom ` C ) y ) --> ( ( ( 1st ` G ) ` x ) ( D Nat E ) ( ( 1st ` G ) ` y ) ) )
115 114 92 ffvelrnd 
 |-  ( ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ g e. ( x ( Hom ` C ) y ) ) /\ z e. ( Base ` D ) ) -> ( ( x ( 2nd ` G ) y ) ` g ) e. ( ( ( 1st ` G ) ` x ) ( D Nat E ) ( ( 1st ` G ) ` y ) ) )
116 111 115 nat1st2nd 
 |-  ( ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ g e. ( x ( Hom ` C ) y ) ) /\ z e. ( Base ` D ) ) -> ( ( x ( 2nd ` G ) y ) ` g ) e. ( <. ( 1st ` ( ( 1st ` G ) ` x ) ) , ( 2nd ` ( ( 1st ` G ) ` x ) ) >. ( D Nat E ) <. ( 1st ` ( ( 1st ` G ) ` y ) ) , ( 2nd ` ( ( 1st ` G ) ` y ) ) >. ) )
117 111 116 9 58 89 natcl 
 |-  ( ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ g e. ( x ( Hom ` C ) y ) ) /\ z e. ( Base ` D ) ) -> ( ( ( x ( 2nd ` G ) y ) ` g ) ` z ) e. ( ( ( 1st ` ( ( 1st ` G ) ` x ) ) ` z ) ( Hom ` E ) ( ( 1st ` ( ( 1st ` G ) ` y ) ) ` z ) ) )
118 14 58 48 85 103 60 110 117 catrid 
 |-  ( ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ g e. ( x ( Hom ` C ) y ) ) /\ z e. ( Base ` D ) ) -> ( ( ( ( x ( 2nd ` G ) y ) ` g ) ` z ) ( <. ( ( 1st ` ( ( 1st ` G ) ` x ) ) ` z ) , ( ( 1st ` ( ( 1st ` G ) ` x ) ) ` z ) >. ( comp ` E ) ( ( 1st ` ( ( 1st ` G ) ` y ) ) ` z ) ) ( ( Id ` E ) ` ( ( 1st ` ( ( 1st ` G ) ` x ) ) ` z ) ) ) = ( ( ( x ( 2nd ` G ) y ) ` g ) ` z ) )
119 95 101 118 3eqtrd 
 |-  ( ( ( ( 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 ) ) = ( ( ( x ( 2nd ` G ) y ) ` g ) ` z ) )
120 119 mpteq2dva 
 |-  ( ( ( 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 ) ) ) = ( z e. ( Base ` D ) |-> ( ( ( x ( 2nd ` G ) y ) ` g ) ` z ) ) )
121 20 adantr 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ( 1st ` G ) ( C Func ( D FuncCat E ) ) ( 2nd ` G ) )
122 8 33 112 121 87 90 funcf2 
 |-  ( ( 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 ) ) )
123 122 ffvelrnda 
 |-  ( ( ( 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 ) ) )
124 111 123 nat1st2nd 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ g e. ( x ( Hom ` C ) y ) ) -> ( ( x ( 2nd ` G ) y ) ` g ) e. ( <. ( 1st ` ( ( 1st ` G ) ` x ) ) , ( 2nd ` ( ( 1st ` G ) ` x ) ) >. ( D Nat E ) <. ( 1st ` ( ( 1st ` G ) ` y ) ) , ( 2nd ` ( ( 1st ` G ) ` y ) ) >. ) )
125 111 124 9 natfn 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ g e. ( x ( Hom ` C ) y ) ) -> ( ( x ( 2nd ` G ) y ) ` g ) Fn ( Base ` D ) )
126 dffn5 
 |-  ( ( ( x ( 2nd ` G ) y ) ` g ) Fn ( Base ` D ) <-> ( ( x ( 2nd ` G ) y ) ` g ) = ( z e. ( Base ` D ) |-> ( ( ( x ( 2nd ` G ) y ) ` g ) ` z ) ) )
127 125 126 sylib 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ g e. ( x ( Hom ` C ) y ) ) -> ( ( x ( 2nd ` G ) y ) ` g ) = ( z e. ( Base ` D ) |-> ( ( ( x ( 2nd ` G ) y ) ` g ) ` z ) ) )
128 120 127 eqtr4d 
 |-  ( ( ( 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 ) ) ) = ( ( x ( 2nd ` G ) y ) ` g ) )
129 128 mpteq2dva 
 |-  ( ( 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 ) ) ) ) = ( g e. ( x ( Hom ` C ) y ) |-> ( ( x ( 2nd ` G ) y ) ` g ) ) )
130 122 feqmptd 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ( x ( 2nd ` G ) y ) = ( g e. ( x ( Hom ` C ) y ) |-> ( ( x ( 2nd ` G ) y ) ` g ) ) )
131 129 130 eqtr4d 
 |-  ( ( 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 ) ) ) ) = ( x ( 2nd ` G ) y ) )
132 131 3impb 
 |-  ( ( 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 ) ) ) ) = ( x ( 2nd ` G ) y ) )
133 132 mpoeq3dva 
 |-  ( 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 ) ) ) ) ) = ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> ( x ( 2nd ` G ) y ) ) )
134 8 20 funcfn2 
 |-  ( ph -> ( 2nd ` G ) Fn ( ( Base ` C ) X. ( Base ` C ) ) )
135 fnov 
 |-  ( ( 2nd ` G ) Fn ( ( Base ` C ) X. ( Base ` C ) ) <-> ( 2nd ` G ) = ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> ( x ( 2nd ` G ) y ) ) )
136 134 135 sylib 
 |-  ( ph -> ( 2nd ` G ) = ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> ( x ( 2nd ` G ) y ) ) )
137 133 136 eqtr4d 
 |-  ( 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 ) ) ) ) ) = ( 2nd ` G ) )
138 83 137 opeq12d 
 |-  ( 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 ) ) ) >. ) , ( 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 ) , ( 2nd ` G ) >. )
139 eqid 
 |-  ( <. C , D >. curryF F ) = ( <. C , D >. curryF F )
140 1 2 3 4 uncfcl 
 |-  ( ph -> F e. ( ( C Xc. D ) Func E ) )
141 139 8 40 2 140 9 34 37 33 93 curfval 
 |-  ( ph -> ( <. C , D >. curryF F ) = <. ( 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 ) ) ) ) ) >. )
142 1st2nd 
 |-  ( ( Rel ( C Func ( D FuncCat E ) ) /\ G e. ( C Func ( D FuncCat E ) ) ) -> G = <. ( 1st ` G ) , ( 2nd ` G ) >. )
143 18 4 142 sylancr 
 |-  ( ph -> G = <. ( 1st ` G ) , ( 2nd ` G ) >. )
144 138 141 143 3eqtr4d 
 |-  ( ph -> ( <. C , D >. curryF F ) = G )