This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ‘ 𝑑 ) ‘ 𝑧 ) ) ) ) ) ⟩ )