Type  Label  Description 
Statement 

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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



Theorem  cnven 6319 
A relational set is equinumerous to its converse. (Contributed by Mario
Carneiro, 28Dec2014.)



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



Theorem  en2sn 6321 
Two singletons are equinumerous. (Contributed by NM, 9Nov2003.)



Theorem  snfig 6322 
A singleton is finite. (Contributed by Jim Kingdon, 13Apr2020.)



Theorem  fiprc 6323 
The class of finite sets is a proper class. (Contributed by Jeff
Hankins, 3Oct2008.)



Theorem  unen 6324 
Equinumerosity of union of disjoint sets. Theorem 4 of [Suppes] p. 92.
(Contributed by NM, 11Jun1998.) (Revised by Mario Carneiro,
26Apr2015.)



Theorem  enm 6325* 
A set equinumerous to an inhabited set is inhabited. (Contributed by
Jim Kingdon, 19May2020.)



Theorem  xpsnen 6326 
A set is equinumerous to its Cartesian product with a singleton.
Proposition 4.22(c) of [Mendelson] p.
254. (Contributed by NM,
4Jan2004.) (Revised by Mario Carneiro, 15Nov2014.)



Theorem  xpsneng 6327 
A set is equinumerous to its Cartesian product with a singleton.
Proposition 4.22(c) of [Mendelson] p.
254. (Contributed by NM,
22Oct2004.)



Theorem  xp1en 6328 
One times a cardinal number. (Contributed by NM, 27Sep2004.) (Revised
by Mario Carneiro, 29Apr2015.)



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



Theorem  xpcomf1o 6330* 
The canonical bijection from to .
(Contributed by Mario Carneiro, 23Apr2014.)



Theorem  xpcomco 6331* 
Composition with the bijection of xpcomf1o 6330 swaps the arguments to a
mapping. (Contributed by Mario Carneiro, 30May2015.)



Theorem  xpcomen 6332 
Commutative law for equinumerosity of Cartesian product. Proposition
4.22(d) of [Mendelson] p. 254.
(Contributed by NM, 5Jan2004.)
(Revised by Mario Carneiro, 15Nov2014.)



Theorem  xpcomeng 6333 
Commutative law for equinumerosity of Cartesian product. Proposition
4.22(d) of [Mendelson] p. 254.
(Contributed by NM, 27Mar2006.)



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



Theorem  xpassen 6335 
Associative law for equinumerosity of Cartesian product. Proposition
4.22(e) of [Mendelson] p. 254.
(Contributed by NM, 22Jan2004.)
(Revised by Mario Carneiro, 15Nov2014.)



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



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



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



Theorem  xpdom3m 6339* 
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 6340 
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 6341 
Covering implies injection on power sets. (Contributed by Stefan
O'Rear, 6Nov2014.) (Revised by Mario Carneiro, 24Jun2015.)



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



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



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



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



2.6.26 Pigeonhole Principle


Theorem  phplem1 6346 
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 6347 
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 6348 
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 6350. (Contributed by NM,
26May1998.)



Theorem  phplem4 6349 
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 6350 
A natural number is equinumerous to its successor minus any element of
the successor. Version of phplem3 6348 with unnecessary hypotheses
removed. (Contributed by Jim Kingdon, 1Sep2021.)



Theorem  nneneq 6351 
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 6352 
A natural number is not equinumerous to its successor. Corollary
10.21(1) of [TakeutiZaring] p. 90.
(Contributed by NM, 26Jul2004.)



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



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



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



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



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



Theorem  phpm 6358* 
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 6346 through phplem4 6349, nneneq 6351, and
this final piece of the proof. (Contributed by NM, 29May1998.)



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



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



2.6.27 Finite sets


Theorem  fidceq 6361 
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 6362 
All decrements of a finite set are equinumerous. (Contributed by Jim
Kingdon, 9Sep2021.)



Theorem  fidifsnid 6363 
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 3538 from
subset to equality when the set is finite. (Contributed by Jim Kingdon,
9Sep2021.)



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



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



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



Theorem  ssfiexmid 6367* 
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  dif1en 6368 
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  fiunsnnn 6369 
Adding one element to a finite set which is equinumerous to a natural
number. (Contributed by Jim Kingdon, 13Sep2021.)



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



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



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



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



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



Theorem  diffitest 6375* 
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 6376* 
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 6377* 
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 6378* 
Variation of findcard2 6377 requiring that the element added in the
induction step not be a member of the original set. (Contributed by
Paul Chapman, 30Nov2012.)



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



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



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



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



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



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



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



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



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



2.6.28 Supremum and infimum


Syntax  csup 6388 
Extend class notation to include supremum of class . Here is
ordinarily a relation that strictly orders class . For example,
could be 'less
than' and could be
the set of real numbers.



Syntax  cinf 6389 
Extend class notation to include infimum of class . Here is
ordinarily a relation that strictly orders class . For example,
could be 'less
than' and could be
the set of real numbers.

inf 

Definition  dfsup 6390* 
Define the supremum of class . It is meaningful when is a
relation that strictly orders and when the supremum exists.
(Contributed by NM, 22May1999.)



Definition  dfinf 6391 
Define the infimum of class . It is meaningful when is a
relation that strictly orders and when the infimum exists. For
example, could
be 'less than', could
be the set of real
numbers, and
could be the set of all positive reals; in this case
the infimum is 0. The infimum is defined as the supremum using the
converse ordering relation. In the given example, 0 is the supremum of
all reals (greatest real number) for which all positive reals are greater.
(Contributed by AV, 2Sep2020.)

inf 

Theorem  supeq1 6392 
Equality theorem for supremum. (Contributed by NM, 22May1999.)



Theorem  supeq1d 6393 
Equality deduction for supremum. (Contributed by Paul Chapman,
22Jun2011.)



Theorem  supeq1i 6394 
Equality inference for supremum. (Contributed by Paul Chapman,
22Jun2011.)



Theorem  supeq2 6395 
Equality theorem for supremum. (Contributed by Jeff Madsen,
2Sep2009.)



Theorem  supeq3 6396 
Equality theorem for supremum. (Contributed by Scott Fenton,
13Jun2018.)



Theorem  supeq123d 6397 
Equality deduction for supremum. (Contributed by Stefan O'Rear,
20Jan2015.)



Theorem  nfsup 6398 
Hypothesis builder for supremum. (Contributed by Mario Carneiro,
20Mar2014.)



Theorem  supmoti 6399* 
Any class has at most
one supremum in
(where is
interpreted as 'less than'). The hypothesis is satisfied by real
numbers (see lttri3 7157) or other orders which correspond to tight
apartnesses. (Contributed by Jim Kingdon, 23Nov2021.)



Theorem  supeuti 6400* 
A supremum is unique. Similar to Theorem I.26 of [Apostol] p. 24 (but
for suprema in general). (Contributed by Jim Kingdon,
23Nov2021.)

