Type  Label  Description 
Statement 

Theorem  xpdom2 6501 
Dominance law for Cartesian product. Proposition 10.33(2) of
[TakeutiZaring] p. 92.
(Contributed by NM, 24Jul2004.) (Revised by
Mario Carneiro, 15Nov2014.)



Theorem  xpdom2g 6502 
Dominance law for Cartesian product. Theorem 6L(c) of [Enderton]
p. 149. (Contributed by Mario Carneiro, 26Apr2015.)



Theorem  xpdom1g 6503 
Dominance law for Cartesian product. Theorem 6L(c) of [Enderton]
p. 149. (Contributed by NM, 25Mar2006.) (Revised by Mario Carneiro,
26Apr2015.)



Theorem  xpdom3m 6504* 
A set is dominated by its Cartesian product with an inhabited set.
Exercise 6 of [Suppes] p. 98.
(Contributed by Jim Kingdon,
15Apr2020.)



Theorem  xpdom1 6505 
Dominance law for Cartesian product. Theorem 6L(c) of [Enderton]
p. 149. (Contributed by NM, 28Sep2004.) (Revised by NM,
29Mar2006.) (Revised by Mario Carneiro, 7May2015.)



Theorem  fopwdom 6506 
Covering implies injection on power sets. (Contributed by Stefan
O'Rear, 6Nov2014.) (Revised by Mario Carneiro, 24Jun2015.)



Theorem  0domg 6507 
Any set dominates the empty set. (Contributed by NM, 26Oct2003.)
(Revised by Mario Carneiro, 26Apr2015.)



Theorem  dom0 6508 
A set dominated by the empty set is empty. (Contributed by NM,
22Nov2004.)



Theorem  0dom 6509 
Any set dominates the empty set. (Contributed by NM, 26Oct2003.)
(Revised by Mario Carneiro, 26Apr2015.)



Theorem  enen1 6510 
Equalitylike theorem for equinumerosity. (Contributed by NM,
18Dec2003.)



Theorem  enen2 6511 
Equalitylike theorem for equinumerosity. (Contributed by NM,
18Dec2003.)



Theorem  domen1 6512 
Equalitylike theorem for equinumerosity and dominance. (Contributed by
NM, 8Nov2003.)



Theorem  domen2 6513 
Equalitylike theorem for equinumerosity and dominance. (Contributed by
NM, 8Nov2003.)



2.6.27 Equinumerosity (cont.)


Theorem  xpf1o 6514* 
Construct a bijection on a Cartesian product given bijections on the
factors. (Contributed by Mario Carneiro, 30May2015.)



Theorem  xpen 6515 
Equinumerosity law for Cartesian product. Proposition 4.22(b) of
[Mendelson] p. 254. (Contributed by
NM, 24Jul2004.)



Theorem  mapen 6516 
Two set exponentiations are equinumerous when their bases and exponents
are equinumerous. Theorem 6H(c) of [Enderton] p. 139. (Contributed by
NM, 16Dec2003.) (Proof shortened by Mario Carneiro, 26Apr2015.)



Theorem  mapdom1g 6517 
Orderpreserving property of set exponentiation. (Contributed by Jim
Kingdon, 15Jul2022.)



Theorem  mapxpen 6518 
Equinumerosity law for double set exponentiation. Proposition 10.45 of
[TakeutiZaring] p. 96.
(Contributed by NM, 21Feb2004.) (Revised by
Mario Carneiro, 24Jun2015.)



Theorem  xpmapenlem 6519* 
Lemma for xpmapen 6520. (Contributed by NM, 1May2004.) (Revised
by
Mario Carneiro, 16Nov2014.)



Theorem  xpmapen 6520 
Equinumerosity law for set exponentiation of a Cartesian product.
Exercise 4.47 of [Mendelson] p. 255.
(Contributed by NM, 23Feb2004.)
(Proof shortened by Mario Carneiro, 16Nov2014.)



Theorem  ssenen 6521* 
Equinumerosity of equinumerous subsets of a set. (Contributed by NM,
30Sep2004.) (Revised by Mario Carneiro, 16Nov2014.)



2.6.28 Pigeonhole Principle


Theorem  phplem1 6522 
Lemma for Pigeonhole Principle. If we join a natural number to itself
minus an element, we end up with its successor minus the same element.
(Contributed by NM, 25May1998.)



Theorem  phplem2 6523 
Lemma for Pigeonhole Principle. A natural number is equinumerous to its
successor minus one of its elements. (Contributed by NM, 11Jun1998.)
(Revised by Mario Carneiro, 16Nov2014.)



Theorem  phplem3 6524 
Lemma for Pigeonhole Principle. A natural number is equinumerous to its
successor minus any element of the successor. For a version without the
redundant hypotheses, see phplem3g 6526. (Contributed by NM,
26May1998.)



Theorem  phplem4 6525 
Lemma for Pigeonhole Principle. Equinumerosity of successors implies
equinumerosity of the original natural numbers. (Contributed by NM,
28May1998.) (Revised by Mario Carneiro, 24Jun2015.)



Theorem  phplem3g 6526 
A natural number is equinumerous to its successor minus any element of
the successor. Version of phplem3 6524 with unnecessary hypotheses
removed. (Contributed by Jim Kingdon, 1Sep2021.)



Theorem  nneneq 6527 
Two equinumerous natural numbers are equal. Proposition 10.20 of
[TakeutiZaring] p. 90 and its
converse. Also compare Corollary 6E of
[Enderton] p. 136. (Contributed by NM,
28May1998.)



Theorem  php5 6528 
A natural number is not equinumerous to its successor. Corollary
10.21(1) of [TakeutiZaring] p. 90.
(Contributed by NM, 26Jul2004.)



Theorem  snnen2og 6529 
A singleton is never equinumerous with the ordinal
number 2. If
is a proper
class, see snnen2oprc 6530. (Contributed by Jim Kingdon,
1Sep2021.)



Theorem  snnen2oprc 6530 
A singleton is never equinumerous with the ordinal
number 2. If
is a set, see snnen2og 6529. (Contributed by Jim Kingdon,
1Sep2021.)



Theorem  1nen2 6531 
One and two are not equinumerous. (Contributed by Jim Kingdon,
25Jan2022.)



Theorem  phplem4dom 6532 
Dominance of successors implies dominance of the original natural
numbers. (Contributed by Jim Kingdon, 1Sep2021.)



Theorem  php5dom 6533 
A natural number does not dominate its successor. (Contributed by Jim
Kingdon, 1Sep2021.)



Theorem  nndomo 6534 
Cardinal ordering agrees with natural number ordering. Example 3 of
[Enderton] p. 146. (Contributed by NM,
17Jun1998.)



Theorem  phpm 6535* 
Pigeonhole Principle. A natural number is not equinumerous to a proper
subset of itself. By "proper subset" here we mean that there
is an
element which is in the natural number and not in the subset, or in
symbols (which is stronger than not being equal
in the absence of excluded middle). Theorem (Pigeonhole Principle) of
[Enderton] p. 134. The theorem is
socalled because you can't put n +
1 pigeons into n holes (if each hole holds only one pigeon). The
proof consists of lemmas phplem1 6522 through phplem4 6525, nneneq 6527, and
this final piece of the proof. (Contributed by NM, 29May1998.)



Theorem  phpelm 6536 
Pigeonhole Principle. A natural number is not equinumerous to an
element of itself. (Contributed by Jim Kingdon, 6Sep2021.)



Theorem  phplem4on 6537 
Equinumerosity of successors of an ordinal and a natural number implies
equinumerosity of the originals. (Contributed by Jim Kingdon,
5Sep2021.)



2.6.29 Finite sets


Theorem  fict 6538 
A finite set is countable. (Contributed by Thierry Arnoux,
27Mar2018.)



Theorem  fidceq 6539 
Equality of members of a finite set is decidable. This may be
counterintuitive: cannot any two sets be elements of a finite set?
Well, to show, for example, that is finite would require
showing it is equinumerous to or to but to show that you'd
need to know
or , respectively.
(Contributed by
Jim Kingdon, 5Sep2021.)

DECID 

Theorem  fidifsnen 6540 
All decrements of a finite set are equinumerous. (Contributed by Jim
Kingdon, 9Sep2021.)



Theorem  fidifsnid 6541 
If we remove a single element from a finite set then put it back in, we
end up with the original finite set. This strengthens difsnss 3568 from
subset to equality when the set is finite. (Contributed by Jim Kingdon,
9Sep2021.)



Theorem  nnfi 6542 
Natural numbers are finite sets. (Contributed by Stefan O'Rear,
21Mar2015.)



Theorem  enfi 6543 
Equinumerous sets have the same finiteness. (Contributed by NM,
22Aug2008.)



Theorem  enfii 6544 
A set equinumerous to a finite set is finite. (Contributed by Mario
Carneiro, 12Mar2015.)



Theorem  ssfilem 6545* 
Lemma for ssfiexmid 6546. (Contributed by Jim Kingdon, 3Feb2022.)



Theorem  ssfiexmid 6546* 
If any subset of a finite set is finite, excluded middle follows. One
direction of Theorem 2.1 of [Bauer], p.
485. (Contributed by Jim
Kingdon, 19May2020.)



Theorem  infiexmid 6547* 
If the intersection of any finite set and any other set is finite,
excluded middle follows. (Contributed by Jim Kingdon, 5Feb2022.)



Theorem  domfiexmid 6548* 
If any set dominated by a finite set is finite, excluded middle follows.
(Contributed by Jim Kingdon, 3Feb2022.)



Theorem  dif1en 6549 
If a set is
equinumerous to the successor of a natural number
, then with an element removed is
equinumerous to .
(Contributed by Jeff Madsen, 2Sep2009.) (Revised by Stefan O'Rear,
16Aug2015.)



Theorem  dif1enen 6550 
Subtracting one element from each of two equinumerous finite sets.
(Contributed by Jim Kingdon, 5Jun2022.)



Theorem  fiunsnnn 6551 
Adding one element to a finite set which is equinumerous to a natural
number. (Contributed by Jim Kingdon, 13Sep2021.)



Theorem  php5fin 6552 
A finite set is not equinumerous to a set which adds one element.
(Contributed by Jim Kingdon, 13Sep2021.)



Theorem  fisbth 6553 
SchroederBernstein Theorem for finite sets. (Contributed by Jim
Kingdon, 12Sep2021.)



Theorem  0fin 6554 
The empty set is finite. (Contributed by FL, 14Jul2008.)



Theorem  fin0 6555* 
A nonempty finite set has at least one element. (Contributed by Jim
Kingdon, 10Sep2021.)



Theorem  fin0or 6556* 
A finite set is either empty or inhabited. (Contributed by Jim Kingdon,
30Sep2021.)



Theorem  diffitest 6557* 
If subtracting any set from a finite set gives a finite set, any
proposition of the form is
decidable. This is not a proof of
full excluded middle, but it is close enough to show we won't be able to
prove . (Contributed by Jim
Kingdon,
8Sep2021.)



Theorem  findcard 6558* 
Schema for induction on the cardinality of a finite set. The inductive
hypothesis is that the result is true on the given set with any one
element removed. The result is then proven to be true for all finite
sets. (Contributed by Jeff Madsen, 2Sep2009.)



Theorem  findcard2 6559* 
Schema for induction on the cardinality of a finite set. The inductive
step shows that the result is true if one more element is added to the
set. The result is then proven to be true for all finite sets.
(Contributed by Jeff Madsen, 8Jul2010.)



Theorem  findcard2s 6560* 
Variation of findcard2 6559 requiring that the element added in the
induction step not be a member of the original set. (Contributed by
Paul Chapman, 30Nov2012.)



Theorem  findcard2d 6561* 
Deduction version of findcard2 6559. If you also need
(which
doesn't come for free due to ssfiexmid 6546), use findcard2sd 6562 instead.
(Contributed by SO, 16Jul2018.)



Theorem  findcard2sd 6562* 
Deduction form of finite set induction . (Contributed by Jim Kingdon,
14Sep2021.)



Theorem  diffisn 6563 
Subtracting a singleton from a finite set produces a finite set.
(Contributed by Jim Kingdon, 11Sep2021.)



Theorem  diffifi 6564 
Subtracting one finite set from another produces a finite set.
(Contributed by Jim Kingdon, 8Sep2021.)



Theorem  infnfi 6565 
An infinite set is not finite. (Contributed by Jim Kingdon,
20Feb2022.)



Theorem  ominf 6566 
The set of natural numbers is not finite. Although we supply this theorem
because we can, the more natural way to express " is infinite" is
which is an instance
of domrefg 6438. (Contributed by NM,
2Jun1998.)



Theorem  isinfinf 6567* 
An infinite set contains subsets of arbitrarily large finite
cardinality. (Contributed by Jim Kingdon, 15Jun2022.)



Theorem  ac6sfi 6568* 
Existence of a choice function for finite sets. (Contributed by Jeff
Hankins, 26Jun2009.) (Proof shortened by Mario Carneiro,
29Jan2014.)



Theorem  tridc 6569* 
A trichotomous order is decidable. (Contributed by Jim Kingdon,
5Sep2022.)

DECID 

Theorem  fimax2gtrilemstep 6570* 
Lemma for fimax2gtri 6571. The induction step. (Contributed by Jim
Kingdon, 5Sep2022.)



Theorem  fimax2gtri 6571* 
A finite set has a maximum under a trichotomous order. (Contributed
by Jim Kingdon, 5Sep2022.)



Theorem  finexdc 6572* 
Decidability of existence, over a finite set and defined by a decidable
proposition. (Contributed by Jim Kingdon, 12Jul2022.)

DECID DECID 

Theorem  dfrex2fin 6573* 
Relationship between universal and existential quantifiers over a finite
set. Remark in Section 2.2.1 of [Pierik], p. 8. Although Pierik does
not mention the decidability condition explicitly, it does say
"only
finitely many x to check" which means there must be some way of
checking
each value of x. (Contributed by Jim Kingdon, 11Jul2022.)

DECID


Theorem  infm 6574* 
An infinite set is inhabited. (Contributed by Jim Kingdon,
18Feb2022.)



Theorem  infn0 6575 
An infinite set is not empty. (Contributed by NM, 23Oct2004.)



Theorem  inffiexmid 6576* 
If any given set is either finite or infinite, excluded middle follows.
(Contributed by Jim Kingdon, 15Jun2022.)



Theorem  en2eqpr 6577 
Building a set with two elements. (Contributed by FL, 11Aug2008.)
(Revised by Mario Carneiro, 10Sep2015.)



Theorem  exmidpw 6578 
Excluded middle is equivalent to the power set of having two
elements. Remark of [PradicBrown2022], p. 2. (Contributed by
Jim
Kingdon, 30Jun2022.)

EXMID


Theorem  fientri3 6579 
Trichotomy of dominance for finite sets. (Contributed by Jim Kingdon,
15Sep2021.)



Theorem  nnwetri 6580* 
A natural number is wellordered by . More specifically, this
order both satisfies and is trichotomous. (Contributed by Jim
Kingdon, 25Sep2021.)



Theorem  onunsnss 6581 
Adding a singleton to create an ordinal. (Contributed by Jim Kingdon,
20Oct2021.)



Theorem  unfiexmid 6582* 
If the union of any two finite sets is finite, excluded middle follows.
Remark 8.1.17 of [AczelRathjen], p.
74. (Contributed by Mario Carneiro
and Jim Kingdon, 5Mar2022.)



Theorem  unsnfi 6583 
Adding a singleton to a finite set yields a finite set. (Contributed by
Jim Kingdon, 3Feb2022.)



Theorem  unsnfidcex 6584 
The condition in unsnfi 6583. This is intended to show that
unsnfi 6583 without that condition would not be provable
but it probably
would need to be strengthened (for example, to imply included middle) to
fully show that. (Contributed by Jim Kingdon, 6Feb2022.)

DECID 

Theorem  unsnfidcel 6585 
The condition in unsnfi 6583. This is intended to show that
unsnfi 6583 without that condition would not be provable
but it probably
would need to be strengthened (for example, to imply included middle) to
fully show that. (Contributed by Jim Kingdon, 6Feb2022.)

DECID 

Theorem  unfidisj 6586 
The union of two disjoint finite sets is finite. (Contributed by Jim
Kingdon, 25Feb2022.)



Theorem  undifdcss 6587* 
Union of complementary parts into whole and decidability. (Contributed
by Jim Kingdon, 17Jun2022.)

DECID 

Theorem  undifdc 6588* 
Union of complementary parts into whole. This is a case where we can
strengthen undifss 3350 from subset to equality. (Contributed by Jim
Kingdon, 17Jun2022.)

DECID


Theorem  undiffi 6589 
Union of complementary parts into whole. This is a case where we can
strengthen undifss 3350 from subset to equality. (Contributed by Jim
Kingdon, 2Mar2022.)



Theorem  unfiin 6590 
The union of two finite sets is finite if their intersection is.
(Contributed by Jim Kingdon, 2Mar2022.)



Theorem  prfidisj 6591 
A pair is finite if it consists of two unequal sets. For the case where
, see snfig 6485. For the cases where one or both is
a proper
class, see prprc1 3535, prprc2 3536, or prprc 3537. (Contributed by Jim
Kingdon, 31May2022.)



Theorem  tpfidisj 6592 
A triple is finite if it consists of three unequal sets. (Contributed
by Jim Kingdon, 1Oct2022.)



Theorem  xpfi 6593 
The Cartesian product of two finite sets is finite. Lemma 8.1.16 of
[AczelRathjen], p. 74.
(Contributed by Jeff Madsen, 2Sep2009.)
(Revised by Mario Carneiro, 12Mar2015.)



Theorem  3xpfi 6594 
The Cartesian product of three finite sets is a finite set. (Contributed
by Alexander van der Vekens, 11Mar2018.)



Theorem  fisseneq 6595 
A finite set is equal to its subset if they are equinumerous.
(Contributed by FL, 11Aug2008.)



Theorem  ssfirab 6596* 
A subset of a finite set is finite if it is defined by a decidable
property. (Contributed by Jim Kingdon, 27May2022.)

DECID 

Theorem  ssfidc 6597* 
A subset of a finite set is finite if membership in the subset is
decidable. (Contributed by Jim Kingdon, 27May2022.)

DECID 

Theorem  snon0 6598 
An ordinal which is a singleton is .
(Contributed by Jim
Kingdon, 19Oct2021.)



Theorem  fnfi 6599 
A version of fnex 5482 for finite sets. (Contributed by Mario
Carneiro,
16Nov2014.) (Revised by Mario Carneiro, 24Jun2015.)



Theorem  fundmfi 6600 
The domain of a finite function is finite. (Contributed by Jim Kingdon,
5Feb2022.)

