Definition df-map 4324

Description: Define the mapping operation or set exponentiation. The set of all functions that map from B to A is written (A ^m B) (see mapval 4332). Many authors write A followed by B as a superscript for this operation and rely on context to avoid confusion other exponentiation operations (e.g. Definition 10.42 of [TakeutiZaring] p. 95). Other authors show B as a prefixed superscript, which is read "A pre B" (e.g. definition of [Enderton] p. 52). Definition 8.21 of [Eisenberg] p. 125 uses the notation Map(B, A) for our (A ^m B). The up-arrow is used by Donald Knuth for iterated exponentiation (Science 194, 1235-1242, 1976). We adopt the first case of his notation (simple exponentiation) and subscript it with m to distinguish it from other kinds of exponentiation.

Assertion

Ref	Expression
df-map	|- ^m = {<.<.x, y>., z>. | z = {f | f:y-->x}}

Distinct variable group:   x,y,z,f

Detailed syntax breakdown of Definition df-map

Step	Hyp	Ref	Expression
1		cm 4322	. 2 class ^m
2		vz	. . . . 5 set z
3	2	cv 955	. . . 4 class z
4		vy	. . . . . . 7 set y
5	4	cv 955	. . . . . 6 class y
6		vx	. . . . . . 7 set x
7	6	cv 955	. . . . . 6 class x
8		vf	. . . . . . 7 set f
9	8	cv 955	. . . . . 6 class f
10	5, 7, 9	wf 3178	. . . . 5 wff f:y-->x
11	10, 8	cab 1463	. . . 4 class {f | f:y-->x}
12	3, 11	wceq 956	. . 3 wff z = {f | f:y-->x}
13	12, 6, 4, 2	copab2 3964	. 2 class {<.<.x, y>., z>. | z = {f | f:y-->x}}
14	1, 13	wceq 956	1 wff ^m = {<.<.x, y>., z>. | z = {f | f:y-->x}}

This definition is referenced by:  fnmap 4329  mapvalg 4330

Copyright terms: Public domain