This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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

Detailed syntax breakdown

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