Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-map Structured version   Visualization version   GIF version

Definition df-map 7746
 Description: Define the mapping operation or set exponentiation. The set of all functions that map from 𝐵 to 𝐴 is written (𝐴 ↑𝑚 𝐵) (see mapval 7756). 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 (𝐴 ↑𝑚 𝐵). 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 𝑚 = (𝑥 ∈ V, 𝑦 ∈ V ↦ {𝑓𝑓:𝑦𝑥})
Distinct variable group:   𝑥,𝑦,𝑓

Detailed syntax breakdown of Definition df-map
StepHypRef Expression
1 cmap 7744 . 2 class 𝑚
2 vx . . 3 setvar 𝑥
3 vy . . 3 setvar 𝑦
4 cvv 3173 . . 3 class V
53cv 1474 . . . . 5 class 𝑦
62cv 1474 . . . . 5 class 𝑥
7 vf . . . . . 6 setvar 𝑓
87cv 1474 . . . . 5 class 𝑓
95, 6, 8wf 5800 . . . 4 wff 𝑓:𝑦𝑥
109, 7cab 2596 . . 3 class {𝑓𝑓:𝑦𝑥}
112, 3, 4, 4, 10cmpt2 6551 . 2 class (𝑥 ∈ V, 𝑦 ∈ V ↦ {𝑓𝑓:𝑦𝑥})
121, 11wceq 1475 1 wff 𝑚 = (𝑥 ∈ V, 𝑦 ∈ V ↦ {𝑓𝑓:𝑦𝑥})
 Colors of variables: wff setvar class This definition is referenced by:  fnmap  7751  reldmmap  7753  mapvalg  7754
 Copyright terms: Public domain W3C validator