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	⊢ ↑_m = ( 𝑥 ∈ V , 𝑦 ∈ V ↦ { 𝑓 ∣ 𝑓 : 𝑦 ⟶ 𝑥 } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmap	⊢ ↑_m
1		vx	⊢ 𝑥
2		cvv	⊢ V
3		vy	⊢ 𝑦
4		vf	⊢ 𝑓
5	4	cv	⊢ 𝑓
6	3	cv	⊢ 𝑦
7	1	cv	⊢ 𝑥
8	6 7 5	wf	⊢ 𝑓 : 𝑦 ⟶ 𝑥
9	8 4	cab	⊢ { 𝑓 ∣ 𝑓 : 𝑦 ⟶ 𝑥 }
10	1 3 2 2 9	cmpo	⊢ ( 𝑥 ∈ V , 𝑦 ∈ V ↦ { 𝑓 ∣ 𝑓 : 𝑦 ⟶ 𝑥 } )
11	0 10	wceq	⊢ ↑_m = ( 𝑥 ∈ V , 𝑦 ∈ V ↦ { 𝑓 ∣ 𝑓 : 𝑦 ⟶ 𝑥 } )