Detailed syntax breakdown of Definition df-curf
Step | Hyp | Ref
| Expression |
1 | | ccurf 17718 |
. 2
class
curryF |
2 | | ve |
. . 3
setvar 𝑒 |
3 | | vf |
. . 3
setvar 𝑓 |
4 | | cvv 3408 |
. . 3
class
V |
5 | | vc |
. . . 4
setvar 𝑐 |
6 | 2 | cv 1542 |
. . . . 5
class 𝑒 |
7 | | c1st 7759 |
. . . . 5
class
1st |
8 | 6, 7 | cfv 6380 |
. . . 4
class
(1st ‘𝑒) |
9 | | vd |
. . . . 5
setvar 𝑑 |
10 | | c2nd 7760 |
. . . . . 6
class
2nd |
11 | 6, 10 | cfv 6380 |
. . . . 5
class
(2nd ‘𝑒) |
12 | | vx |
. . . . . . 7
setvar 𝑥 |
13 | 5 | cv 1542 |
. . . . . . . 8
class 𝑐 |
14 | | cbs 16760 |
. . . . . . . 8
class
Base |
15 | 13, 14 | cfv 6380 |
. . . . . . 7
class
(Base‘𝑐) |
16 | | vy |
. . . . . . . . 9
setvar 𝑦 |
17 | 9 | cv 1542 |
. . . . . . . . . 10
class 𝑑 |
18 | 17, 14 | cfv 6380 |
. . . . . . . . 9
class
(Base‘𝑑) |
19 | 12 | cv 1542 |
. . . . . . . . . 10
class 𝑥 |
20 | 16 | cv 1542 |
. . . . . . . . . 10
class 𝑦 |
21 | 3 | cv 1542 |
. . . . . . . . . . 11
class 𝑓 |
22 | 21, 7 | cfv 6380 |
. . . . . . . . . 10
class
(1st ‘𝑓) |
23 | 19, 20, 22 | co 7213 |
. . . . . . . . 9
class (𝑥(1st ‘𝑓)𝑦) |
24 | 16, 18, 23 | cmpt 5135 |
. . . . . . . 8
class (𝑦 ∈ (Base‘𝑑) ↦ (𝑥(1st ‘𝑓)𝑦)) |
25 | | vz |
. . . . . . . . 9
setvar 𝑧 |
26 | | vg |
. . . . . . . . . 10
setvar 𝑔 |
27 | 25 | cv 1542 |
. . . . . . . . . . 11
class 𝑧 |
28 | | chom 16813 |
. . . . . . . . . . . 12
class
Hom |
29 | 17, 28 | cfv 6380 |
. . . . . . . . . . 11
class (Hom
‘𝑑) |
30 | 20, 27, 29 | co 7213 |
. . . . . . . . . 10
class (𝑦(Hom ‘𝑑)𝑧) |
31 | | ccid 17168 |
. . . . . . . . . . . . 13
class
Id |
32 | 13, 31 | cfv 6380 |
. . . . . . . . . . . 12
class
(Id‘𝑐) |
33 | 19, 32 | cfv 6380 |
. . . . . . . . . . 11
class
((Id‘𝑐)‘𝑥) |
34 | 26 | cv 1542 |
. . . . . . . . . . 11
class 𝑔 |
35 | 19, 20 | cop 4547 |
. . . . . . . . . . . 12
class
〈𝑥, 𝑦〉 |
36 | 19, 27 | cop 4547 |
. . . . . . . . . . . 12
class
〈𝑥, 𝑧〉 |
37 | 21, 10 | cfv 6380 |
. . . . . . . . . . . 12
class
(2nd ‘𝑓) |
38 | 35, 36, 37 | co 7213 |
. . . . . . . . . . 11
class
(〈𝑥, 𝑦〉(2nd
‘𝑓)〈𝑥, 𝑧〉) |
39 | 33, 34, 38 | co 7213 |
. . . . . . . . . 10
class
(((Id‘𝑐)‘𝑥)(〈𝑥, 𝑦〉(2nd ‘𝑓)〈𝑥, 𝑧〉)𝑔) |
40 | 26, 30, 39 | cmpt 5135 |
. . . . . . . . 9
class (𝑔 ∈ (𝑦(Hom ‘𝑑)𝑧) ↦ (((Id‘𝑐)‘𝑥)(〈𝑥, 𝑦〉(2nd ‘𝑓)〈𝑥, 𝑧〉)𝑔)) |
41 | 16, 25, 18, 18, 40 | cmpo 7215 |
. . . . . . . 8
class (𝑦 ∈ (Base‘𝑑), 𝑧 ∈ (Base‘𝑑) ↦ (𝑔 ∈ (𝑦(Hom ‘𝑑)𝑧) ↦ (((Id‘𝑐)‘𝑥)(〈𝑥, 𝑦〉(2nd ‘𝑓)〈𝑥, 𝑧〉)𝑔))) |
42 | 24, 41 | cop 4547 |
. . . . . . 7
class
〈(𝑦 ∈
(Base‘𝑑) ↦
(𝑥(1st
‘𝑓)𝑦)), (𝑦 ∈ (Base‘𝑑), 𝑧 ∈ (Base‘𝑑) ↦ (𝑔 ∈ (𝑦(Hom ‘𝑑)𝑧) ↦ (((Id‘𝑐)‘𝑥)(〈𝑥, 𝑦〉(2nd ‘𝑓)〈𝑥, 𝑧〉)𝑔)))〉 |
43 | 12, 15, 42 | cmpt 5135 |
. . . . . 6
class (𝑥 ∈ (Base‘𝑐) ↦ 〈(𝑦 ∈ (Base‘𝑑) ↦ (𝑥(1st ‘𝑓)𝑦)), (𝑦 ∈ (Base‘𝑑), 𝑧 ∈ (Base‘𝑑) ↦ (𝑔 ∈ (𝑦(Hom ‘𝑑)𝑧) ↦ (((Id‘𝑐)‘𝑥)(〈𝑥, 𝑦〉(2nd ‘𝑓)〈𝑥, 𝑧〉)𝑔)))〉) |
44 | 13, 28 | cfv 6380 |
. . . . . . . . 9
class (Hom
‘𝑐) |
45 | 19, 20, 44 | co 7213 |
. . . . . . . 8
class (𝑥(Hom ‘𝑐)𝑦) |
46 | 17, 31 | cfv 6380 |
. . . . . . . . . . 11
class
(Id‘𝑑) |
47 | 27, 46 | cfv 6380 |
. . . . . . . . . 10
class
((Id‘𝑑)‘𝑧) |
48 | 20, 27 | cop 4547 |
. . . . . . . . . . 11
class
〈𝑦, 𝑧〉 |
49 | 36, 48, 37 | co 7213 |
. . . . . . . . . 10
class
(〈𝑥, 𝑧〉(2nd
‘𝑓)〈𝑦, 𝑧〉) |
50 | 34, 47, 49 | co 7213 |
. . . . . . . . 9
class (𝑔(〈𝑥, 𝑧〉(2nd ‘𝑓)〈𝑦, 𝑧〉)((Id‘𝑑)‘𝑧)) |
51 | 25, 18, 50 | cmpt 5135 |
. . . . . . . 8
class (𝑧 ∈ (Base‘𝑑) ↦ (𝑔(〈𝑥, 𝑧〉(2nd ‘𝑓)〈𝑦, 𝑧〉)((Id‘𝑑)‘𝑧))) |
52 | 26, 45, 51 | cmpt 5135 |
. . . . . . 7
class (𝑔 ∈ (𝑥(Hom ‘𝑐)𝑦) ↦ (𝑧 ∈ (Base‘𝑑) ↦ (𝑔(〈𝑥, 𝑧〉(2nd ‘𝑓)〈𝑦, 𝑧〉)((Id‘𝑑)‘𝑧)))) |
53 | 12, 16, 15, 15, 52 | cmpo 7215 |
. . . . . 6
class (𝑥 ∈ (Base‘𝑐), 𝑦 ∈ (Base‘𝑐) ↦ (𝑔 ∈ (𝑥(Hom ‘𝑐)𝑦) ↦ (𝑧 ∈ (Base‘𝑑) ↦ (𝑔(〈𝑥, 𝑧〉(2nd ‘𝑓)〈𝑦, 𝑧〉)((Id‘𝑑)‘𝑧))))) |
54 | 43, 53 | cop 4547 |
. . . . 5
class
〈(𝑥 ∈
(Base‘𝑐) ↦
〈(𝑦 ∈
(Base‘𝑑) ↦
(𝑥(1st
‘𝑓)𝑦)), (𝑦 ∈ (Base‘𝑑), 𝑧 ∈ (Base‘𝑑) ↦ (𝑔 ∈ (𝑦(Hom ‘𝑑)𝑧) ↦ (((Id‘𝑐)‘𝑥)(〈𝑥, 𝑦〉(2nd ‘𝑓)〈𝑥, 𝑧〉)𝑔)))〉), (𝑥 ∈ (Base‘𝑐), 𝑦 ∈ (Base‘𝑐) ↦ (𝑔 ∈ (𝑥(Hom ‘𝑐)𝑦) ↦ (𝑧 ∈ (Base‘𝑑) ↦ (𝑔(〈𝑥, 𝑧〉(2nd ‘𝑓)〈𝑦, 𝑧〉)((Id‘𝑑)‘𝑧)))))〉 |
55 | 9, 11, 54 | csb 3811 |
. . . 4
class
⦋(2nd ‘𝑒) / 𝑑⦌〈(𝑥 ∈ (Base‘𝑐) ↦ 〈(𝑦 ∈ (Base‘𝑑) ↦ (𝑥(1st ‘𝑓)𝑦)), (𝑦 ∈ (Base‘𝑑), 𝑧 ∈ (Base‘𝑑) ↦ (𝑔 ∈ (𝑦(Hom ‘𝑑)𝑧) ↦ (((Id‘𝑐)‘𝑥)(〈𝑥, 𝑦〉(2nd ‘𝑓)〈𝑥, 𝑧〉)𝑔)))〉), (𝑥 ∈ (Base‘𝑐), 𝑦 ∈ (Base‘𝑐) ↦ (𝑔 ∈ (𝑥(Hom ‘𝑐)𝑦) ↦ (𝑧 ∈ (Base‘𝑑) ↦ (𝑔(〈𝑥, 𝑧〉(2nd ‘𝑓)〈𝑦, 𝑧〉)((Id‘𝑑)‘𝑧)))))〉 |
56 | 5, 8, 55 | csb 3811 |
. . 3
class
⦋(1st ‘𝑒) / 𝑐⦌⦋(2nd
‘𝑒) / 𝑑⦌〈(𝑥 ∈ (Base‘𝑐) ↦ 〈(𝑦 ∈ (Base‘𝑑) ↦ (𝑥(1st ‘𝑓)𝑦)), (𝑦 ∈ (Base‘𝑑), 𝑧 ∈ (Base‘𝑑) ↦ (𝑔 ∈ (𝑦(Hom ‘𝑑)𝑧) ↦ (((Id‘𝑐)‘𝑥)(〈𝑥, 𝑦〉(2nd ‘𝑓)〈𝑥, 𝑧〉)𝑔)))〉), (𝑥 ∈ (Base‘𝑐), 𝑦 ∈ (Base‘𝑐) ↦ (𝑔 ∈ (𝑥(Hom ‘𝑐)𝑦) ↦ (𝑧 ∈ (Base‘𝑑) ↦ (𝑔(〈𝑥, 𝑧〉(2nd ‘𝑓)〈𝑦, 𝑧〉)((Id‘𝑑)‘𝑧)))))〉 |
57 | 2, 3, 4, 4, 56 | cmpo 7215 |
. 2
class (𝑒 ∈ V, 𝑓 ∈ V ↦
⦋(1st ‘𝑒) / 𝑐⦌⦋(2nd
‘𝑒) / 𝑑⦌〈(𝑥 ∈ (Base‘𝑐) ↦ 〈(𝑦 ∈ (Base‘𝑑) ↦ (𝑥(1st ‘𝑓)𝑦)), (𝑦 ∈ (Base‘𝑑), 𝑧 ∈ (Base‘𝑑) ↦ (𝑔 ∈ (𝑦(Hom ‘𝑑)𝑧) ↦ (((Id‘𝑐)‘𝑥)(〈𝑥, 𝑦〉(2nd ‘𝑓)〈𝑥, 𝑧〉)𝑔)))〉), (𝑥 ∈ (Base‘𝑐), 𝑦 ∈ (Base‘𝑐) ↦ (𝑔 ∈ (𝑥(Hom ‘𝑐)𝑦) ↦ (𝑧 ∈ (Base‘𝑑) ↦ (𝑔(〈𝑥, 𝑧〉(2nd ‘𝑓)〈𝑦, 𝑧〉)((Id‘𝑑)‘𝑧)))))〉) |
58 | 1, 57 | wceq 1543 |
1
wff
curryF = (𝑒 ∈ V, 𝑓 ∈ V ↦
⦋(1st ‘𝑒) / 𝑐⦌⦋(2nd
‘𝑒) / 𝑑⦌〈(𝑥 ∈ (Base‘𝑐) ↦ 〈(𝑦 ∈ (Base‘𝑑) ↦ (𝑥(1st ‘𝑓)𝑦)), (𝑦 ∈ (Base‘𝑑), 𝑧 ∈ (Base‘𝑑) ↦ (𝑔 ∈ (𝑦(Hom ‘𝑑)𝑧) ↦ (((Id‘𝑐)‘𝑥)(〈𝑥, 𝑦〉(2nd ‘𝑓)〈𝑥, 𝑧〉)𝑔)))〉), (𝑥 ∈ (Base‘𝑐), 𝑦 ∈ (Base‘𝑐) ↦ (𝑔 ∈ (𝑥(Hom ‘𝑐)𝑦) ↦ (𝑧 ∈ (Base‘𝑑) ↦ (𝑔(〈𝑥, 𝑧〉(2nd ‘𝑓)〈𝑦, 𝑧〉)((Id‘𝑑)‘𝑧)))))〉) |