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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmap	$$class{\uparrow }_{𝑚}$$
1		vx	$$setvarx$$
2		cvv	$$class\mathrm{V}$$
3		vy	$$setvary$$
4		vf	$$setvarf$$
5	4	cv	$$setvarf$$
6	3	cv	$$setvary$$
7	1	cv	$$setvarx$$
8	6 7 5	wf	$$wfff:y⟶x$$
9	8 4	cab	$$class\left\{f|f:y⟶x\right\}$$
10	1 3 2 2 9	cmpo	$$class\left(x\in \mathrm{V},y\in \mathrm{V}⟼\left\{f|f:y⟶x\right\}\right)$$
11	0 10	wceq	$$wff{\uparrow }_{𝑚}=\left(x\in \mathrm{V},y\in \mathrm{V}⟼\left\{f|f:y⟶x\right\}\right)$$