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	$$⊢{\uparrow }_{𝑝𝑚}=\left(x\in \mathrm{V},y\in \mathrm{V}⟼\left\{f\in 𝒫\left(y\times x\right)|\mathrm{Fun}f\right\}\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cpm	$$class{\uparrow }_{𝑝𝑚}$$
1		vx	$$setvarx$$
2		cvv	$$class\mathrm{V}$$
3		vy	$$setvary$$
4		vf	$$setvarf$$
5	3	cv	$$setvary$$
6	1	cv	$$setvarx$$
7	5 6	cxp	$$class\left(y\times x\right)$$
8	7	cpw	$$class𝒫\left(y\times x\right)$$
9	4	cv	$$setvarf$$
10	9	wfun	$$wff\mathrm{Fun}f$$
11	10 4 8	crab	$$class\left\{f\in 𝒫\left(y\times x\right)|\mathrm{Fun}f\right\}$$
12	1 3 2 2 11	cmpo	$$class\left(x\in \mathrm{V},y\in \mathrm{V}⟼\left\{f\in 𝒫\left(y\times x\right)|\mathrm{Fun}f\right\}\right)$$
13	0 12	wceq	$$wff{\uparrow }_{𝑝𝑚}=\left(x\in \mathrm{V},y\in \mathrm{V}⟼\left\{f\in 𝒫\left(y\times x\right)|\mathrm{Fun}f\right\}\right)$$