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 = ( 𝑒 ∈ 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 ‘ 𝑑 ) ‘ 𝑧 ) ) ) ) ) ⟩ )