Definition df-map 8868

Description: Define the mapping operation or set exponentiation. The set of all functions that map from 𝐵 to 𝐴 is written (𝐴 ↑_m 𝐵) (see mapval 8878). Many authors write 𝐴 followed by 𝐵 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 𝐵 as a prefixed superscript, which is read "𝐴 pre 𝐵 " (e.g., definition of [Enderton] p. 52). Definition 8.21 of [Eisenberg] p. 125 uses the notation Map(𝐵, 𝐴) for our (𝐴 ↑_m 𝐵). 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 = (𝑥 ∈ V, 𝑦 ∈ V ↦ {𝑓 ∣ 𝑓:𝑦⟶𝑥})

Distinct variable group:   𝑥,𝑦,𝑓

Detailed syntax breakdown of Definition df-map

Step	Hyp	Ref	Expression
1		cmap 8866	. 2 class ↑m
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		cvv 3480	. . 3 class V
5	3	cv 1539	. . . . 5 class 𝑦
6	2	cv 1539	. . . . 5 class 𝑥
7		vf	. . . . . 6 setvar 𝑓
8	7	cv 1539	. . . . 5 class 𝑓
9	5, 6, 8	wf 6557	. . . 4 wff 𝑓:𝑦⟶𝑥
10	9, 7	cab 2714	. . 3 class {𝑓 ∣ 𝑓:𝑦⟶𝑥}
11	2, 3, 4, 4, 10	cmpo 7433	. 2 class (𝑥 ∈ V, 𝑦 ∈ V ↦ {𝑓 ∣ 𝑓:𝑦⟶𝑥})
12	1, 11	wceq 1540	1 wff ↑m = (𝑥 ∈ V, 𝑦 ∈ V ↦ {𝑓 ∣ 𝑓:𝑦⟶𝑥})

This definition is referenced by:  fnmap  8873  reldmmap  8875  mapvalg  8876  naryfval  48549