NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  df-pm GIF version

Definition df-pm 6002
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 (Apm B) (see pmvalg 6010). 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 6001) . See mapsspm 6021 for its relationship to set exponentiation. (Contributed by NM, 15-Nov-2007.)
Assertion
Ref Expression
df-pm pm = (x V, y V {f (y × x) Fun f})
Distinct variable group:   x,y,f

Detailed syntax breakdown of Definition df-pm
StepHypRef Expression
1 cpm 6000 . 2 class pm
2 vx . . 3 setvar x
3 vy . . 3 setvar y
4 cvv 2859 . . 3 class V
5 vf . . . . . 6 setvar f
65cv 1641 . . . . 5 class f
76wfun 4775 . . . 4 wff Fun f
83cv 1641 . . . . . 6 class y
92cv 1641 . . . . . 6 class x
108, 9cxp 4770 . . . . 5 class (y × x)
1110cpw 3722 . . . 4 class (y × x)
127, 5, 11crab 2618 . . 3 class {f (y × x) Fun f}
132, 3, 4, 4, 12cmpt2 5653 . 2 class (x V, y V {f (y × x) Fun f})
141, 13wceq 1642 1 wff pm = (x V, y V {f (y × x) Fun f})
Colors of variables: wff setvar class
This definition is referenced by:  fnpm  6008  pmvalg  6010
  Copyright terms: Public domain W3C validator