Metamath Proof Explorer 
< Previous
Next >
Nearby theorems 

Mirrors > Home > MPE Home > Th. List > dfpm  Unicode version 
Description: Define the partial mapping operation. A partial function from to is a function from a subset of to . The set of all partial functions from to is written (see pmvalg 6988). A notation for this operation apparently does not appear in the literature. We use to distinguish it from the less general set exponentiation operation (dfmap 6979) . See mapsspm 7006 for its relationship to set exponentiation. (Contributed by NM, 15Nov2007.) 
Ref  Expression 

dfpm 
Step  Hyp  Ref  Expression 

1  cpm 6978  . 2  
2  vx  . . 3  
3  vy  . . 3  
4  cvv 2916  . . 3  
5  vf  . . . . . 6  
6  5  cv 1648  . . . . 5 
7  6  wfun 5407  . . . 4 
8  3  cv 1648  . . . . . 6 
9  2  cv 1648  . . . . . 6 
10  8, 9  cxp 4835  . . . . 5 
11  10  cpw 3759  . . . 4 
12  7, 5, 11  crab 2670  . . 3 
13  2, 3, 4, 4, 12  cmpt2 6042  . 2 
14  1, 13  wceq 1649  1 
Colors of variables: wff set class 
This definition is referenced by: fnpm 6985 pmvalg 6988 
Copyright terms: Public domain  W3C validator 