Type  Label  Description 
Statement 

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



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



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



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



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



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



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



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



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



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



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



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



Theorem  ixpprc 6613* 
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 6614* 
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 6615* 
The union of an infinite Cartesian product is included in a Cartesian
product. (Contributed by NM, 28Sep2006.) (Revised by Mario Carneiro,
24Jun2015.)



Theorem  ixpexgg 6616* 
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 6617* 
The intersection of two infinite Cartesian products. (Contributed by
Mario Carneiro, 3Feb2015.)



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



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



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



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



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



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



Theorem  ixpm 6624* 
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 6625 
The infinite Cartesian product of a family with an empty
member is empty. (Contributed by NM, 1Oct2006.) (Revised by Jim
Kingdon, 16Feb2023.)



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



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



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



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



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



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



2.6.27 Equinumerosity


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



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



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



Definition  dfen 6635* 
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 6641. (Contributed by NM, 28Mar1998.)



Definition  dfdom 6636* 
Define the dominance relation. Compare Definition of [Enderton] p. 145.
Typical textbook definitions are derived as brdom 6644 and domen 6645.
(Contributed by NM, 28Mar1998.)



Definition  dffin 6637* 
Define the (proper) class of all finite sets. Similar to Definition
10.29 of [TakeutiZaring] p. 91,
whose "Fin(a)" corresponds to
our " ". This definition is
meaningful whether or not we
accept the Axiom of Infinity axinf2 13233. (Contributed by NM,
22Aug2008.)



Theorem  relen 6638 
Equinumerosity is a relation. (Contributed by NM, 28Mar1998.)



Theorem  reldom 6639 
Dominance is a relation. (Contributed by NM, 28Mar1998.)



Theorem  encv 6640 
If two classes are equinumerous, both classes are sets. (Contributed by
AV, 21Mar2019.)



Theorem  bren 6641* 
Equinumerosity relation. (Contributed by NM, 15Jun1998.)



Theorem  brdomg 6642* 
Dominance relation. (Contributed by NM, 15Jun1998.)



Theorem  brdomi 6643* 
Dominance relation. (Contributed by Mario Carneiro, 26Apr2015.)



Theorem  brdom 6644* 
Dominance relation. (Contributed by NM, 15Jun1998.)



Theorem  domen 6645* 
Dominance in terms of equinumerosity. Example 1 of [Enderton] p. 146.
(Contributed by NM, 15Jun1998.)



Theorem  domeng 6646* 
Dominance in terms of equinumerosity, with the sethood requirement
expressed as an antecedent. Example 1 of [Enderton] p. 146.
(Contributed by NM, 24Apr2004.)



Theorem  ctex 6647 
A class dominated by is a set. See also ctfoex 7003 which says that
a countable class is a set. (Contributed by Thierry Arnoux, 29Dec2016.)
(Proof shortened by Jim Kingdon, 13Mar2023.)



Theorem  f1oen3g 6648 
The domain and range of a onetoone, onto function are equinumerous.
This variation of f1oeng 6651 does not require the Axiom of Replacement.
(Contributed by NM, 13Jan2007.) (Revised by Mario Carneiro,
10Sep2015.)



Theorem  f1oen2g 6649 
The domain and range of a onetoone, onto function are equinumerous.
This variation of f1oeng 6651 does not require the Axiom of Replacement.
(Contributed by Mario Carneiro, 10Sep2015.)



Theorem  f1dom2g 6650 
The domain of a onetoone function is dominated by its codomain. This
variation of f1domg 6652 does not require the Axiom of Replacement.
(Contributed by Mario Carneiro, 24Jun2015.)



Theorem  f1oeng 6651 
The domain and range of a onetoone, onto function are equinumerous.
(Contributed by NM, 19Jun1998.)



Theorem  f1domg 6652 
The domain of a onetoone function is dominated by its codomain.
(Contributed by NM, 4Sep2004.)



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



Theorem  f1dom 6654 
The domain of a onetoone function is dominated by its codomain.
(Contributed by NM, 19Jun1998.)



Theorem  isfi 6655* 
Express " is
finite." Definition 10.29 of [TakeutiZaring] p. 91
(whose " " is a predicate instead of a class). (Contributed by
NM, 22Aug2008.)



Theorem  enssdom 6656 
Equinumerosity implies dominance. (Contributed by NM, 31Mar1998.)



Theorem  endom 6657 
Equinumerosity implies dominance. Theorem 15 of [Suppes] p. 94.
(Contributed by NM, 28May1998.)



Theorem  enrefg 6658 
Equinumerosity is reflexive. Theorem 1 of [Suppes] p. 92. (Contributed
by NM, 18Jun1998.) (Revised by Mario Carneiro, 26Apr2015.)



Theorem  enref 6659 
Equinumerosity is reflexive. Theorem 1 of [Suppes] p. 92. (Contributed
by NM, 25Sep2004.)



Theorem  eqeng 6660 
Equality implies equinumerosity. (Contributed by NM, 26Oct2003.)



Theorem  domrefg 6661 
Dominance is reflexive. (Contributed by NM, 18Jun1998.)



Theorem  en2d 6662* 
Equinumerosity inference from an implicit onetoone onto function.
(Contributed by NM, 27Jul2004.) (Revised by Mario Carneiro,
12May2014.)



Theorem  en3d 6663* 
Equinumerosity inference from an implicit onetoone onto function.
(Contributed by NM, 27Jul2004.) (Revised by Mario Carneiro,
12May2014.)



Theorem  en2i 6664* 
Equinumerosity inference from an implicit onetoone onto function.
(Contributed by NM, 4Jan2004.)



Theorem  en3i 6665* 
Equinumerosity inference from an implicit onetoone onto function.
(Contributed by NM, 19Jul2004.)



Theorem  dom2lem 6666* 
A mapping (first hypothesis) that is onetoone (second hypothesis)
implies its domain is dominated by its codomain. (Contributed by NM,
24Jul2004.)



Theorem  dom2d 6667* 
A mapping (first hypothesis) that is onetoone (second hypothesis)
implies its domain is dominated by its codomain. (Contributed by NM,
24Jul2004.) (Revised by Mario Carneiro, 20May2013.)



Theorem  dom3d 6668* 
A mapping (first hypothesis) that is onetoone (second hypothesis)
implies its domain is dominated by its codomain. (Contributed by Mario
Carneiro, 20May2013.)



Theorem  dom2 6669* 
A mapping (first hypothesis) that is onetoone (second hypothesis)
implies its domain is dominated by its codomain. and can be
read and , as can be inferred from their
distinct variable conditions. (Contributed by NM, 26Oct2003.)



Theorem  dom3 6670* 
A mapping (first hypothesis) that is onetoone (second hypothesis)
implies its domain is dominated by its codomain. and can be
read and , as can be inferred from their
distinct variable conditions. (Contributed by Mario Carneiro,
20May2013.)



Theorem  idssen 6671 
Equality implies equinumerosity. (Contributed by NM, 30Apr1998.)
(Revised by Mario Carneiro, 15Nov2014.)



Theorem  ssdomg 6672 
A set dominates its subsets. Theorem 16 of [Suppes] p. 94. (Contributed
by NM, 19Jun1998.) (Revised by Mario Carneiro, 24Jun2015.)



Theorem  ener 6673 
Equinumerosity is an equivalence relation. (Contributed by NM,
19Mar1998.) (Revised by Mario Carneiro, 15Nov2014.)



Theorem  ensymb 6674 
Symmetry of equinumerosity. Theorem 2 of [Suppes] p. 92. (Contributed by
Mario Carneiro, 26Apr2015.)



Theorem  ensym 6675 
Symmetry of equinumerosity. Theorem 2 of [Suppes] p. 92. (Contributed by
NM, 26Oct2003.) (Revised by Mario Carneiro, 26Apr2015.)



Theorem  ensymi 6676 
Symmetry of equinumerosity. Theorem 2 of [Suppes] p. 92. (Contributed
by NM, 25Sep2004.)



Theorem  ensymd 6677 
Symmetry of equinumerosity. Deduction form of ensym 6675. (Contributed
by David Moews, 1May2017.)



Theorem  entr 6678 
Transitivity of equinumerosity. Theorem 3 of [Suppes] p. 92.
(Contributed by NM, 9Jun1998.)



Theorem  domtr 6679 
Transitivity of dominance relation. Theorem 17 of [Suppes] p. 94.
(Contributed by NM, 4Jun1998.) (Revised by Mario Carneiro,
15Nov2014.)



Theorem  entri 6680 
A chained equinumerosity inference. (Contributed by NM,
25Sep2004.)



Theorem  entr2i 6681 
A chained equinumerosity inference. (Contributed by NM,
25Sep2004.)



Theorem  entr3i 6682 
A chained equinumerosity inference. (Contributed by NM,
25Sep2004.)



Theorem  entr4i 6683 
A chained equinumerosity inference. (Contributed by NM,
25Sep2004.)



Theorem  endomtr 6684 
Transitivity of equinumerosity and dominance. (Contributed by NM,
7Jun1998.)



Theorem  domentr 6685 
Transitivity of dominance and equinumerosity. (Contributed by NM,
7Jun1998.)



Theorem  f1imaeng 6686 
A onetoone function's image under a subset of its domain is equinumerous
to the subset. (Contributed by Mario Carneiro, 15May2015.)



Theorem  f1imaen2g 6687 
A onetoone function's image under a subset of its domain is equinumerous
to the subset. (This version of f1imaen 6688 does not need axsetind 4452.)
(Contributed by Mario Carneiro, 16Nov2014.) (Revised by Mario Carneiro,
25Jun2015.)



Theorem  f1imaen 6688 
A onetoone function's image under a subset of its domain is
equinumerous to the subset. (Contributed by NM, 30Sep2004.)



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



Theorem  ensn1 6690 
A singleton is equinumerous to ordinal one. (Contributed by NM,
4Nov2002.)



Theorem  ensn1g 6691 
A singleton is equinumerous to ordinal one. (Contributed by NM,
23Apr2004.)



Theorem  enpr1g 6692 
has only
one element. (Contributed by FL, 15Feb2010.)



Theorem  en1 6693* 
A set is equinumerous to ordinal one iff it is a singleton.
(Contributed by NM, 25Jul2004.)



Theorem  en1bg 6694 
A set is equinumerous to ordinal one iff it is a singleton.
(Contributed by Jim Kingdon, 13Apr2020.)



Theorem  reuen1 6695* 
Two ways to express "exactly one". (Contributed by Stefan O'Rear,
28Oct2014.)



Theorem  euen1 6696 
Two ways to express "exactly one". (Contributed by Stefan O'Rear,
28Oct2014.)



Theorem  euen1b 6697* 
Two ways to express " has a unique element". (Contributed by
Mario Carneiro, 9Apr2015.)



Theorem  en1uniel 6698 
A singleton contains its sole element. (Contributed by Stefan O'Rear,
16Aug2015.)



Theorem  2dom 6699* 
A set that dominates ordinal 2 has at least 2 different members.
(Contributed by NM, 25Jul2004.)



Theorem  fundmen 6700 
A function is equinumerous to its domain. Exercise 4 of [Suppes] p. 98.
(Contributed by NM, 28Jul2004.) (Revised by Mario Carneiro,
15Nov2014.)

