Metamath Proof Explorer

Definition df-curf

Description: Define the curry functor, which maps a functor F : C X. D --> E to curryF ( F ) : C --> ( D --> E ) . (Contributed by Mario Carneiro, 11-Jan-2017)

Ref Expression
Assertion df-curf 
|- curryF = ( e e. _V , f e. _V |-> [_ ( 1st ` e ) / c ]_ [_ ( 2nd ` e ) / d ]_ <. ( 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 ) ) ) ) ) >. )

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccurf 
 |-  curryF
1 ve 
 |-  e
2 cvv 
 |-  _V
3 vf 
 |-  f
4 c1st 
 |-  1st
5 1 cv 
 |-  e
6 5 4 cfv 
 |-  ( 1st ` e )
7 vc 
 |-  c
8 c2nd 
 |-  2nd
9 5 8 cfv 
 |-  ( 2nd ` e )
10 vd 
 |-  d
11 vx 
 |-  x
12 cbs 
 |-  Base
13 7 cv 
 |-  c
14 13 12 cfv 
 |-  ( Base ` c )
15 vy 
 |-  y
16 10 cv 
 |-  d
17 16 12 cfv 
 |-  ( Base ` d )
18 11 cv 
 |-  x
19 3 cv 
 |-  f
20 19 4 cfv 
 |-  ( 1st ` f )
21 15 cv 
 |-  y
22 18 21 20 co 
 |-  ( x ( 1st ` f ) y )
23 15 17 22 cmpt 
 |-  ( y e. ( Base ` d ) |-> ( x ( 1st ` f ) y ) )
24 vz 
 |-  z
25 vg 
 |-  g
26 chom 
 |-  Hom
27 16 26 cfv 
 |-  ( Hom ` d )
28 24 cv 
 |-  z
29 21 28 27 co 
 |-  ( y ( Hom ` d ) z )
30 ccid 
 |-  Id
31 13 30 cfv 
 |-  ( Id ` c )
32 18 31 cfv 
 |-  ( ( Id ` c ) ` x )
33 18 21 cop 
 |-  <. x , y >.
34 19 8 cfv 
 |-  ( 2nd ` f )
35 18 28 cop 
 |-  <. x , z >.
36 33 35 34 co 
 |-  ( <. x , y >. ( 2nd ` f ) <. x , z >. )
37 25 cv 
 |-  g
38 32 37 36 co 
 |-  ( ( ( Id ` c ) ` x ) ( <. x , y >. ( 2nd ` f ) <. x , z >. ) g )
39 25 29 38 cmpt 
 |-  ( g e. ( y ( Hom ` d ) z ) |-> ( ( ( Id ` c ) ` x ) ( <. x , y >. ( 2nd ` f ) <. x , z >. ) g ) )
40 15 24 17 17 39 cmpo 
 |-  ( y e. ( Base ` d ) , z e. ( Base ` d ) |-> ( g e. ( y ( Hom ` d ) z ) |-> ( ( ( Id ` c ) ` x ) ( <. x , y >. ( 2nd ` f ) <. x , z >. ) g ) ) )
41 23 40 cop 
 |-  <. ( 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 ) ) ) >.
42 11 14 41 cmpt 
 |-  ( 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 ) ) ) >. )
43 13 26 cfv 
 |-  ( Hom ` c )
44 18 21 43 co 
 |-  ( x ( Hom ` c ) y )
45 21 28 cop 
 |-  <. y , z >.
46 35 45 34 co 
 |-  ( <. x , z >. ( 2nd ` f ) <. y , z >. )
47 16 30 cfv 
 |-  ( Id ` d )
48 28 47 cfv 
 |-  ( ( Id ` d ) ` z )
49 37 48 46 co 
 |-  ( g ( <. x , z >. ( 2nd ` f ) <. y , z >. ) ( ( Id ` d ) ` z ) )
50 24 17 49 cmpt 
 |-  ( z e. ( Base ` d ) |-> ( g ( <. x , z >. ( 2nd ` f ) <. y , z >. ) ( ( Id ` d ) ` z ) ) )
51 25 44 50 cmpt 
 |-  ( g e. ( x ( Hom ` c ) y ) |-> ( z e. ( Base ` d ) |-> ( g ( <. x , z >. ( 2nd ` f ) <. y , z >. ) ( ( Id ` d ) ` z ) ) ) )
52 11 15 14 14 51 cmpo 
 |-  ( 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 ) ) ) ) )
53 42 52 cop 
 |-  <. ( 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 ) ) ) ) ) >.
54 10 9 53 csb 
 |-  [_ ( 2nd ` e ) / d ]_ <. ( 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 ) ) ) ) ) >.
55 7 6 54 csb 
 |-  [_ ( 1st ` e ) / c ]_ [_ ( 2nd ` e ) / d ]_ <. ( 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 ) ) ) ) ) >.
56 1 3 2 2 55 cmpo 
 |-  ( e e. _V , f e. _V |-> [_ ( 1st ` e ) / c ]_ [_ ( 2nd ` e ) / d ]_ <. ( 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 ) ) ) ) ) >. )
57 0 56 wceq 
 |-  curryF = ( e e. _V , f e. _V |-> [_ ( 1st ` e ) / c ]_ [_ ( 2nd ` e ) / d ]_ <. ( 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 ) ) ) ) ) >. )