Definition df-bj-unc

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

	Ref	Expression
Assertion	df-bj-unc	⊢ uncurry_ = ( 𝑥 ∈ V , 𝑦 ∈ V , 𝑧 ∈ V ↦ ( 𝑓 ∈ ( 𝑥 Set⟶ ( 𝑦 Set⟶ 𝑧 ) ) ↦ ( 𝑎 ∈ 𝑥 , 𝑏 ∈ 𝑦 ↦ ( ( 𝑓 ‘ 𝑎 ) ‘ 𝑏 ) ) ) )

Detailed syntax breakdown

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