Definition df-map 6612

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 6622). 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. (Contributed by NM, 8-Dec-2003.)

Assertion

Ref	Expression
df-map	|- ^m = ( x e. _V , y e. _V |-> { f | f : y --> x } )

Distinct variable group:   x, y, f

Detailed syntax breakdown of Definition df-map

Step	Hyp	Ref	Expression
1		cmap 6610	. 2 class ^m
2		vx	. . 3 setvar x
3		vy	. . 3 setvar y
4		cvv 2725	. . 3 class _V
5	3	cv 1342	. . . . 5 class y
6	2	cv 1342	. . . . 5 class x
7		vf	. . . . . 6 setvar f
8	7	cv 1342	. . . . 5 class f
9	5, 6, 8	wf 5183	. . . 4 wff f : y --> x
10	9, 7	cab 2151	. . 3 class { f | f : y --> x }
11	2, 3, 4, 4, 10	cmpo 5843	. 2 class ( x e. _V , y e. _V |-> { f | f : y --> x } )
12	1, 11	wceq 1343	1 wff ^m = ( x e. _V , y e. _V |-> { f | f : y --> x } )

This definition is referenced by:  fnmap  6617  reldmmap  6619  mapvalg  6620  elmapex  6631