Users' Mathboxes Mathbox for Frédéric Liné < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-cur2 Unicode version

Definition df-cur2 25197
Description: Definition of currying (2nd sort). Currying the operation 
f consists in creating a mapping that returns for every value  x of  ran  dom  f the partial application of  f to  x. (Contributed by FL, 24-Jan-2010.)
Assertion
Ref Expression
df-cur2  |-  cur2  =  { <. f ,  g
>.  |  ( Fun  f  /\  Rel  dom  f  /\  g  =  (
x  e.  ran  dom  f  |->  ( f  o.  `' ( 1st  |`  ( _V  X.  { x }
) ) ) ) ) }
Distinct variable group:    f, g, x

Detailed syntax breakdown of Definition df-cur2
StepHypRef Expression
1 ccur2 25195 . 2  class  cur2
2 vf . . . . . 6  set  f
32cv 1622 . . . . 5  class  f
43wfun 5249 . . . 4  wff  Fun  f
53cdm 4689 . . . . 5  class  dom  f
65wrel 4694 . . . 4  wff  Rel  dom  f
7 vg . . . . . 6  set  g
87cv 1622 . . . . 5  class  g
9 vx . . . . . 6  set  x
105crn 4690 . . . . . 6  class  ran  dom  f
11 c1st 6120 . . . . . . . . 9  class  1st
12 cvv 2788 . . . . . . . . . 10  class  _V
139cv 1622 . . . . . . . . . . 11  class  x
1413csn 3640 . . . . . . . . . 10  class  { x }
1512, 14cxp 4687 . . . . . . . . 9  class  ( _V 
X.  { x }
)
1611, 15cres 4691 . . . . . . . 8  class  ( 1st  |`  ( _V  X.  {
x } ) )
1716ccnv 4688 . . . . . . 7  class  `' ( 1st  |`  ( _V  X.  { x } ) )
183, 17ccom 4693 . . . . . 6  class  ( f  o.  `' ( 1st  |`  ( _V  X.  {
x } ) ) )
199, 10, 18cmpt 4077 . . . . 5  class  ( x  e.  ran  dom  f  |->  ( f  o.  `' ( 1st  |`  ( _V  X.  { x } ) ) ) )
208, 19wceq 1623 . . . 4  wff  g  =  ( x  e.  ran  dom  f  |->  ( f  o.  `' ( 1st  |`  ( _V  X.  { x }
) ) ) )
214, 6, 20w3a 934 . . 3  wff  ( Fun  f  /\  Rel  dom  f  /\  g  =  ( x  e.  ran  dom  f  |->  ( f  o.  `' ( 1st  |`  ( _V  X.  { x }
) ) ) ) )
2221, 2, 7copab 4076 . 2  class  { <. f ,  g >.  |  ( Fun  f  /\  Rel  dom  f  /\  g  =  ( x  e.  ran  dom  f  |->  ( f  o.  `' ( 1st  |`  ( _V  X.  { x }
) ) ) ) ) }
231, 22wceq 1623 1  wff  cur2  =  { <. f ,  g
>.  |  ( Fun  f  /\  Rel  dom  f  /\  g  =  (
x  e.  ran  dom  f  |->  ( f  o.  `' ( 1st  |`  ( _V  X.  { x }
) ) ) ) ) }
Colors of variables: wff set class
  Copyright terms: Public domain W3C validator