Definition df-pm

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 ). 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 ). See mapsspm for its relationship to set exponentiation. (Contributed by NM, 15-Nov-2007)

	Ref	Expression
Assertion	df-pm	|- ^pm = ( x e. _V , y e. _V |-> { f e. ~P ( y X. x ) | Fun f } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cpm	|- ^pm
1		vx	|- x
2		cvv	|- _V
3		vy	|- y
4		vf	|- f
5	3	cv	|- y
6	1	cv	|- x
7	5 6	cxp	|- ( y X. x )
8	7	cpw	|- ~P ( y X. x )
9	4	cv	|- f
10	9	wfun	|- Fun f
11	10 4 8	crab	|- { f e. ~P ( y X. x ) | Fun f }
12	1 3 2 2 11	cmpo	|- ( x e. _V , y e. _V |-> { f e. ~P ( y X. x ) | Fun f } )
13	0 12	wceq	|- ^pm = ( x e. _V , y e. _V |-> { f e. ~P ( y X. x ) | Fun f } )