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

Definition df-curf 16848
Description: Define the curry functor, which maps a functor 𝐹:𝐶 × 𝐷𝐸 to curryF (𝐹):𝐶⟶(𝐷𝐸). (Contributed by Mario Carneiro, 11-Jan-2017.)
Assertion
Ref Expression
df-curf curryF = (𝑒 ∈ V, 𝑓 ∈ V ↦ (1st𝑒) / 𝑐(2nd𝑒) / 𝑑⟨(𝑥 ∈ (Base‘𝑐) ↦ ⟨(𝑦 ∈ (Base‘𝑑) ↦ (𝑥(1st𝑓)𝑦)), (𝑦 ∈ (Base‘𝑑), 𝑧 ∈ (Base‘𝑑) ↦ (𝑔 ∈ (𝑦(Hom ‘𝑑)𝑧) ↦ (((Id‘𝑐)‘𝑥)(⟨𝑥, 𝑦⟩(2nd𝑓)⟨𝑥, 𝑧⟩)𝑔)))⟩), (𝑥 ∈ (Base‘𝑐), 𝑦 ∈ (Base‘𝑐) ↦ (𝑔 ∈ (𝑥(Hom ‘𝑐)𝑦) ↦ (𝑧 ∈ (Base‘𝑑) ↦ (𝑔(⟨𝑥, 𝑧⟩(2nd𝑓)⟨𝑦, 𝑧⟩)((Id‘𝑑)‘𝑧)))))⟩)
Distinct variable group:   𝑐,𝑑,𝑓,𝑔,𝑥,𝑦,𝑒,𝑧

Detailed syntax breakdown of Definition df-curf
StepHypRef Expression
1 ccurf 16844 . 2 class curryF
2 ve . . 3 setvar 𝑒
3 vf . . 3 setvar 𝑓
4 cvv 3198 . . 3 class V
5 vc . . . 4 setvar 𝑐
62cv 1481 . . . . 5 class 𝑒
7 c1st 7163 . . . . 5 class 1st
86, 7cfv 5886 . . . 4 class (1st𝑒)
9 vd . . . . 5 setvar 𝑑
10 c2nd 7164 . . . . . 6 class 2nd
116, 10cfv 5886 . . . . 5 class (2nd𝑒)
12 vx . . . . . . 7 setvar 𝑥
135cv 1481 . . . . . . . 8 class 𝑐
14 cbs 15851 . . . . . . . 8 class Base
1513, 14cfv 5886 . . . . . . 7 class (Base‘𝑐)
16 vy . . . . . . . . 9 setvar 𝑦
179cv 1481 . . . . . . . . . 10 class 𝑑
1817, 14cfv 5886 . . . . . . . . 9 class (Base‘𝑑)
1912cv 1481 . . . . . . . . . 10 class 𝑥
2016cv 1481 . . . . . . . . . 10 class 𝑦
213cv 1481 . . . . . . . . . . 11 class 𝑓
2221, 7cfv 5886 . . . . . . . . . 10 class (1st𝑓)
2319, 20, 22co 6647 . . . . . . . . 9 class (𝑥(1st𝑓)𝑦)
2416, 18, 23cmpt 4727 . . . . . . . 8 class (𝑦 ∈ (Base‘𝑑) ↦ (𝑥(1st𝑓)𝑦))
25 vz . . . . . . . . 9 setvar 𝑧
26 vg . . . . . . . . . 10 setvar 𝑔
2725cv 1481 . . . . . . . . . . 11 class 𝑧
28 chom 15946 . . . . . . . . . . . 12 class Hom
2917, 28cfv 5886 . . . . . . . . . . 11 class (Hom ‘𝑑)
3020, 27, 29co 6647 . . . . . . . . . 10 class (𝑦(Hom ‘𝑑)𝑧)
31 ccid 16320 . . . . . . . . . . . . 13 class Id
3213, 31cfv 5886 . . . . . . . . . . . 12 class (Id‘𝑐)
3319, 32cfv 5886 . . . . . . . . . . 11 class ((Id‘𝑐)‘𝑥)
3426cv 1481 . . . . . . . . . . 11 class 𝑔
3519, 20cop 4181 . . . . . . . . . . . 12 class 𝑥, 𝑦
3619, 27cop 4181 . . . . . . . . . . . 12 class 𝑥, 𝑧
3721, 10cfv 5886 . . . . . . . . . . . 12 class (2nd𝑓)
3835, 36, 37co 6647 . . . . . . . . . . 11 class (⟨𝑥, 𝑦⟩(2nd𝑓)⟨𝑥, 𝑧⟩)
3933, 34, 38co 6647 . . . . . . . . . 10 class (((Id‘𝑐)‘𝑥)(⟨𝑥, 𝑦⟩(2nd𝑓)⟨𝑥, 𝑧⟩)𝑔)
4026, 30, 39cmpt 4727 . . . . . . . . 9 class (𝑔 ∈ (𝑦(Hom ‘𝑑)𝑧) ↦ (((Id‘𝑐)‘𝑥)(⟨𝑥, 𝑦⟩(2nd𝑓)⟨𝑥, 𝑧⟩)𝑔))
4116, 25, 18, 18, 40cmpt2 6649 . . . . . . . 8 class (𝑦 ∈ (Base‘𝑑), 𝑧 ∈ (Base‘𝑑) ↦ (𝑔 ∈ (𝑦(Hom ‘𝑑)𝑧) ↦ (((Id‘𝑐)‘𝑥)(⟨𝑥, 𝑦⟩(2nd𝑓)⟨𝑥, 𝑧⟩)𝑔)))
4224, 41cop 4181 . . . . . . 7 class ⟨(𝑦 ∈ (Base‘𝑑) ↦ (𝑥(1st𝑓)𝑦)), (𝑦 ∈ (Base‘𝑑), 𝑧 ∈ (Base‘𝑑) ↦ (𝑔 ∈ (𝑦(Hom ‘𝑑)𝑧) ↦ (((Id‘𝑐)‘𝑥)(⟨𝑥, 𝑦⟩(2nd𝑓)⟨𝑥, 𝑧⟩)𝑔)))⟩
4312, 15, 42cmpt 4727 . . . . . 6 class (𝑥 ∈ (Base‘𝑐) ↦ ⟨(𝑦 ∈ (Base‘𝑑) ↦ (𝑥(1st𝑓)𝑦)), (𝑦 ∈ (Base‘𝑑), 𝑧 ∈ (Base‘𝑑) ↦ (𝑔 ∈ (𝑦(Hom ‘𝑑)𝑧) ↦ (((Id‘𝑐)‘𝑥)(⟨𝑥, 𝑦⟩(2nd𝑓)⟨𝑥, 𝑧⟩)𝑔)))⟩)
4413, 28cfv 5886 . . . . . . . . 9 class (Hom ‘𝑐)
4519, 20, 44co 6647 . . . . . . . 8 class (𝑥(Hom ‘𝑐)𝑦)
4617, 31cfv 5886 . . . . . . . . . . 11 class (Id‘𝑑)
4727, 46cfv 5886 . . . . . . . . . 10 class ((Id‘𝑑)‘𝑧)
4820, 27cop 4181 . . . . . . . . . . 11 class 𝑦, 𝑧
4936, 48, 37co 6647 . . . . . . . . . 10 class (⟨𝑥, 𝑧⟩(2nd𝑓)⟨𝑦, 𝑧⟩)
5034, 47, 49co 6647 . . . . . . . . 9 class (𝑔(⟨𝑥, 𝑧⟩(2nd𝑓)⟨𝑦, 𝑧⟩)((Id‘𝑑)‘𝑧))
5125, 18, 50cmpt 4727 . . . . . . . 8 class (𝑧 ∈ (Base‘𝑑) ↦ (𝑔(⟨𝑥, 𝑧⟩(2nd𝑓)⟨𝑦, 𝑧⟩)((Id‘𝑑)‘𝑧)))
5226, 45, 51cmpt 4727 . . . . . . 7 class (𝑔 ∈ (𝑥(Hom ‘𝑐)𝑦) ↦ (𝑧 ∈ (Base‘𝑑) ↦ (𝑔(⟨𝑥, 𝑧⟩(2nd𝑓)⟨𝑦, 𝑧⟩)((Id‘𝑑)‘𝑧))))
5312, 16, 15, 15, 52cmpt2 6649 . . . . . 6 class (𝑥 ∈ (Base‘𝑐), 𝑦 ∈ (Base‘𝑐) ↦ (𝑔 ∈ (𝑥(Hom ‘𝑐)𝑦) ↦ (𝑧 ∈ (Base‘𝑑) ↦ (𝑔(⟨𝑥, 𝑧⟩(2nd𝑓)⟨𝑦, 𝑧⟩)((Id‘𝑑)‘𝑧)))))
5443, 53cop 4181 . . . . 5 class ⟨(𝑥 ∈ (Base‘𝑐) ↦ ⟨(𝑦 ∈ (Base‘𝑑) ↦ (𝑥(1st𝑓)𝑦)), (𝑦 ∈ (Base‘𝑑), 𝑧 ∈ (Base‘𝑑) ↦ (𝑔 ∈ (𝑦(Hom ‘𝑑)𝑧) ↦ (((Id‘𝑐)‘𝑥)(⟨𝑥, 𝑦⟩(2nd𝑓)⟨𝑥, 𝑧⟩)𝑔)))⟩), (𝑥 ∈ (Base‘𝑐), 𝑦 ∈ (Base‘𝑐) ↦ (𝑔 ∈ (𝑥(Hom ‘𝑐)𝑦) ↦ (𝑧 ∈ (Base‘𝑑) ↦ (𝑔(⟨𝑥, 𝑧⟩(2nd𝑓)⟨𝑦, 𝑧⟩)((Id‘𝑑)‘𝑧)))))⟩
559, 11, 54csb 3531 . . . 4 class (2nd𝑒) / 𝑑⟨(𝑥 ∈ (Base‘𝑐) ↦ ⟨(𝑦 ∈ (Base‘𝑑) ↦ (𝑥(1st𝑓)𝑦)), (𝑦 ∈ (Base‘𝑑), 𝑧 ∈ (Base‘𝑑) ↦ (𝑔 ∈ (𝑦(Hom ‘𝑑)𝑧) ↦ (((Id‘𝑐)‘𝑥)(⟨𝑥, 𝑦⟩(2nd𝑓)⟨𝑥, 𝑧⟩)𝑔)))⟩), (𝑥 ∈ (Base‘𝑐), 𝑦 ∈ (Base‘𝑐) ↦ (𝑔 ∈ (𝑥(Hom ‘𝑐)𝑦) ↦ (𝑧 ∈ (Base‘𝑑) ↦ (𝑔(⟨𝑥, 𝑧⟩(2nd𝑓)⟨𝑦, 𝑧⟩)((Id‘𝑑)‘𝑧)))))⟩
565, 8, 55csb 3531 . . 3 class (1st𝑒) / 𝑐(2nd𝑒) / 𝑑⟨(𝑥 ∈ (Base‘𝑐) ↦ ⟨(𝑦 ∈ (Base‘𝑑) ↦ (𝑥(1st𝑓)𝑦)), (𝑦 ∈ (Base‘𝑑), 𝑧 ∈ (Base‘𝑑) ↦ (𝑔 ∈ (𝑦(Hom ‘𝑑)𝑧) ↦ (((Id‘𝑐)‘𝑥)(⟨𝑥, 𝑦⟩(2nd𝑓)⟨𝑥, 𝑧⟩)𝑔)))⟩), (𝑥 ∈ (Base‘𝑐), 𝑦 ∈ (Base‘𝑐) ↦ (𝑔 ∈ (𝑥(Hom ‘𝑐)𝑦) ↦ (𝑧 ∈ (Base‘𝑑) ↦ (𝑔(⟨𝑥, 𝑧⟩(2nd𝑓)⟨𝑦, 𝑧⟩)((Id‘𝑑)‘𝑧)))))⟩
572, 3, 4, 4, 56cmpt2 6649 . 2 class (𝑒 ∈ V, 𝑓 ∈ V ↦ (1st𝑒) / 𝑐(2nd𝑒) / 𝑑⟨(𝑥 ∈ (Base‘𝑐) ↦ ⟨(𝑦 ∈ (Base‘𝑑) ↦ (𝑥(1st𝑓)𝑦)), (𝑦 ∈ (Base‘𝑑), 𝑧 ∈ (Base‘𝑑) ↦ (𝑔 ∈ (𝑦(Hom ‘𝑑)𝑧) ↦ (((Id‘𝑐)‘𝑥)(⟨𝑥, 𝑦⟩(2nd𝑓)⟨𝑥, 𝑧⟩)𝑔)))⟩), (𝑥 ∈ (Base‘𝑐), 𝑦 ∈ (Base‘𝑐) ↦ (𝑔 ∈ (𝑥(Hom ‘𝑐)𝑦) ↦ (𝑧 ∈ (Base‘𝑑) ↦ (𝑔(⟨𝑥, 𝑧⟩(2nd𝑓)⟨𝑦, 𝑧⟩)((Id‘𝑑)‘𝑧)))))⟩)
581, 57wceq 1482 1 wff curryF = (𝑒 ∈ V, 𝑓 ∈ V ↦ (1st𝑒) / 𝑐(2nd𝑒) / 𝑑⟨(𝑥 ∈ (Base‘𝑐) ↦ ⟨(𝑦 ∈ (Base‘𝑑) ↦ (𝑥(1st𝑓)𝑦)), (𝑦 ∈ (Base‘𝑑), 𝑧 ∈ (Base‘𝑑) ↦ (𝑔 ∈ (𝑦(Hom ‘𝑑)𝑧) ↦ (((Id‘𝑐)‘𝑥)(⟨𝑥, 𝑦⟩(2nd𝑓)⟨𝑥, 𝑧⟩)𝑔)))⟩), (𝑥 ∈ (Base‘𝑐), 𝑦 ∈ (Base‘𝑐) ↦ (𝑔 ∈ (𝑥(Hom ‘𝑐)𝑦) ↦ (𝑧 ∈ (Base‘𝑑) ↦ (𝑔(⟨𝑥, 𝑧⟩(2nd𝑓)⟨𝑦, 𝑧⟩)((Id‘𝑑)‘𝑧)))))⟩)
Colors of variables: wff setvar class
This definition is referenced by:  curfval  16857
  Copyright terms: Public domain W3C validator