Definition df-bj-cur

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

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccur-	⊢ curry_
1		vx	⊢ 𝑥
2		cvv	⊢ V
3		vy	⊢ 𝑦
4		vz	⊢ 𝑧
5		vf	⊢ 𝑓
6	1	cv	⊢ 𝑥
7	3	cv	⊢ 𝑦
8	6 7	cxp	⊢ ( 𝑥 × 𝑦 )
9		csethom	⊢ Set⟶
10	4	cv	⊢ 𝑧
11	8 10 9	co	⊢ ( ( 𝑥 × 𝑦 ) Set⟶ 𝑧 )
12		va	⊢ 𝑎
13		vb	⊢ 𝑏
14	5	cv	⊢ 𝑓
15	12	cv	⊢ 𝑎
16	13	cv	⊢ 𝑏
17	15 16	cop	⊢ ⟨ 𝑎 , 𝑏 ⟩
18	17 14	cfv	⊢ ( 𝑓 ‘ ⟨ 𝑎 , 𝑏 ⟩ )
19	13 7 18	cmpt	⊢ ( 𝑏 ∈ 𝑦 ↦ ( 𝑓 ‘ ⟨ 𝑎 , 𝑏 ⟩ ) )
20	12 6 19	cmpt	⊢ ( 𝑎 ∈ 𝑥 ↦ ( 𝑏 ∈ 𝑦 ↦ ( 𝑓 ‘ ⟨ 𝑎 , 𝑏 ⟩ ) ) )
21	5 11 20	cmpt	⊢ ( 𝑓 ∈ ( ( 𝑥 × 𝑦 ) Set⟶ 𝑧 ) ↦ ( 𝑎 ∈ 𝑥 ↦ ( 𝑏 ∈ 𝑦 ↦ ( 𝑓 ‘ ⟨ 𝑎 , 𝑏 ⟩ ) ) ) )
22	1 3 4 2 2 2 21	cmpt3	⊢ ( 𝑥 ∈ V , 𝑦 ∈ V , 𝑧 ∈ V ↦ ( 𝑓 ∈ ( ( 𝑥 × 𝑦 ) Set⟶ 𝑧 ) ↦ ( 𝑎 ∈ 𝑥 ↦ ( 𝑏 ∈ 𝑦 ↦ ( 𝑓 ‘ ⟨ 𝑎 , 𝑏 ⟩ ) ) ) ) )
23	0 22	wceq	⊢ curry_ = ( 𝑥 ∈ V , 𝑦 ∈ V , 𝑧 ∈ V ↦ ( 𝑓 ∈ ( ( 𝑥 × 𝑦 ) Set⟶ 𝑧 ) ↦ ( 𝑎 ∈ 𝑥 ↦ ( 𝑏 ∈ 𝑦 ↦ ( 𝑓 ‘ ⟨ 𝑎 , 𝑏 ⟩ ) ) ) ) )