ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-pm Unicode version

Definition df-pm 6513
Description: Define the partial mapping operation. A partial function from  B to  A is a function from a subset of  B to  A. The set of all partial functions from  B to  A is written  ( A  ^pm  B ) (see pmvalg 6521). A notation for this operation apparently does not appear in the literature. We use 
^pm to distinguish it from the less general set exponentiation operation  ^m (df-map 6512) . See mapsspm 6544 for its relationship to set exponentiation. (Contributed by NM, 15-Nov-2007.)
Assertion
Ref Expression
df-pm  |-  ^pm  =  ( x  e.  _V ,  y  e.  _V  |->  { f  e.  ~P ( y  X.  x
)  |  Fun  f } )
Distinct variable group:    x, y, f

Detailed syntax breakdown of Definition df-pm
StepHypRef Expression
1 cpm 6511 . 2  class  ^pm
2 vx . . 3  setvar  x
3 vy . . 3  setvar  y
4 cvv 2660 . . 3  class  _V
5 vf . . . . . 6  setvar  f
65cv 1315 . . . . 5  class  f
76wfun 5087 . . . 4  wff  Fun  f
83cv 1315 . . . . . 6  class  y
92cv 1315 . . . . . 6  class  x
108, 9cxp 4507 . . . . 5  class  ( y  X.  x )
1110cpw 3480 . . . 4  class  ~P (
y  X.  x )
127, 5, 11crab 2397 . . 3  class  { f  e.  ~P ( y  X.  x )  |  Fun  f }
132, 3, 4, 4, 12cmpo 5744 . 2  class  ( x  e.  _V ,  y  e.  _V  |->  { f  e.  ~P ( y  X.  x )  |  Fun  f } )
141, 13wceq 1316 1  wff  ^pm  =  ( x  e.  _V ,  y  e.  _V  |->  { f  e.  ~P ( y  X.  x
)  |  Fun  f } )
Colors of variables: wff set class
This definition is referenced by:  fnpm  6518  pmvalg  6521  elpmi  6529  pmresg  6538  pmsspw  6545
  Copyright terms: Public domain W3C validator