Definition df-map

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 ). 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 withm to distinguish it from other kinds of exponentiation. (Contributed by NM, 8-Dec-2003)

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmap	|- ^m
1		vx	|- x
2		cvv	|- _V
3		vy	|- y
4		vf	|- f
5	4	cv	|- f
6	3	cv	|- y
7	1	cv	|- x
8	6 7 5	wf	|- f : y --> x
9	8 4	cab	|- { f | f : y --> x }
10	1 3 2 2 9	cmpo	|- ( x e. _V , y e. _V |-> { f | f : y --> x } )
11	0 10	wceq	|- ^m = ( x e. _V , y e. _V |-> { f | f : y --> x } )