Type  Label  Description 
Statement 

Theorem  oviec 6501* 
Express an operation on equivalence classes of ordered pairs in terms of
equivalence class of operations on ordered pairs. See iset.mm for
additional comments describing the hypotheses. (Unnecessary distinct
variable restrictions were removed by David Abernethy, 4Jun2013.)
(Contributed by NM, 6Aug1995.) (Revised by Mario Carneiro,
4Jun2013.)



Theorem  ecovcom 6502* 
Lemma used to transfer a commutative law via an equivalence relation.
Most uses will want ecovicom 6503 instead. (Contributed by NM,
29Aug1995.) (Revised by David Abernethy, 4Jun2013.)



Theorem  ecovicom 6503* 
Lemma used to transfer a commutative law via an equivalence relation.
(Contributed by Jim Kingdon, 15Sep2019.)



Theorem  ecovass 6504* 
Lemma used to transfer an associative law via an equivalence relation.
In most cases ecoviass 6505 will be more useful. (Contributed by NM,
31Aug1995.) (Revised by David Abernethy, 4Jun2013.)



Theorem  ecoviass 6505* 
Lemma used to transfer an associative law via an equivalence relation.
(Contributed by Jim Kingdon, 16Sep2019.)



Theorem  ecovdi 6506* 
Lemma used to transfer a distributive law via an equivalence relation.
Most likely ecovidi 6507 will be more helpful. (Contributed by NM,
2Sep1995.) (Revised by David Abernethy, 4Jun2013.)



Theorem  ecovidi 6507* 
Lemma used to transfer a distributive law via an equivalence relation.
(Contributed by Jim Kingdon, 17Sep2019.)



2.6.25 The mapping operation


Syntax  cmap 6508 
Extend the definition of a class to include the mapping operation. (Read
for , "the set of all functions that map
from to
.)



Syntax  cpm 6509 
Extend the definition of a class to include the partial mapping operation.
(Read for , "the set of all partial functions
that map from
to .)



Definition  dfmap 6510* 
Define the mapping operation or set exponentiation. The set of all
functions that map from to is
written (see
mapval 6520). 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, 8Dec2003.)



Definition  dfpm 6511* 
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 6519). 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 6510) . See mapsspm 6542 for
its relationship to set exponentiation. (Contributed by NM,
15Nov2007.)



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



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



Theorem  mapex 6514* 
The class of all functions mapping one set to another is a set. Remark
after Definition 10.24 of [Kunen] p. 31.
(Contributed by Raph Levien,
4Dec2003.)



Theorem  fnmap 6515 
Set exponentiation has a universal domain. (Contributed by NM,
8Dec2003.) (Revised by Mario Carneiro, 8Sep2013.)



Theorem  fnpm 6516 
Partial function exponentiation has a universal domain. (Contributed by
Mario Carneiro, 14Nov2013.)



Theorem  reldmmap 6517 
Set exponentiation is a wellbehaved binary operator. (Contributed by
Stefan O'Rear, 27Feb2015.)



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



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



Theorem  mapval 6520* 
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
NM, 8Dec2003.)



Theorem  elmapg 6521 
Membership relation for set exponentiation. (Contributed by NM,
17Oct2006.) (Revised by Mario Carneiro, 15Nov2014.)



Theorem  elmapd 6522 
Deduction form of elmapg 6521. (Contributed by BJ, 11Apr2020.)



Theorem  mapdm0 6523 
The empty set is the only map with empty domain. (Contributed by Glauco
Siliprandi, 11Oct2020.) (Proof shortened by Thierry Arnoux,
3Dec2021.)



Theorem  elpmg 6524 
The predicate "is a partial function." (Contributed by Mario
Carneiro,
14Nov2013.)



Theorem  elpm2g 6525 
The predicate "is a partial function." (Contributed by NM,
31Dec2013.)



Theorem  elpm2r 6526 
Sufficient condition for being a partial function. (Contributed by NM,
31Dec2013.)



Theorem  elpmi 6527 
A partial function is a function. (Contributed by Mario Carneiro,
15Sep2015.)



Theorem  pmfun 6528 
A partial function is a function. (Contributed by Mario Carneiro,
30Jan2014.) (Revised by Mario Carneiro, 26Apr2015.)



Theorem  elmapex 6529 
Eliminate antecedent for mapping theorems: domain can be taken to be a
set. (Contributed by Stefan O'Rear, 8Oct2014.)



Theorem  elmapi 6530 
A mapping is a function, forward direction only with superfluous
antecedent removed. (Contributed by Stefan O'Rear, 10Oct2014.)



Theorem  elmapfn 6531 
A mapping is a function with the appropriate domain. (Contributed by AV,
6Apr2019.)



Theorem  elmapfun 6532 
A mapping is always a function. (Contributed by Stefan O'Rear,
9Oct2014.) (Revised by Stefan O'Rear, 5May2015.)



Theorem  elmapssres 6533 
A restricted mapping is a mapping. (Contributed by Stefan O'Rear,
9Oct2014.) (Revised by Mario Carneiro, 5May2015.)



Theorem  fpmg 6534 
A total function is a partial function. (Contributed by Mario Carneiro,
31Dec2013.)



Theorem  pmss12g 6535 
Subset relation for the set of partial functions. (Contributed by Mario
Carneiro, 31Dec2013.)



Theorem  pmresg 6536 
Elementhood of a restricted function in the set of partial functions.
(Contributed by Mario Carneiro, 31Dec2013.)



Theorem  elmap 6537 
Membership relation for set exponentiation. (Contributed by NM,
8Dec2003.)



Theorem  mapval2 6538* 
Alternate expression for the value of set exponentiation. (Contributed
by NM, 3Nov2007.)



Theorem  elpm 6539 
The predicate "is a partial function." (Contributed by NM,
15Nov2007.) (Revised by Mario Carneiro, 14Nov2013.)



Theorem  elpm2 6540 
The predicate "is a partial function." (Contributed by NM,
15Nov2007.) (Revised by Mario Carneiro, 31Dec2013.)



Theorem  fpm 6541 
A total function is a partial function. (Contributed by NM,
15Nov2007.) (Revised by Mario Carneiro, 31Dec2013.)



Theorem  mapsspm 6542 
Set exponentiation is a subset of partial maps. (Contributed by NM,
15Nov2007.) (Revised by Mario Carneiro, 27Feb2016.)



Theorem  pmsspw 6543 
Partial maps are a subset of the power set of the Cartesian product of
its arguments. (Contributed by Mario Carneiro, 2Jan2017.)



Theorem  mapsspw 6544 
Set exponentiation is a subset of the power set of the Cartesian product
of its arguments. (Contributed by NM, 8Dec2006.) (Revised by Mario
Carneiro, 26Apr2015.)



Theorem  fvmptmap 6545* 
Special case of fvmpt 5464 for operator theorems. (Contributed by NM,
27Nov2007.)



Theorem  map0e 6546 
Set exponentiation with an empty exponent (ordinal number 0) is ordinal
number 1. Exercise 4.42(a) of [Mendelson] p. 255. (Contributed by NM,
10Dec2003.) (Revised by Mario Carneiro, 30Apr2015.)



Theorem  map0b 6547 
Set exponentiation with an empty base is the empty set, provided the
exponent is nonempty. Theorem 96 of [Suppes] p. 89. (Contributed by
NM, 10Dec2003.) (Revised by Mario Carneiro, 26Apr2015.)



Theorem  map0g 6548 
Set exponentiation is empty iff the base is empty and the exponent is
not empty. Theorem 97 of [Suppes] p. 89.
(Contributed by Mario
Carneiro, 30Apr2015.)



Theorem  map0 6549 
Set exponentiation is empty iff the base is empty and the exponent is
not empty. Theorem 97 of [Suppes] p. 89.
(Contributed by NM,
10Dec2003.)



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



Theorem  mapss 6551 
Subset inheritance for set exponentiation. Theorem 99 of [Suppes]
p. 89. (Contributed by NM, 10Dec2003.) (Revised by Mario Carneiro,
26Apr2015.)



Theorem  fdiagfn 6552* 
Functionality of the diagonal map. (Contributed by Stefan O'Rear,
24Jan2015.)



Theorem  fvdiagfn 6553* 
Functionality of the diagonal map. (Contributed by Stefan O'Rear,
24Jan2015.)



Theorem  mapsnconst 6554 
Every singleton map is a constant function. (Contributed by Stefan
O'Rear, 25Mar2015.)



Theorem  mapsncnv 6555* 
Expression for the inverse of the canonical map between a set and its
set of singleton functions. (Contributed by Stefan O'Rear,
21Mar2015.)



Theorem  mapsnf1o2 6556* 
Explicit bijection between a set and its singleton functions.
(Contributed by Stefan O'Rear, 21Mar2015.)



Theorem  mapsnf1o3 6557* 
Explicit bijection in the reverse of mapsnf1o2 6556. (Contributed by
Stefan O'Rear, 24Mar2015.)



2.6.26 Infinite Cartesian products


Syntax  cixp 6558 
Extend class notation to include infinite Cartesian products.



Definition  dfixp 6559* 
Definition of infinite Cartesian product of [Enderton] p. 54. Enderton
uses a bold "X" with
written underneath or
as a subscript, as
does Stoll p. 47. Some books use a capital pi, but we will reserve that
notation for products of numbers. Usually represents a class
expression containing free and thus can be thought of as
. Normally,
is not free in ,
although this is
not a requirement of the definition. (Contributed by NM,
28Sep2006.)



Theorem  dfixp 6560* 
Eliminate the expression in dfixp 6559, under the
assumption that and are
disjoint. This way, we can say that
is bound in
even if it
appears free in .
(Contributed by Mario Carneiro, 12Aug2016.)



Theorem  ixpsnval 6561* 
The value of an infinite Cartesian product with a singleton.
(Contributed by AV, 3Dec2018.)



Theorem  elixp2 6562* 
Membership in an infinite Cartesian product. See dfixp 6559 for
discussion of the notation. (Contributed by NM, 28Sep2006.)



Theorem  fvixp 6563* 
Projection of a factor of an indexed Cartesian product. (Contributed by
Mario Carneiro, 11Jun2016.)



Theorem  ixpfn 6564* 
A nuple is a function. (Contributed by FL, 6Jun2011.) (Revised by
Mario Carneiro, 31May2014.)



Theorem  elixp 6565* 
Membership in an infinite Cartesian product. (Contributed by NM,
28Sep2006.)



Theorem  elixpconst 6566* 
Membership in an infinite Cartesian product of a constant .
(Contributed by NM, 12Apr2008.)



Theorem  ixpconstg 6567* 
Infinite Cartesian product of a constant . (Contributed by Mario
Carneiro, 11Jan2015.)



Theorem  ixpconst 6568* 
Infinite Cartesian product of a constant . (Contributed by NM,
28Sep2006.)



Theorem  ixpeq1 6569* 
Equality theorem for infinite Cartesian product. (Contributed by NM,
29Sep2006.)



Theorem  ixpeq1d 6570* 
Equality theorem for infinite Cartesian product. (Contributed by Mario
Carneiro, 11Jun2016.)



Theorem  ss2ixp 6571 
Subclass theorem for infinite Cartesian product. (Contributed by NM,
29Sep2006.) (Revised by Mario Carneiro, 12Aug2016.)



Theorem  ixpeq2 6572 
Equality theorem for infinite Cartesian product. (Contributed by NM,
29Sep2006.)



Theorem  ixpeq2dva 6573* 
Equality theorem for infinite Cartesian product. (Contributed by Mario
Carneiro, 11Jun2016.)



Theorem  ixpeq2dv 6574* 
Equality theorem for infinite Cartesian product. (Contributed by Mario
Carneiro, 11Jun2016.)



Theorem  cbvixp 6575* 
Change bound variable in an indexed Cartesian product. (Contributed by
Jeff Madsen, 20Jun2011.)



Theorem  cbvixpv 6576* 
Change bound variable in an indexed Cartesian product. (Contributed by
Jeff Madsen, 2Sep2009.)



Theorem  nfixpxy 6577* 
Boundvariable hypothesis builder for indexed Cartesian product.
(Contributed by Mario Carneiro, 15Oct2016.) (Revised by Jim Kingdon,
15Feb2023.)



Theorem  nfixp1 6578 
The index variable in an indexed Cartesian product is not free.
(Contributed by Jeff Madsen, 19Jun2011.) (Revised by Mario Carneiro,
15Oct2016.)



Theorem  ixpprc 6579* 
A cartesian product of properclass many sets is empty, because any
function in the cartesian product has to be a set with domain ,
which is not possible for a proper class domain. (Contributed by Mario
Carneiro, 25Jan2015.)



Theorem  ixpf 6580* 
A member of an infinite Cartesian product maps to the indexed union of
the product argument. Remark in [Enderton] p. 54. (Contributed by NM,
28Sep2006.)



Theorem  uniixp 6581* 
The union of an infinite Cartesian product is included in a Cartesian
product. (Contributed by NM, 28Sep2006.) (Revised by Mario Carneiro,
24Jun2015.)



Theorem  ixpexgg 6582* 
The existence of an infinite Cartesian product. is normally a
freevariable parameter in . Remark in Enderton p. 54.
(Contributed by NM, 28Sep2006.) (Revised by Jim Kingdon,
15Feb2023.)



Theorem  ixpin 6583* 
The intersection of two infinite Cartesian products. (Contributed by
Mario Carneiro, 3Feb2015.)



Theorem  ixpiinm 6584* 
The indexed intersection of a collection of infinite Cartesian products.
(Contributed by Mario Carneiro, 6Feb2015.) (Revised by Jim Kingdon,
15Feb2023.)



Theorem  ixpintm 6585* 
The intersection of a collection of infinite Cartesian products.
(Contributed by Mario Carneiro, 3Feb2015.) (Revised by Jim Kingdon,
15Feb2023.)



Theorem  ixp0x 6586 
An infinite Cartesian product with an empty index set. (Contributed by
NM, 21Sep2007.)



Theorem  ixpssmap2g 6587* 
An infinite Cartesian product is a subset of set exponentiation. This
version of ixpssmapg 6588 avoids axcoll 4011. (Contributed by Mario
Carneiro, 16Nov2014.)



Theorem  ixpssmapg 6588* 
An infinite Cartesian product is a subset of set exponentiation.
(Contributed by Jeff Madsen, 19Jun2011.)



Theorem  0elixp 6589 
Membership of the empty set in an infinite Cartesian product.
(Contributed by Steve Rodriguez, 29Sep2006.)



Theorem  ixpm 6590* 
If an infinite Cartesian product of a family is inhabited,
every is inhabited. (Contributed by Mario Carneiro,
22Jun2016.) (Revised by Jim Kingdon, 16Feb2023.)



Theorem  ixp0 6591 
The infinite Cartesian product of a family with an empty
member is empty. (Contributed by NM, 1Oct2006.) (Revised by Jim
Kingdon, 16Feb2023.)



Theorem  ixpssmap 6592* 
An infinite Cartesian product is a subset of set exponentiation. Remark
in [Enderton] p. 54. (Contributed by
NM, 28Sep2006.)



Theorem  resixp 6593* 
Restriction of an element of an infinite Cartesian product.
(Contributed by FL, 7Nov2011.) (Proof shortened by Mario Carneiro,
31May2014.)



Theorem  mptelixpg 6594* 
Condition for an explicit member of an indexed product. (Contributed by
Stefan O'Rear, 4Jan2015.)



Theorem  elixpsn 6595* 
Membership in a class of singleton functions. (Contributed by Stefan
O'Rear, 24Jan2015.)



Theorem  ixpsnf1o 6596* 
A bijection between a class and singlepoint functions to it.
(Contributed by Stefan O'Rear, 24Jan2015.)



Theorem  mapsnf1o 6597* 
A bijection between a set and singlepoint functions to it.
(Contributed by Stefan O'Rear, 24Jan2015.)



2.6.27 Equinumerosity


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



Syntax  cdom 6599 
Extend class definition to include the dominance relation (curly
lessthanorequal)



Syntax  cfn 6600 
Extend class definition to include the class of all finite sets.

