Metamath Proof Explorer

Definition df-bj-cur

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

Ref Expression
Assertion df-bj-cur 
|- curry_ = ( x e. _V , y e. _V , z e. _V |-> ( f e. ( ( x X. y ) -Set-> z ) |-> ( a e. x |-> ( b e. y |-> ( f ` <. a , b >. ) ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccur- 
 |-  curry_
1 vx 
 |-  x
2 cvv 
 |-  _V
3 vy 
 |-  y
4 vz 
 |-  z
5 vf 
 |-  f
6 1 cv 
 |-  x
7 3 cv 
 |-  y
8 6 7 cxp 
 |-  ( x X. y )
9 csethom 
 |-  -Set->
10 4 cv 
 |-  z
11 8 10 9 co 
 |-  ( ( x X. y ) -Set-> z )
12 va 
 |-  a
13 vb 
 |-  b
14 5 cv 
 |-  f
15 12 cv 
 |-  a
16 13 cv 
 |-  b
17 15 16 cop 
 |-  <. a , b >.
18 17 14 cfv 
 |-  ( f ` <. a , b >. )
19 13 7 18 cmpt 
 |-  ( b e. y |-> ( f ` <. a , b >. ) )
20 12 6 19 cmpt 
 |-  ( a e. x |-> ( b e. y |-> ( f ` <. a , b >. ) ) )
21 5 11 20 cmpt 
 |-  ( f e. ( ( x X. y ) -Set-> z ) |-> ( a e. x |-> ( b e. y |-> ( f ` <. a , b >. ) ) ) )
22 1 3 4 2 2 2 21 cmpt3 
 |-  ( x e. _V , y e. _V , z e. _V |-> ( f e. ( ( x X. y ) -Set-> z ) |-> ( a e. x |-> ( b e. y |-> ( f ` <. a , b >. ) ) ) ) )
23 0 22 wceq 
 |-  curry_ = ( x e. _V , y e. _V , z e. _V |-> ( f e. ( ( x X. y ) -Set-> z ) |-> ( a e. x |-> ( b e. y |-> ( f ` <. a , b >. ) ) ) ) )