ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-map Unicode version

Definition df-map 6512
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 6522). 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 with m to distinguish it from other kinds of exponentiation. (Contributed by NM, 8-Dec-2003.)
Assertion
Ref Expression
df-map  |-  ^m  =  ( x  e.  _V ,  y  e.  _V  |->  { f  |  f : y --> x }
)
Distinct variable group:    x, y, f

Detailed syntax breakdown of Definition df-map
StepHypRef Expression
1 cmap 6510 . 2  class  ^m
2 vx . . 3  setvar  x
3 vy . . 3  setvar  y
4 cvv 2660 . . 3  class  _V
53cv 1315 . . . . 5  class  y
62cv 1315 . . . . 5  class  x
7 vf . . . . . 6  setvar  f
87cv 1315 . . . . 5  class  f
95, 6, 8wf 5089 . . . 4  wff  f : y --> x
109, 7cab 2103 . . 3  class  { f  |  f : y --> x }
112, 3, 4, 4, 10cmpo 5744 . 2  class  ( x  e.  _V ,  y  e.  _V  |->  { f  |  f : y --> x } )
121, 11wceq 1316 1  wff  ^m  =  ( x  e.  _V ,  y  e.  _V  |->  { f  |  f : y --> x }
)
Colors of variables: wff set class
This definition is referenced by:  fnmap  6517  reldmmap  6519  mapvalg  6520  elmapex  6531
  Copyright terms: Public domain W3C validator