NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  df-map GIF version

Definition df-map 6001
Description: Define the mapping operation or set exponentiation. The set of all functions that map from B to A is written (Am B) (see mapval 6011). 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 (Am 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 with m to distinguish it from other kinds of exponentiation. (Contributed by NM, 15-Nov-2007.)
Assertion
Ref Expression
df-map m = (x V, y V {f f:y–→x})
Distinct variable group:   x,y,f

Detailed syntax breakdown of Definition df-map
StepHypRef Expression
1 cmap 5999 . 2 class m
2 vx . . 3 setvar x
3 vy . . 3 setvar y
4 cvv 2859 . . 3 class V
53cv 1641 . . . . 5 class y
62cv 1641 . . . . 5 class x
7 vf . . . . . 6 setvar f
87cv 1641 . . . . 5 class f
95, 6, 8wf 4777 . . . 4 wff f:y–→x
109, 7cab 2339 . . 3 class {f f:y–→x}
112, 3, 4, 4, 10cmpt2 5653 . 2 class (x V, y V {f f:y–→x})
121, 11wceq 1642 1 wff m = (x V, y V {f f:y–→x})
Colors of variables: wff setvar class
This definition is referenced by:  fnmap  6007  mapvalg  6009
  Copyright terms: Public domain W3C validator