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

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

Detailed syntax breakdown of Definition df-cur1
StepHypRef Expression
1 ccur1 25194 . 2  class  cur1
2 vf . . . . . . 7  set  f
32cv 1622 . . . . . 6  class  f
43wfun 5249 . . . . 5  wff  Fun  f
53cdm 4689 . . . . . 6  class  dom  f
65wrel 4694 . . . . 5  wff  Rel  dom  f
74, 6wa 358 . . . 4  wff  ( Fun  f  /\  Rel  dom  f )
8 vg . . . . . 6  set  g
98cv 1622 . . . . 5  class  g
10 vx . . . . . 6  set  x
115cdm 4689 . . . . . 6  class  dom  dom  f
12 c2nd 6121 . . . . . . . . 9  class  2nd
1310cv 1622 . . . . . . . . . . 11  class  x
1413csn 3640 . . . . . . . . . 10  class  { x }
15 cvv 2788 . . . . . . . . . 10  class  _V
1614, 15cxp 4687 . . . . . . . . 9  class  ( { x }  X.  _V )
1712, 16cres 4691 . . . . . . . 8  class  ( 2nd  |`  ( { x }  X.  _V ) )
1817ccnv 4688 . . . . . . 7  class  `' ( 2nd  |`  ( {
x }  X.  _V ) )
193, 18ccom 4693 . . . . . 6  class  ( f  o.  `' ( 2nd  |`  ( { x }  X.  _V ) ) )
2010, 11, 19cmpt 4077 . . . . 5  class  ( x  e.  dom  dom  f  |->  ( f  o.  `' ( 2nd  |`  ( {
x }  X.  _V ) ) ) )
219, 20wceq 1623 . . . 4  wff  g  =  ( x  e.  dom  dom  f  |->  ( f  o.  `' ( 2nd  |`  ( { x }  X.  _V ) ) ) )
227, 21wa 358 . . 3  wff  ( ( Fun  f  /\  Rel  dom  f )  /\  g  =  ( x  e. 
dom  dom  f  |->  ( f  o.  `' ( 2nd  |`  ( { x }  X.  _V ) ) ) ) )
2322, 2, 8copab 4076 . 2  class  { <. f ,  g >.  |  ( ( Fun  f  /\  Rel  dom  f )  /\  g  =  ( x  e.  dom  dom  f  |->  ( f  o.  `' ( 2nd  |`  ( {
x }  X.  _V ) ) ) ) ) }
241, 23wceq 1623 1  wff  cur1  =  { <. f ,  g
>.  |  ( ( Fun  f  /\  Rel  dom  f )  /\  g  =  ( x  e. 
dom  dom  f  |->  ( f  o.  `' ( 2nd  |`  ( { x }  X.  _V ) ) ) ) ) }
Colors of variables: wff set class
This definition is referenced by:  cur1val  25198
  Copyright terms: Public domain W3C validator