Definition df-pm 4331

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 4337). 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 4330) . See mapsspm 4345 for its relationship to set exponentiation.

Assertion

Ref	Expression
df-pm	|- ^pm = {<.<.x, y>., z>. | z = {f | (Fun f /\ f (_ (y X. x))}}

Distinct variable group:   x,y,z,f

Detailed syntax breakdown of Definition df-pm

Step	Hyp	Ref	Expression
1		cpm 4329	. 2 class ^pm
2		vz	. . . . 5 set z
3	2	cv 957	. . . 4 class z
4		vf	. . . . . . . 8 set f
5	4	cv 957	. . . . . . 7 class f
6	5	wfun 3182	. . . . . 6 wff Fun f
7		vy	. . . . . . . . 9 set y
8	7	cv 957	. . . . . . . 8 class y
9		vx	. . . . . . . . 9 set x
10	9	cv 957	. . . . . . . 8 class x
11	8, 10	cxp 3174	. . . . . . 7 class (y X. x)
12	5, 11	wss 2050	. . . . . 6 wff f (_ (y X. x)
13	6, 12	wa 223	. . . . 5 wff (Fun f /\ f (_ (y X. x))
14	13, 4	cab 1466	. . . 4 class {f | (Fun f /\ f (_ (y X. x))}
15	3, 14	wceq 958	. . 3 wff z = {f | (Fun f /\ f (_ (y X. x))}
16	15, 9, 7, 2	copab2 3970	. 2 class {<.<.x, y>., z>. | z = {f | (Fun f /\ f (_ (y X. x))}}
17	1, 16	wceq 958	1 wff ^pm = {<.<.x, y>., z>. | z = {f | (Fun f /\ f (_ (y X. x))}}

This definition is referenced by:  pmvalg 4337

Copyright terms: Public domain