Definition df-bj-cur 34426

Description: Define currying. See also df-cur 7933. (Contributed by BJ, 11-Apr-2020.)

Assertion

Ref	Expression
df-bj-cur	⊢ curry_ = (𝑥 ∈ V, 𝑦 ∈ V, 𝑧 ∈ V ↦ (𝑓 ∈ ((𝑥 × 𝑦) Set⟶ 𝑧) ↦ (𝑎 ∈ 𝑥 ↦ (𝑏 ∈ 𝑦 ↦ (𝑓‘⟨𝑎, 𝑏⟩)))))

Distinct variable group:   𝑥,𝑦,𝑧,𝑎,𝑏,𝑓

Detailed syntax breakdown of Definition df-bj-cur

Step	Hyp	Ref	Expression
1		ccur- 34425	. 2 class curry_
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		vz	. . 3 setvar 𝑧
5		cvv 3494	. . 3 class V
6		vf	. . . 4 setvar 𝑓
7	2	cv 1536	. . . . . 6 class 𝑥
8	3	cv 1536	. . . . . 6 class 𝑦
9	7, 8	cxp 5553	. . . . 5 class (𝑥 × 𝑦)
10	4	cv 1536	. . . . 5 class 𝑧
11		csethom 34417	. . . . 5 class Set⟶
12	9, 10, 11	co 7156	. . . 4 class ((𝑥 × 𝑦) Set⟶ 𝑧)
13		va	. . . . 5 setvar 𝑎
14		vb	. . . . . 6 setvar 𝑏
15	13	cv 1536	. . . . . . . 8 class 𝑎
16	14	cv 1536	. . . . . . . 8 class 𝑏
17	15, 16	cop 4573	. . . . . . 7 class ⟨𝑎, 𝑏⟩
18	6	cv 1536	. . . . . . 7 class 𝑓
19	17, 18	cfv 6355	. . . . . 6 class (𝑓‘⟨𝑎, 𝑏⟩)
20	14, 8, 19	cmpt 5146	. . . . 5 class (𝑏 ∈ 𝑦 ↦ (𝑓‘⟨𝑎, 𝑏⟩))
21	13, 7, 20	cmpt 5146	. . . 4 class (𝑎 ∈ 𝑥 ↦ (𝑏 ∈ 𝑦 ↦ (𝑓‘⟨𝑎, 𝑏⟩)))
22	6, 12, 21	cmpt 5146	. . 3 class (𝑓 ∈ ((𝑥 × 𝑦) Set⟶ 𝑧) ↦ (𝑎 ∈ 𝑥 ↦ (𝑏 ∈ 𝑦 ↦ (𝑓‘⟨𝑎, 𝑏⟩))))
23	2, 3, 4, 5, 5, 5, 22	cmpt3 34415	. 2 class (𝑥 ∈ V, 𝑦 ∈ V, 𝑧 ∈ V ↦ (𝑓 ∈ ((𝑥 × 𝑦) Set⟶ 𝑧) ↦ (𝑎 ∈ 𝑥 ↦ (𝑏 ∈ 𝑦 ↦ (𝑓‘⟨𝑎, 𝑏⟩)))))
24	1, 23	wceq 1537	1 wff curry_ = (𝑥 ∈ V, 𝑦 ∈ V, 𝑧 ∈ V ↦ (𝑓 ∈ ((𝑥 × 𝑦) Set⟶ 𝑧) ↦ (𝑎 ∈ 𝑥 ↦ (𝑏 ∈ 𝑦 ↦ (𝑓‘⟨𝑎, 𝑏⟩)))))

This definition is referenced by: (None)