Definition df-curf 16854

Description: Define the curry functor, which maps a functor F : C X. D --> E to curry_F ( 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

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

This definition is referenced by:  curfval  16863