MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-curf Unicode version

Definition df-curf 13988
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.)
Assertion
Ref Expression
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 ) ) ) ) ) >. )
Distinct variable group:    c, d, f, g, x, y, e, z

Detailed syntax breakdown of Definition df-curf
StepHypRef Expression
1 ccurf 13984 . 2  class curryF
2 ve . . 3  set  e
3 vf . . 3  set  f
4 cvv 2788 . . 3  class  _V
5 vc . . . 4  set  c
62cv 1622 . . . . 5  class  e
7 c1st 6120 . . . . 5  class  1st
86, 7cfv 5255 . . . 4  class  ( 1st `  e )
9 vd . . . . 5  set  d
10 c2nd 6121 . . . . . 6  class  2nd
116, 10cfv 5255 . . . . 5  class  ( 2nd `  e )
12 vx . . . . . . 7  set  x
135cv 1622 . . . . . . . 8  class  c
14 cbs 13148 . . . . . . . 8  class  Base
1513, 14cfv 5255 . . . . . . 7  class  ( Base `  c )
16 vy . . . . . . . . 9  set  y
179cv 1622 . . . . . . . . . 10  class  d
1817, 14cfv 5255 . . . . . . . . 9  class  ( Base `  d )
1912cv 1622 . . . . . . . . . 10  class  x
2016cv 1622 . . . . . . . . . 10  class  y
213cv 1622 . . . . . . . . . . 11  class  f
2221, 7cfv 5255 . . . . . . . . . 10  class  ( 1st `  f )
2319, 20, 22co 5858 . . . . . . . . 9  class  ( x ( 1st `  f
) y )
2416, 18, 23cmpt 4077 . . . . . . . 8  class  ( y  e.  ( Base `  d
)  |->  ( x ( 1st `  f ) y ) )
25 vz . . . . . . . . 9  set  z
26 vg . . . . . . . . . 10  set  g
2725cv 1622 . . . . . . . . . . 11  class  z
28 chom 13219 . . . . . . . . . . . 12  class  Hom
2917, 28cfv 5255 . . . . . . . . . . 11  class  (  Hom  `  d )
3020, 27, 29co 5858 . . . . . . . . . 10  class  ( y (  Hom  `  d
) z )
31 ccid 13567 . . . . . . . . . . . . 13  class  Id
3213, 31cfv 5255 . . . . . . . . . . . 12  class  ( Id
`  c )
3319, 32cfv 5255 . . . . . . . . . . 11  class  ( ( Id `  c ) `
 x )
3426cv 1622 . . . . . . . . . . 11  class  g
3519, 20cop 3643 . . . . . . . . . . . 12  class  <. x ,  y >.
3619, 27cop 3643 . . . . . . . . . . . 12  class  <. x ,  z >.
3721, 10cfv 5255 . . . . . . . . . . . 12  class  ( 2nd `  f )
3835, 36, 37co 5858 . . . . . . . . . . 11  class  ( <.
x ,  y >.
( 2nd `  f
) <. x ,  z
>. )
3933, 34, 38co 5858 . . . . . . . . . 10  class  ( ( ( Id `  c
) `  x )
( <. x ,  y
>. ( 2nd `  f
) <. x ,  z
>. ) g )
4026, 30, 39cmpt 4077 . . . . . . . . 9  class  ( g  e.  ( y (  Hom  `  d )
z )  |->  ( ( ( Id `  c
) `  x )
( <. x ,  y
>. ( 2nd `  f
) <. x ,  z
>. ) g ) )
4116, 25, 18, 18, 40cmpt2 5860 . . . . . . . 8  class  ( y  e.  ( Base `  d
) ,  z  e.  ( Base `  d
)  |->  ( g  e.  ( y (  Hom  `  d ) z ) 
|->  ( ( ( Id
`  c ) `  x ) ( <.
x ,  y >.
( 2nd `  f
) <. x ,  z
>. ) g ) ) )
4224, 41cop 3643 . . . . . . 7  class  <. (
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 ) ) ) >.
4312, 15, 42cmpt 4077 . . . . . 6  class  ( 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 ) ) ) >. )
4413, 28cfv 5255 . . . . . . . . 9  class  (  Hom  `  c )
4519, 20, 44co 5858 . . . . . . . 8  class  ( x (  Hom  `  c
) y )
4617, 31cfv 5255 . . . . . . . . . . 11  class  ( Id
`  d )
4727, 46cfv 5255 . . . . . . . . . 10  class  ( ( Id `  d ) `
 z )
4820, 27cop 3643 . . . . . . . . . . 11  class  <. y ,  z >.
4936, 48, 37co 5858 . . . . . . . . . 10  class  ( <.
x ,  z >.
( 2nd `  f
) <. y ,  z
>. )
5034, 47, 49co 5858 . . . . . . . . 9  class  ( g ( <. x ,  z
>. ( 2nd `  f
) <. y ,  z
>. ) ( ( Id
`  d ) `  z ) )
5125, 18, 50cmpt 4077 . . . . . . . 8  class  ( z  e.  ( Base `  d
)  |->  ( g (
<. x ,  z >.
( 2nd `  f
) <. y ,  z
>. ) ( ( Id
`  d ) `  z ) ) )
5226, 45, 51cmpt 4077 . . . . . . 7  class  ( g  e.  ( x (  Hom  `  c )
y )  |->  ( z  e.  ( Base `  d
)  |->  ( g (
<. x ,  z >.
( 2nd `  f
) <. y ,  z
>. ) ( ( Id
`  d ) `  z ) ) ) )
5312, 16, 15, 15, 52cmpt2 5860 . . . . . 6  class  ( 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 ) ) ) ) )
5443, 53cop 3643 . . . . 5  class  <. (
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 ) ) ) ) ) >.
559, 11, 54csb 3081 . . . 4  class  [_ ( 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 ) ) ) ) ) >.
565, 8, 55csb 3081 . . 3  class  [_ ( 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 ) ) ) ) ) >.
572, 3, 4, 4, 56cmpt2 5860 . 2  class  ( 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 ) ) ) ) ) >. )
581, 57wceq 1623 1  wff 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 ) ) ) ) ) >. )
Colors of variables: wff set class
This definition is referenced by:  curfval  13997
  Copyright terms: Public domain W3C validator