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

Definition df-map 7020
 Description: Define the mapping operation or set exponentiation. The set of all functions that map from to is written (see mapval 7030). 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
Distinct variable group:   ,,

Detailed syntax breakdown of Definition df-map
StepHypRef Expression
1 cmap 7018 . 2
2 vx . . 3
3 vy . . 3
4 cvv 2956 . . 3
53cv 1651 . . . . 5
62cv 1651 . . . . 5
7 vf . . . . . 6
87cv 1651 . . . . 5
95, 6, 8wf 5450 . . . 4
109, 7cab 2422 . . 3
112, 3, 4, 4, 10cmpt2 6083 . 2
121, 11wceq 1652 1
 Colors of variables: wff set class This definition is referenced by:  fnmap  7025  reldmmap  7027  mapvalg  7028
 Copyright terms: Public domain W3C validator