Type  Label  Description 
Statement 

Definition  dfmap 6001* 
Define the mapping operation or set exponentiation. The set of all
functions that map from to is
written
(see
mapval 6011). 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
uparrow is used by Donald Knuth
for iterated exponentiation (Science 194, 12351242, 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, 15Nov2007.)



Definition  dfpm 6002* 
Define the partial mapping operation. A partial function from to
is a function
from a subset of to
. The set of all
partial functions from to is
written
(see
pmvalg 6010). A notation for this operation apparently
does not appear in
the literature. We use to distinguish it from the less general
set exponentiation operation (dfmap 6001) . See mapsspm 6021 for
its relationship to set exponentiation. (Contributed by NM,
15Nov2007.)



Theorem  mapexi 6003* 
The class of all functions mapping one set to another is a set. Remark
after Definition 10.24 of [Kunen] p. 31.
(Contributed by set.mm
contributors, 25Feb2015.)



Theorem  mapprc 6004* 
When is a proper
class, the class of all functions mapping
to is empty.
Exercise 4.41 of [Mendelson] p. 255.
(Contributed
by set.mm contributors, 8Dec2003.)



Theorem  pmex 6005* 
The class of all partial functions from one set to another is a set.
(Contributed by set.mm contributors, 15Nov2007.)



Theorem  mapex 6006* 
The class of all functions mapping one set to another is a set. Remark
after Definition 10.24 of [Kunen] p. 31.
(Contributed by set.mm
contributors, 25Feb2015.)



Theorem  fnmap 6007 
Set exponentiation has a universal domain. (Contributed by set.mm
contributors, 8Dec2003.) (Revised by set.mm contributors,
8Sep2013.) (Revised by Scott Fenton, 19Apr2019.)



Theorem  fnpm 6008 
Partial function exponentiation has a universal domain. (Contributed by
set.mm contributors, 14Nov2013.) (Revised by Scott Fenton,
19Apr2019.)



Theorem  mapvalg 6009* 
The value of set exponentiation. is the set of all
functions that map from to .
Definition 10.24 of [Kunen]
p. 24. (Contributed by set.mm contributors, 8Dec2003.) (Revised by
set.mm contributors, 8Sep2013.)



Theorem  pmvalg 6010* 
The value of the partial mapping operation.
is the set
of all partial functions that map from to . (Contributed by
set.mm contributors, 15Nov2007.) (Revised by set.mm contributors,
8Sep2013.)



Theorem  mapval 6011* 
The value of set exponentiation (inference version). is
the set of all functions that map from to . Definition
10.24 of [Kunen] p. 24. (Contributed by
set.mm contributors,
8Dec2003.)



Theorem  elmapg 6012 
Membership relation for set exponentiation. (Contributed by set.mm
contributors, 17Oct2006.)



Theorem  elpmg 6013 
The predicate "is a partial function." (Contributed by set.mm
contributors, 14Nov2013.)



Theorem  elpm2g 6014 
The predicate "is a partial function." (Contributed by set.mm
contributors, 31Dec2013.)



Theorem  pmfun 6015 
A partial function is a function. (Contributed by Mario Carneiro,
30Jan2014.)



Theorem  elmapi 6016 
A mapping is a function, forward direction only with antecedents removed.
(Contributed by set.mm contributors, 25Feb2015.)



Theorem  elmap 6017 
Membership relation for set exponentiation. (Contributed by set.mm
contributors, 8Dec2003.)



Theorem  mapval2 6018* 
Alternate expression for the value of set exponentiation. (Contributed
by set.mm contributors, 3Nov2007.)



Theorem  elpm 6019 
The predicate "is a partial function." (Contributed by set.mm
contributors, 15Nov2007.) (Revised by set.mm contributors,
14Nov2013.)



Theorem  elpm2 6020 
The predicate "is a partial function." (Contributed by set.mm
contributors, 15Nov2007.) (Revised by set.mm contributors,
31Dec2013.)



Theorem  mapsspm 6021 
Set exponentiation is a subset of partial maps. (Contributed by set.mm
contributors, 15Nov2007.)



Theorem  mapsspw 6022 
Set exponentiation is a subset of the power set of the cross product of
its arguments. (Contributed by set.mm contributors, 8Dec2006.)



Theorem  map0e 6023 
Set exponentiation with an empty exponent is the unit class of the empty
set. (Contributed by set.mm contributors, 10Dec2003.)



Theorem  map0b 6024 
Set exponentiation with an empty base is the empty set, provided the
exponent is nonempty. Theorem 96 of [Suppes] p. 89. (Contributed by
set.mm contributors, 10Dec2003.) (Revised by set.mm contributors,
19Mar2007.)



Theorem  map0 6025 
Set exponentiation is empty iff the base is empty and the exponent is
not empty. Theorem 97 of [Suppes] p. 89.
(Contributed by set.mm
contributors, 10Dec2003.) (Revised by set.mm contributors,
17May2007.)



Theorem  mapsn 6026* 
The value of set exponentiation with a singleton exponent. Theorem 98
of [Suppes] p. 89. (Contributed by
set.mm contributors,
10Dec2003.)



Theorem  mapss 6027 
Subset inheritance for set exponentiation. Theorem 99 of [Suppes]
p. 89. (Contributed by set.mm contributors, 10Dec2003.)



2.4.4 Equinumerosity


Syntax  cen 6028 
Extend class definition to include the equinumerosity relation
("approximately equals" symbol)



Definition  dfen 6029* 
Define the equinumerosity relation. Definition of [Enderton] p. 129.
We define
to be a binary relation rather than a connective, so
its arguments must be sets to be meaningful. This is acceptable because
we do not consider equinumerosity for proper classes. We derive the
usual definition as bren 6030. (Contributed by NM, 28Mar1998.)



Theorem  bren 6030* 
Equinumerosity relationship. (Contributed by SF, 23Feb2015.)



Theorem  enex 6031 
The equinumerosity relationship is a set. (Contributed by SF,
23Feb2015.)



Theorem  f1oeng 6032 
The domain and range of a onetoone, onto function are equinumerous.
(Contributed by SF, 23Feb2015.)



Theorem  f1oen 6033 
The domain and range of a onetoone, onto function are equinumerous.
(Contributed by SF, 19Jun1998.)



Theorem  enrflxg 6034 
Equinumerosity is reflexive. (Contributed by SF, 23Feb2015.)



Theorem  enrflx 6035 
Equinumerosity is reflexive. (Contributed by SF, 23Feb2015.)



Theorem  ensymi 6036 
Equinumerosity is symmetric. (Contributed by SF, 23Feb2015.)



Theorem  ensym 6037 
Equinumerosity is symmetric. (Contributed by SF, 23Feb2015.)



Theorem  entr 6038 
Equinumerosity is transitive. (Contributed by SF, 23Feb2015.)



Theorem  ener 6039 
Equinumerosity is an equivalence relationship over the universe.
(Contributed by SF, 23Feb2015.)

Er 

Theorem  idssen 6040 
Equality implies equinumerosity. (Contributed by SF, 30Apr1998.)



Theorem  dmen 6041 
The domain of equinumerosity. (Contributed by SF, 10May1998.)



Theorem  en0 6042 
The empty set is equinumerous only to itself. Exercise 1 of
[TakeutiZaring] p. 88.
(Contributed by SF, 27May1998.)



Theorem  fundmen 6043 
A function is equinumerous to its domain. Exercise 4 of [Suppes]
p. 98. (Contributed by SF, 23Feb2015.)



Theorem  fundmeng 6044 
A function is equinumerous to its domain. Exercise 4 of [Suppes]
p. 98. (Contributed by set.mm contributors, 17Sep2013.)



Theorem  cnven 6045 
A relational set is equinumerous to its converse. (Contributed by
set.mm contributors, 28Dec2014.) (Modified by Scott Fenton,
17Apr2021.)



Theorem  fndmeng 6046 
A function is equinumerate to its domain. (Contributed by Paul Chapman,
22Jun2011.)



Theorem  en2sn 6047 
Two singletons are equinumerous. (Contributed by set.mm contributors,
9Nov2003.)



Theorem  unen 6048 
Equinumerosity of union of disjoint sets. Theorem 4 of [Suppes] p. 92.
(Contributed by set.mm contributors, 11Jun1998.)



Theorem  xpsnen 6049 
A set is equinumerous to its crossproduct with a singleton.
Proposition 4.22(c) of [Mendelson] p.
254. (Contributed by set.mm
contributors, 23Feb2015.)



Theorem  xpsneng 6050 
A set is equinumerous to its crossproduct with a singleton.
Proposition 4.22(c) of [Mendelson] p.
254. (Contributed by set.mm
contributors, 22Oct2004.)



Theorem  endisj 6051* 
Any two sets are equinumerous to disjoint sets. Exercise 4.39 of
[Mendelson] p. 255. (Contributed by
set.mm contributors,
16Apr2004.)



Theorem  xpcomen 6052 
Commutative law for equinumerosity of cross product. Proposition
4.22(d) of [Mendelson] p. 254.
(Contributed by set.mm contributors,
5Jan2004.) (Revised by set.mm contributors, 23Apr2014.)



Theorem  xpcomeng 6053 
Commutative law for equinumerosity of cross product. Proposition
4.22(d) of [Mendelson] p. 254.
(Contributed by set.mm contributors,
27Mar2006.)



Theorem  xpsnen2g 6054 
A set is equinumerous to its crossproduct with a singleton on the left.
(Contributed by Stefan O'Rear, 21Nov2014.)



Theorem  xpen 6055 
Equinumerosity law for cross product. Proposition 4.22(b) of
[Mendelson] p. 254. (Contributed by
set.mm contributors, 24Jul2004.)
(Revised by set.mm contributors, 9Mar2013.)



Theorem  xpassenlem 6056 
Lemma for xpassen 6057. Compute a projection. (Contributed by
Scott
Fenton, 19Apr2021.)

Proj1 Proj1 Proj1 Proj2
Proj1
Proj1 Proj2 Proj2
Proj2 Proj2 

Theorem  xpassen 6057 
Associative law for equinumerosity of cross product. Proposition
4.22(e) of [Mendelson] p. 254.
(Contributed by SF, 24Feb2015.)



Theorem  ensn 6058 
Two singletons are equinumerous. Theorem XI.1.10 of [Rosser] p. 348.
(Contributed by SF, 25Feb2015.)



Theorem  enadjlem1 6059 
Lemma for enadj 6060. Calculate equality of differences.
(Contributed by
SF, 25Feb2015.)



Theorem  enadj 6060 
Equivalence law for adjunction. Theorem XI.1.13 of [Rosser] p. 348.
(Contributed by SF, 25Feb2015.)



Theorem  enpw1lem1 6061* 
Lemma for enpw1 6062. Set up stratification for the reverse
direction.
(Contributed by SF, 26Feb2015.)



Theorem  enpw1 6062 
Two classes are equinumerous iff their unit power classes are
equinumerous. Theorem XI.1.33 of [Rosser] p. 368. (Contributed by SF,
26Feb2015.)

_{1} _{1} 

Theorem  enmap2lem1 6063* 
Lemma for enmap2 6068. Set up stratification. (Contributed by SF,
26Feb2015.)



Theorem  enmap2lem2 6064* 
Lemma for enmap2 6068. Establish the functionhood and domain of
.
(Contributed by SF, 26Feb2015.)



Theorem  enmap2lem3 6065* 
Lemma for enmap2 6068. Binary relationship condition over .
(Contributed by SF, 26Feb2015.)



Theorem  enmap2lem4 6066* 
Lemma for enmap2 6068. The converse of is a function. (Contributed
by SF, 26Feb2015.)



Theorem  enmap2lem5 6067* 
Lemma for enmap2 6068. Calculate the range of . (Contributed by
SF, 26Feb2015.)



Theorem  enmap2 6068 
Set exponentiation preserves equinumerosity in the second argument.
Theorem XI.1.22 of [Rosser] p. 357.
(Contributed by SF,
26Feb2015.)



Theorem  enmap1lem1 6069* 
Lemma for enmap1 6074. Set up stratification. (Contributed by SF,
3Mar2015.)



Theorem  enmap1lem2 6070* 
Lemma for enmap1 6074. Establish functionhood. (Contributed by
SF,
3Mar2015.)



Theorem  enmap1lem3 6071* 
Lemma for enmap2 6068. Binary relationship condition over .
(Contributed by SF, 3Mar2015.)



Theorem  enmap1lem4 6072* 
Lemma for enmap2 6068. The converse of is a function. (Contributed
by SF, 3Mar2015.)



Theorem  enmap1lem5 6073* 
Lemma for enmap2 6068. Calculate the range of . (Contributed by
SF, 3Mar2015.)



Theorem  enmap1 6074 
Set exponentiation preserves equinumerosity in the first argument.
Theorem XI.1.23 of [Rosser] p. 357.
(Contributed by SF, 3Mar2015.)



Theorem  enpw1pw 6075 
Unit power class and power class commute within equivalence. Theorem
XI.1.35 of [Rosser] p. 368. (Contributed
by SF, 26Feb2015.)

_{1} _{1} 

Theorem  enprmaplem1 6076* 
Lemma for enprmap 6082. Set up stratification. (Contributed by SF,
3Mar2015.)



Theorem  enprmaplem2 6077* 
Lemma for enprmap 6082. Establish functionhood. (Contributed by
SF,
3Mar2015.)



Theorem  enprmaplem3 6078* 
Lemma for enprmap 6082. The converse of is a function.
(Contributed by SF, 3Mar2015.)



Theorem  enprmaplem4 6079* 
Lemma for enprmap 6082. More stratification condition setup.
(Contributed by SF, 3Mar2015.)



Theorem  enprmaplem5 6080* 
Lemma for enprmap 6082. Establish that is a subset of the range
of .
(Contributed by SF, 3Mar2015.)



Theorem  enprmaplem6 6081* 
Lemma for enprmap 6082. The range of is . (Contributed by
SF, 3Mar2015.)



Theorem  enprmap 6082 
A mapping from a two element pair onto a set is equinumerous with the
power class of the set. Theorem XI.1.28 of [Rosser] p. 360.
(Contributed by SF, 3Mar2015.)



Theorem  enprmapc 6083 
A mapping from a two element pair onto a set is equinumerous with the
power class of the set. Theorem XI.1.28 of [Rosser] p. 360.
(Contributed by SF, 3Mar2015.)



Theorem  nenpw1pwlem1 6084* 
Lemma for nenpw1pw 6086. Set up stratification. (Contributed by SF,
10Mar2015.)



Theorem  nenpw1pwlem2 6085* 
Lemma for nenpw1pw 6086. Establish the main theorem with an extra
hypothesis. (Contributed by SF, 10Mar2015.)

_{1} 

Theorem  nenpw1pw 6086 
No unit power class is equinumerous with the corresponding power class.
Theorem XI.1.6 of [Rosser] p. 347.
(Contributed by SF, 10Mar2015.)

_{1} 

Theorem  enpw 6087 
If and are equinumerous, then so
are their power sets.
Theorem XI.1.36 of [Rosser] p. 369.
(Contributed by SF,
17Mar2015.)



2.4.5 Cardinal numbers


Syntax  cncs 6088 
Extend the definition of a class to include the set of cardinal
numbers.

NC 

Syntax  clec 6089 
Extend the definition of a class to include cardinal less than or
equal.

_{c} 

Syntax  cltc 6090 
Extend the definition of a class to include cardinal strict less than.

_{c} 

Syntax  cnc 6091 
Extend the definition of a class to include the cardinality operation.

Nc 

Syntax  cmuc 6092 
Extend the definition of a class to include cardinal multiplication.

·_{c} 

Syntax  ctc 6093 
Extend the definition of a class to include cardinal type raising.

T_{c}


Syntax  c2c 6094 
Extend the definition of a class to include cardinal two.

2_{c} 

Syntax  c3c 6095 
Extend the definition of a class to include cardinal three.

3_{c} 

Syntax  cce 6096 
Extend the definition of a class to include cardinal exponentiation.

↑_{c} 

Syntax  ctcfn 6097 
Extend the definition of a class to include the stratified Traising
function.

TcFn 

Definition  dfncs 6098 
Define the set of all cardinal numbers. We define them as equivalence
classes of sets of the same size. Definition from [Rosser] p. 372.
(Contributed by Scott Fenton, 24Feb2015.)

NC 

Definition  dflec 6099* 
Define cardinal less than or equal. Definition from [Rosser] p. 375.
(Contributed by Scott Fenton, 24Feb2015.)

_{c}


Definition  dfltc 6100 
Define cardinal less than. Definition from [Rosser] p. 375. (Contributed
by Scott Fenton, 24Feb2015.)

_{c}
_{c} 