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 = ( 𝑒 ∈ V , 𝑓 ∈ V ↦ ⦋ ( 1st ‘ 𝑒 ) / 𝑐 ⦌ ⦋ ( 2nd ‘ 𝑒 ) / 𝑑 ⦌ ⟨ ( 𝑥 ∈ ( Base ‘ 𝑐 ) ↦ ⟨ ( 𝑦 ∈ ( Base ‘ 𝑑 ) ↦ ( 𝑥 ( 1st ‘ 𝑓 ) 𝑦 ) ) , ( 𝑦 ∈ ( Base ‘ 𝑑 ) , 𝑧 ∈ ( Base ‘ 𝑑 ) ↦ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑑 ) 𝑧 ) ↦ ( ( ( Id ‘ 𝑐 ) ‘ 𝑥 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2nd ‘ 𝑓 ) ⟨ 𝑥 , 𝑧 ⟩ ) 𝑔 ) ) ) ⟩ ) , ( 𝑥 ∈ ( Base ‘ 𝑐 ) , 𝑦 ∈ ( Base ‘ 𝑐 ) ↦ ( 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝑐 ) 𝑦 ) ↦ ( 𝑧 ∈ ( Base ‘ 𝑑 ) ↦ ( 𝑔 ( ⟨ 𝑥 , 𝑧 ⟩ ( 2nd ‘ 𝑓 ) ⟨ 𝑦 , 𝑧 ⟩ ) ( ( Id ‘ 𝑑 ) ‘ 𝑧 ) ) ) ) ) ⟩ )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccurf	⊢ curryF
1		ve	⊢ 𝑒
2		cvv	⊢ V
3		vf	⊢ 𝑓
4		c1st	⊢ 1st
5	1	cv	⊢ 𝑒
6	5 4	cfv	⊢ ( 1st ‘ 𝑒 )
7		vc	⊢ 𝑐
8		c2nd	⊢ 2nd
9	5 8	cfv	⊢ ( 2nd ‘ 𝑒 )
10		vd	⊢ 𝑑
11		vx	⊢ 𝑥
12		cbs	⊢ Base
13	7	cv	⊢ 𝑐
14	13 12	cfv	⊢ ( Base ‘ 𝑐 )
15		vy	⊢ 𝑦
16	10	cv	⊢ 𝑑
17	16 12	cfv	⊢ ( Base ‘ 𝑑 )
18	11	cv	⊢ 𝑥
19	3	cv	⊢ 𝑓
20	19 4	cfv	⊢ ( 1st ‘ 𝑓 )
21	15	cv	⊢ 𝑦
22	18 21 20	co	⊢ ( 𝑥 ( 1st ‘ 𝑓 ) 𝑦 )
23	15 17 22	cmpt	⊢ ( 𝑦 ∈ ( Base ‘ 𝑑 ) ↦ ( 𝑥 ( 1st ‘ 𝑓 ) 𝑦 ) )
24		vz	⊢ 𝑧
25		vg	⊢ 𝑔
26		chom	⊢ Hom
27	16 26	cfv	⊢ ( Hom ‘ 𝑑 )
28	24	cv	⊢ 𝑧
29	21 28 27	co	⊢ ( 𝑦 ( Hom ‘ 𝑑 ) 𝑧 )
30		ccid	⊢ Id
31	13 30	cfv	⊢ ( Id ‘ 𝑐 )
32	18 31	cfv	⊢ ( ( Id ‘ 𝑐 ) ‘ 𝑥 )
33	18 21	cop	⊢ ⟨ 𝑥 , 𝑦 ⟩
34	19 8	cfv	⊢ ( 2nd ‘ 𝑓 )
35	18 28	cop	⊢ ⟨ 𝑥 , 𝑧 ⟩
36	33 35 34	co	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ( 2nd ‘ 𝑓 ) ⟨ 𝑥 , 𝑧 ⟩ )
37	25	cv	⊢ 𝑔
38	32 37 36	co	⊢ ( ( ( Id ‘ 𝑐 ) ‘ 𝑥 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2nd ‘ 𝑓 ) ⟨ 𝑥 , 𝑧 ⟩ ) 𝑔 )
39	25 29 38	cmpt	⊢ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑑 ) 𝑧 ) ↦ ( ( ( Id ‘ 𝑐 ) ‘ 𝑥 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2nd ‘ 𝑓 ) ⟨ 𝑥 , 𝑧 ⟩ ) 𝑔 ) )
40	15 24 17 17 39	cmpo	⊢ ( 𝑦 ∈ ( Base ‘ 𝑑 ) , 𝑧 ∈ ( Base ‘ 𝑑 ) ↦ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑑 ) 𝑧 ) ↦ ( ( ( Id ‘ 𝑐 ) ‘ 𝑥 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2nd ‘ 𝑓 ) ⟨ 𝑥 , 𝑧 ⟩ ) 𝑔 ) ) )
41	23 40	cop	⊢ ⟨ ( 𝑦 ∈ ( Base ‘ 𝑑 ) ↦ ( 𝑥 ( 1st ‘ 𝑓 ) 𝑦 ) ) , ( 𝑦 ∈ ( Base ‘ 𝑑 ) , 𝑧 ∈ ( Base ‘ 𝑑 ) ↦ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑑 ) 𝑧 ) ↦ ( ( ( Id ‘ 𝑐 ) ‘ 𝑥 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2nd ‘ 𝑓 ) ⟨ 𝑥 , 𝑧 ⟩ ) 𝑔 ) ) ) ⟩
42	11 14 41	cmpt	⊢ ( 𝑥 ∈ ( Base ‘ 𝑐 ) ↦ ⟨ ( 𝑦 ∈ ( Base ‘ 𝑑 ) ↦ ( 𝑥 ( 1st ‘ 𝑓 ) 𝑦 ) ) , ( 𝑦 ∈ ( Base ‘ 𝑑 ) , 𝑧 ∈ ( Base ‘ 𝑑 ) ↦ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑑 ) 𝑧 ) ↦ ( ( ( Id ‘ 𝑐 ) ‘ 𝑥 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2nd ‘ 𝑓 ) ⟨ 𝑥 , 𝑧 ⟩ ) 𝑔 ) ) ) ⟩ )
43	13 26	cfv	⊢ ( Hom ‘ 𝑐 )
44	18 21 43	co	⊢ ( 𝑥 ( Hom ‘ 𝑐 ) 𝑦 )
45	21 28	cop	⊢ ⟨ 𝑦 , 𝑧 ⟩
46	35 45 34	co	⊢ ( ⟨ 𝑥 , 𝑧 ⟩ ( 2nd ‘ 𝑓 ) ⟨ 𝑦 , 𝑧 ⟩ )
47	16 30	cfv	⊢ ( Id ‘ 𝑑 )
48	28 47	cfv	⊢ ( ( Id ‘ 𝑑 ) ‘ 𝑧 )
49	37 48 46	co	⊢ ( 𝑔 ( ⟨ 𝑥 , 𝑧 ⟩ ( 2nd ‘ 𝑓 ) ⟨ 𝑦 , 𝑧 ⟩ ) ( ( Id ‘ 𝑑 ) ‘ 𝑧 ) )
50	24 17 49	cmpt	⊢ ( 𝑧 ∈ ( Base ‘ 𝑑 ) ↦ ( 𝑔 ( ⟨ 𝑥 , 𝑧 ⟩ ( 2nd ‘ 𝑓 ) ⟨ 𝑦 , 𝑧 ⟩ ) ( ( Id ‘ 𝑑 ) ‘ 𝑧 ) ) )
51	25 44 50	cmpt	⊢ ( 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝑐 ) 𝑦 ) ↦ ( 𝑧 ∈ ( Base ‘ 𝑑 ) ↦ ( 𝑔 ( ⟨ 𝑥 , 𝑧 ⟩ ( 2nd ‘ 𝑓 ) ⟨ 𝑦 , 𝑧 ⟩ ) ( ( Id ‘ 𝑑 ) ‘ 𝑧 ) ) ) )
52	11 15 14 14 51	cmpo	⊢ ( 𝑥 ∈ ( Base ‘ 𝑐 ) , 𝑦 ∈ ( Base ‘ 𝑐 ) ↦ ( 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝑐 ) 𝑦 ) ↦ ( 𝑧 ∈ ( Base ‘ 𝑑 ) ↦ ( 𝑔 ( ⟨ 𝑥 , 𝑧 ⟩ ( 2nd ‘ 𝑓 ) ⟨ 𝑦 , 𝑧 ⟩ ) ( ( Id ‘ 𝑑 ) ‘ 𝑧 ) ) ) ) )
53	42 52	cop	⊢ ⟨ ( 𝑥 ∈ ( Base ‘ 𝑐 ) ↦ ⟨ ( 𝑦 ∈ ( Base ‘ 𝑑 ) ↦ ( 𝑥 ( 1st ‘ 𝑓 ) 𝑦 ) ) , ( 𝑦 ∈ ( Base ‘ 𝑑 ) , 𝑧 ∈ ( Base ‘ 𝑑 ) ↦ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑑 ) 𝑧 ) ↦ ( ( ( Id ‘ 𝑐 ) ‘ 𝑥 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2nd ‘ 𝑓 ) ⟨ 𝑥 , 𝑧 ⟩ ) 𝑔 ) ) ) ⟩ ) , ( 𝑥 ∈ ( Base ‘ 𝑐 ) , 𝑦 ∈ ( Base ‘ 𝑐 ) ↦ ( 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝑐 ) 𝑦 ) ↦ ( 𝑧 ∈ ( Base ‘ 𝑑 ) ↦ ( 𝑔 ( ⟨ 𝑥 , 𝑧 ⟩ ( 2nd ‘ 𝑓 ) ⟨ 𝑦 , 𝑧 ⟩ ) ( ( Id ‘ 𝑑 ) ‘ 𝑧 ) ) ) ) ) ⟩
54	10 9 53	csb	⊢ ⦋ ( 2nd ‘ 𝑒 ) / 𝑑 ⦌ ⟨ ( 𝑥 ∈ ( Base ‘ 𝑐 ) ↦ ⟨ ( 𝑦 ∈ ( Base ‘ 𝑑 ) ↦ ( 𝑥 ( 1st ‘ 𝑓 ) 𝑦 ) ) , ( 𝑦 ∈ ( Base ‘ 𝑑 ) , 𝑧 ∈ ( Base ‘ 𝑑 ) ↦ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑑 ) 𝑧 ) ↦ ( ( ( Id ‘ 𝑐 ) ‘ 𝑥 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2nd ‘ 𝑓 ) ⟨ 𝑥 , 𝑧 ⟩ ) 𝑔 ) ) ) ⟩ ) , ( 𝑥 ∈ ( Base ‘ 𝑐 ) , 𝑦 ∈ ( Base ‘ 𝑐 ) ↦ ( 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝑐 ) 𝑦 ) ↦ ( 𝑧 ∈ ( Base ‘ 𝑑 ) ↦ ( 𝑔 ( ⟨ 𝑥 , 𝑧 ⟩ ( 2nd ‘ 𝑓 ) ⟨ 𝑦 , 𝑧 ⟩ ) ( ( Id ‘ 𝑑 ) ‘ 𝑧 ) ) ) ) ) ⟩
55	7 6 54	csb	⊢ ⦋ ( 1st ‘ 𝑒 ) / 𝑐 ⦌ ⦋ ( 2nd ‘ 𝑒 ) / 𝑑 ⦌ ⟨ ( 𝑥 ∈ ( Base ‘ 𝑐 ) ↦ ⟨ ( 𝑦 ∈ ( Base ‘ 𝑑 ) ↦ ( 𝑥 ( 1st ‘ 𝑓 ) 𝑦 ) ) , ( 𝑦 ∈ ( Base ‘ 𝑑 ) , 𝑧 ∈ ( Base ‘ 𝑑 ) ↦ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑑 ) 𝑧 ) ↦ ( ( ( Id ‘ 𝑐 ) ‘ 𝑥 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2nd ‘ 𝑓 ) ⟨ 𝑥 , 𝑧 ⟩ ) 𝑔 ) ) ) ⟩ ) , ( 𝑥 ∈ ( Base ‘ 𝑐 ) , 𝑦 ∈ ( Base ‘ 𝑐 ) ↦ ( 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝑐 ) 𝑦 ) ↦ ( 𝑧 ∈ ( Base ‘ 𝑑 ) ↦ ( 𝑔 ( ⟨ 𝑥 , 𝑧 ⟩ ( 2nd ‘ 𝑓 ) ⟨ 𝑦 , 𝑧 ⟩ ) ( ( Id ‘ 𝑑 ) ‘ 𝑧 ) ) ) ) ) ⟩
56	1 3 2 2 55	cmpo	⊢ ( 𝑒 ∈ V , 𝑓 ∈ V ↦ ⦋ ( 1st ‘ 𝑒 ) / 𝑐 ⦌ ⦋ ( 2nd ‘ 𝑒 ) / 𝑑 ⦌ ⟨ ( 𝑥 ∈ ( Base ‘ 𝑐 ) ↦ ⟨ ( 𝑦 ∈ ( Base ‘ 𝑑 ) ↦ ( 𝑥 ( 1st ‘ 𝑓 ) 𝑦 ) ) , ( 𝑦 ∈ ( Base ‘ 𝑑 ) , 𝑧 ∈ ( Base ‘ 𝑑 ) ↦ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑑 ) 𝑧 ) ↦ ( ( ( Id ‘ 𝑐 ) ‘ 𝑥 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2nd ‘ 𝑓 ) ⟨ 𝑥 , 𝑧 ⟩ ) 𝑔 ) ) ) ⟩ ) , ( 𝑥 ∈ ( Base ‘ 𝑐 ) , 𝑦 ∈ ( Base ‘ 𝑐 ) ↦ ( 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝑐 ) 𝑦 ) ↦ ( 𝑧 ∈ ( Base ‘ 𝑑 ) ↦ ( 𝑔 ( ⟨ 𝑥 , 𝑧 ⟩ ( 2nd ‘ 𝑓 ) ⟨ 𝑦 , 𝑧 ⟩ ) ( ( Id ‘ 𝑑 ) ‘ 𝑧 ) ) ) ) ) ⟩ )
57	0 56	wceq	⊢ curryF = ( 𝑒 ∈ V , 𝑓 ∈ V ↦ ⦋ ( 1st ‘ 𝑒 ) / 𝑐 ⦌ ⦋ ( 2nd ‘ 𝑒 ) / 𝑑 ⦌ ⟨ ( 𝑥 ∈ ( Base ‘ 𝑐 ) ↦ ⟨ ( 𝑦 ∈ ( Base ‘ 𝑑 ) ↦ ( 𝑥 ( 1st ‘ 𝑓 ) 𝑦 ) ) , ( 𝑦 ∈ ( Base ‘ 𝑑 ) , 𝑧 ∈ ( Base ‘ 𝑑 ) ↦ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑑 ) 𝑧 ) ↦ ( ( ( Id ‘ 𝑐 ) ‘ 𝑥 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2nd ‘ 𝑓 ) ⟨ 𝑥 , 𝑧 ⟩ ) 𝑔 ) ) ) ⟩ ) , ( 𝑥 ∈ ( Base ‘ 𝑐 ) , 𝑦 ∈ ( Base ‘ 𝑐 ) ↦ ( 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝑐 ) 𝑦 ) ↦ ( 𝑧 ∈ ( Base ‘ 𝑑 ) ↦ ( 𝑔 ( ⟨ 𝑥 , 𝑧 ⟩ ( 2nd ‘ 𝑓 ) ⟨ 𝑦 , 𝑧 ⟩ ) ( ( Id ‘ 𝑑 ) ‘ 𝑧 ) ) ) ) ) ⟩ )