Type  Label  Description 
Statement 

Theorem  nnmcli 6001 
is closed under
multiplication. Inference form of nnmcl 5999.
(Contributed by Scott Fenton, 20Apr2012.)



Theorem  nnacom 6002 
Addition of natural numbers is commutative. Theorem 4K(2) of [Enderton]
p. 81. (Contributed by NM, 6May1995.) (Revised by Mario Carneiro,
15Nov2014.)



Theorem  nnaass 6003 
Addition of natural numbers is associative. Theorem 4K(1) of [Enderton]
p. 81. (Contributed by NM, 20Sep1995.) (Revised by Mario Carneiro,
15Nov2014.)



Theorem  nndi 6004 
Distributive law for natural numbers (leftdistributivity). Theorem
4K(3) of [Enderton] p. 81.
(Contributed by NM, 20Sep1995.) (Revised
by Mario Carneiro, 15Nov2014.)



Theorem  nnmass 6005 
Multiplication of natural numbers is associative. Theorem 4K(4) of
[Enderton] p. 81. (Contributed by NM,
20Sep1995.) (Revised by Mario
Carneiro, 15Nov2014.)



Theorem  nnmsucr 6006 
Multiplication with successor. Exercise 16 of [Enderton] p. 82.
(Contributed by NM, 21Sep1995.) (Proof shortened by Andrew Salmon,
22Oct2011.)



Theorem  nnmcom 6007 
Multiplication of natural numbers is commutative. Theorem 4K(5) of
[Enderton] p. 81. (Contributed by NM,
21Sep1995.) (Proof shortened
by Andrew Salmon, 22Oct2011.)



Theorem  nndir 6008 
Distributive law for natural numbers (rightdistributivity). (Contributed
by Jim Kingdon, 3Dec2019.)



Theorem  nnsucelsuc 6009 
Membership is inherited by successors. The reverse direction holds for
all ordinals, as seen at onsucelsucr 4199, but the forward direction, for
all ordinals, implies excluded middle as seen as onsucelsucexmid 4215.
(Contributed by Jim Kingdon, 25Aug2019.)



Theorem  nnsucsssuc 6010 
Membership is inherited by successors. The reverse direction holds for
all ordinals, as seen at onsucsssucr 4200, but the forward direction, for
all ordinals, implies excluded middle as seen as onsucsssucexmid 4212.
(Contributed by Jim Kingdon, 25Aug2019.)



Theorem  nntri3or 6011 
Trichotomy for natural numbers. (Contributed by Jim Kingdon,
25Aug2019.)



Theorem  nntri2 6012 
A trichotomy law for natural numbers. (Contributed by Jim Kingdon,
28Aug2019.)



Theorem  nntri1 6013 
A trichotomy law for natural numbers. (Contributed by Jim Kingdon,
28Aug2019.)



Theorem  nntri3 6014 
A trichotomy law for natural numbers. (Contributed by Jim Kingdon,
15May2020.)



Theorem  nndceq 6015 
Equality of natural numbers is decidable. Theorem 7.2.6 of [HoTT], p.
(varies). For the specific case where is zero, see nndceq0 4282.
(Contributed by Jim Kingdon, 31Aug2019.)

DECID 

Theorem  nndcel 6016 
Set membership between two natural numbers is decidable. (Contributed by
Jim Kingdon, 6Sep2019.)

DECID 

Theorem  nnaordi 6017 
Ordering property of addition. Proposition 8.4 of [TakeutiZaring]
p. 58, limited to natural numbers. (Contributed by NM, 3Feb1996.)
(Revised by Mario Carneiro, 15Nov2014.)



Theorem  nnaord 6018 
Ordering property of addition. Proposition 8.4 of [TakeutiZaring] p. 58,
limited to natural numbers, and its converse. (Contributed by NM,
7Mar1996.) (Revised by Mario Carneiro, 15Nov2014.)



Theorem  nnaordr 6019 
Ordering property of addition of natural numbers. (Contributed by NM,
9Nov2002.)



Theorem  nnaword 6020 
Weak ordering property of addition. (Contributed by NM, 17Sep1995.)
(Revised by Mario Carneiro, 15Nov2014.)



Theorem  nnacan 6021 
Cancellation law for addition of natural numbers. (Contributed by NM,
27Oct1995.) (Revised by Mario Carneiro, 15Nov2014.)



Theorem  nnaword1 6022 
Weak ordering property of addition. (Contributed by NM, 9Nov2002.)
(Revised by Mario Carneiro, 15Nov2014.)



Theorem  nnaword2 6023 
Weak ordering property of addition. (Contributed by NM, 9Nov2002.)



Theorem  nnawordi 6024 
Adding to both sides of an inequality in (Contributed by Scott
Fenton, 16Apr2012.) (Revised by Mario Carneiro, 12May2012.)



Theorem  nnmordi 6025 
Ordering property of multiplication. Half of Proposition 8.19 of
[TakeutiZaring] p. 63, limited to
natural numbers. (Contributed by NM,
18Sep1995.) (Revised by Mario Carneiro, 15Nov2014.)



Theorem  nnmord 6026 
Ordering property of multiplication. Proposition 8.19 of [TakeutiZaring]
p. 63, limited to natural numbers. (Contributed by NM, 22Jan1996.)
(Revised by Mario Carneiro, 15Nov2014.)



Theorem  nnmword 6027 
Weak ordering property of ordinal multiplication. (Contributed by Mario
Carneiro, 17Nov2014.)



Theorem  nnmcan 6028 
Cancellation law for multiplication of natural numbers. (Contributed by
NM, 26Oct1995.) (Revised by Mario Carneiro, 15Nov2014.)



Theorem  1onn 6029 
One is a natural number. (Contributed by NM, 29Oct1995.)



Theorem  2onn 6030 
The ordinal 2 is a natural number. (Contributed by NM, 28Sep2004.)



Theorem  3onn 6031 
The ordinal 3 is a natural number. (Contributed by Mario Carneiro,
5Jan2016.)



Theorem  4onn 6032 
The ordinal 4 is a natural number. (Contributed by Mario Carneiro,
5Jan2016.)



Theorem  nnm1 6033 
Multiply an element of by .
(Contributed by Mario
Carneiro, 17Nov2014.)



Theorem  nnm2 6034 
Multiply an element of by
(Contributed by Scott Fenton,
18Apr2012.) (Revised by Mario Carneiro, 17Nov2014.)



Theorem  nn2m 6035 
Multiply an element of by
(Contributed by Scott Fenton,
16Apr2012.) (Revised by Mario Carneiro, 17Nov2014.)



Theorem  nnaordex 6036* 
Equivalence for ordering. Compare Exercise 23 of [Enderton] p. 88.
(Contributed by NM, 5Dec1995.) (Revised by Mario Carneiro,
15Nov2014.)



Theorem  nnawordex 6037* 
Equivalence for weak ordering of natural numbers. (Contributed by NM,
8Nov2002.) (Revised by Mario Carneiro, 15Nov2014.)



Theorem  nnm00 6038 
The product of two natural numbers is zero iff at least one of them is
zero. (Contributed by Jim Kingdon, 11Nov2004.)



2.6.24 Equivalence relations and
classes


Syntax  wer 6039 
Extend the definition of a wff to include the equivalence predicate.



Syntax  cec 6040 
Extend the definition of a class to include equivalence class.



Syntax  cqs 6041 
Extend the definition of a class to include quotient set.



Definition  dfer 6042 
Define the equivalence relation predicate. Our notation is not standard.
A formal notation doesn't seem to exist in the literature; instead only
informal English tends to be used. The present definition, although
somewhat cryptic, nicely avoids dummy variables. In dfer2 6043 we derive a
more typical definition. We show that an equivalence relation is
reflexive, symmetric, and transitive in erref 6062, ersymb 6056, and ertr 6057.
(Contributed by NM, 4Jun1995.) (Revised by Mario Carneiro,
2Nov2015.)



Theorem  dfer2 6043* 
Alternate definition of equivalence predicate. (Contributed by NM,
3Jan1997.) (Revised by Mario Carneiro, 12Aug2015.)



Definition  dfec 6044 
Define the coset of
. Exercise 35 of [Enderton] p. 61. This
is called the equivalence class of modulo when is an
equivalence relation (i.e. when ; see dfer2 6043). In this case,
is a
representative (member) of the equivalence class ,
which contains all sets that are equivalent to . Definition of
[Enderton] p. 57 uses the notation (subscript) , although
we simply follow the brackets by since we don't have subscripted
expressions. For an alternate definition, see dfec2 6045. (Contributed by
NM, 23Jul1995.)



Theorem  dfec2 6045* 
Alternate definition of coset of .
Definition 34 of
[Suppes] p. 81. (Contributed by NM,
3Jan1997.) (Proof shortened by
Mario Carneiro, 9Jul2014.)



Theorem  ecexg 6046 
An equivalence class modulo a set is a set. (Contributed by NM,
24Jul1995.)



Theorem  ecexr 6047 
An inhabited equivalence class implies the representative is a set.
(Contributed by Mario Carneiro, 9Jul2014.)



Definition  dfqs 6048* 
Define quotient set.
is usually an equivalence relation.
Definition of [Enderton] p. 58.
(Contributed by NM, 23Jul1995.)



Theorem  ereq1 6049 
Equality theorem for equivalence predicate. (Contributed by NM,
4Jun1995.) (Revised by Mario Carneiro, 12Aug2015.)



Theorem  ereq2 6050 
Equality theorem for equivalence predicate. (Contributed by Mario
Carneiro, 12Aug2015.)



Theorem  errel 6051 
An equivalence relation is a relation. (Contributed by Mario Carneiro,
12Aug2015.)



Theorem  erdm 6052 
The domain of an equivalence relation. (Contributed by Mario Carneiro,
12Aug2015.)



Theorem  ercl 6053 
Elementhood in the field of an equivalence relation. (Contributed by
Mario Carneiro, 12Aug2015.)



Theorem  ersym 6054 
An equivalence relation is symmetric. (Contributed by NM, 4Jun1995.)
(Revised by Mario Carneiro, 12Aug2015.)



Theorem  ercl2 6055 
Elementhood in the field of an equivalence relation. (Contributed by
Mario Carneiro, 12Aug2015.)



Theorem  ersymb 6056 
An equivalence relation is symmetric. (Contributed by NM,
30Jul1995.) (Revised by Mario Carneiro, 12Aug2015.)



Theorem  ertr 6057 
An equivalence relation is transitive. (Contributed by NM,
4Jun1995.) (Revised by Mario Carneiro, 12Aug2015.)



Theorem  ertrd 6058 
A transitivity relation for equivalences. (Contributed by Mario
Carneiro, 9Jul2014.)



Theorem  ertr2d 6059 
A transitivity relation for equivalences. (Contributed by Mario
Carneiro, 9Jul2014.)



Theorem  ertr3d 6060 
A transitivity relation for equivalences. (Contributed by Mario
Carneiro, 9Jul2014.)



Theorem  ertr4d 6061 
A transitivity relation for equivalences. (Contributed by Mario
Carneiro, 9Jul2014.)



Theorem  erref 6062 
An equivalence relation is reflexive on its field. Compare Theorem 3M
of [Enderton] p. 56. (Contributed by
Mario Carneiro, 6May2013.)
(Revised by Mario Carneiro, 12Aug2015.)



Theorem  ercnv 6063 
The converse of an equivalence relation is itself. (Contributed by
Mario Carneiro, 12Aug2015.)



Theorem  errn 6064 
The range and domain of an equivalence relation are equal. (Contributed
by Rodolfo Medina, 11Oct2010.) (Revised by Mario Carneiro,
12Aug2015.)



Theorem  erssxp 6065 
An equivalence relation is a subset of the cartesian product of the
field. (Contributed by Mario Carneiro, 12Aug2015.)



Theorem  erex 6066 
An equivalence relation is a set if its domain is a set. (Contributed by
Rodolfo Medina, 15Oct2010.) (Proof shortened by Mario Carneiro,
12Aug2015.)



Theorem  erexb 6067 
An equivalence relation is a set if and only if its domain is a set.
(Contributed by Rodolfo Medina, 15Oct2010.) (Revised by Mario Carneiro,
12Aug2015.)



Theorem  iserd 6068* 
A reflexive, symmetric, transitive relation is an equivalence relation
on its domain. (Contributed by Mario Carneiro, 9Jul2014.) (Revised
by Mario Carneiro, 12Aug2015.)



Theorem  brdifun 6069 
Evaluate the incomparability relation. (Contributed by Mario Carneiro,
9Jul2014.)



Theorem  swoer 6070* 
Incomparability under a strict weak partial order is an equivalence
relation. (Contributed by Mario Carneiro, 9Jul2014.) (Revised by
Mario Carneiro, 12Aug2015.)



Theorem  swoord1 6071* 
The incomparability equivalence relation is compatible with the
original order. (Contributed by Mario Carneiro, 31Dec2014.)



Theorem  swoord2 6072* 
The incomparability equivalence relation is compatible with the
original order. (Contributed by Mario Carneiro, 31Dec2014.)



Theorem  eqerlem 6073* 
Lemma for eqer 6074. (Contributed by NM, 17Mar2008.) (Proof
shortened
by Mario Carneiro, 6Dec2016.)



Theorem  eqer 6074* 
Equivalence relation involving equality of dependent classes
and . (Contributed by NM, 17Mar2008.) (Revised by Mario
Carneiro, 12Aug2015.)



Theorem  ider 6075 
The identity relation is an equivalence relation. (Contributed by NM,
10May1998.) (Proof shortened by Andrew Salmon, 22Oct2011.) (Proof
shortened by Mario Carneiro, 9Jul2014.)



Theorem  0er 6076 
The empty set is an equivalence relation on the empty set. (Contributed
by Mario Carneiro, 5Sep2015.)



Theorem  eceq1 6077 
Equality theorem for equivalence class. (Contributed by NM,
23Jul1995.)



Theorem  eceq1d 6078 
Equality theorem for equivalence class (deduction form). (Contributed
by Jim Kingdon, 31Dec2019.)



Theorem  eceq2 6079 
Equality theorem for equivalence class. (Contributed by NM,
23Jul1995.)



Theorem  elecg 6080 
Membership in an equivalence class. Theorem 72 of [Suppes] p. 82.
(Contributed by Mario Carneiro, 9Jul2014.)



Theorem  elec 6081 
Membership in an equivalence class. Theorem 72 of [Suppes] p. 82.
(Contributed by NM, 23Jul1995.)



Theorem  relelec 6082 
Membership in an equivalence class when is a relation.
(Contributed by Mario Carneiro, 11Sep2015.)



Theorem  ecss 6083 
An equivalence class is a subset of the domain. (Contributed by NM,
6Aug1995.) (Revised by Mario Carneiro, 12Aug2015.)



Theorem  ecdmn0m 6084* 
A representative of an inhabited equivalence class belongs to the domain
of the equivalence relation. (Contributed by Jim Kingdon,
21Aug2019.)



Theorem  ereldm 6085 
Equality of equivalence classes implies equivalence of domain
membership. (Contributed by NM, 28Jan1996.) (Revised by Mario
Carneiro, 12Aug2015.)



Theorem  erth 6086 
Basic property of equivalence relations. Theorem 73 of [Suppes] p. 82.
(Contributed by NM, 23Jul1995.) (Revised by Mario Carneiro,
6Jul2015.)



Theorem  erth2 6087 
Basic property of equivalence relations. Compare Theorem 73 of [Suppes]
p. 82. Assumes membership of the second argument in the domain.
(Contributed by NM, 30Jul1995.) (Revised by Mario Carneiro,
6Jul2015.)



Theorem  erthi 6088 
Basic property of equivalence relations. Part of Lemma 3N of [Enderton]
p. 57. (Contributed by NM, 30Jul1995.) (Revised by Mario Carneiro,
9Jul2014.)



Theorem  ecidsn 6089 
An equivalence class modulo the identity relation is a singleton.
(Contributed by NM, 24Oct2004.)



Theorem  qseq1 6090 
Equality theorem for quotient set. (Contributed by NM, 23Jul1995.)



Theorem  qseq2 6091 
Equality theorem for quotient set. (Contributed by NM, 23Jul1995.)



Theorem  elqsg 6092* 
Closed form of elqs 6093. (Contributed by Rodolfo Medina,
12Oct2010.)



Theorem  elqs 6093* 
Membership in a quotient set. (Contributed by NM, 23Jul1995.)



Theorem  elqsi 6094* 
Membership in a quotient set. (Contributed by NM, 23Jul1995.)



Theorem  ecelqsg 6095 
Membership of an equivalence class in a quotient set. (Contributed by
Jeff Madsen, 10Jun2010.) (Revised by Mario Carneiro, 9Jul2014.)



Theorem  ecelqsi 6096 
Membership of an equivalence class in a quotient set. (Contributed by
NM, 25Jul1995.) (Revised by Mario Carneiro, 9Jul2014.)



Theorem  ecopqsi 6097 
"Closure" law for equivalence class of ordered pairs. (Contributed
by
NM, 25Mar1996.)



Theorem  qsexg 6098 
A quotient set exists. (Contributed by FL, 19May2007.) (Revised by
Mario Carneiro, 9Jul2014.)



Theorem  qsex 6099 
A quotient set exists. (Contributed by NM, 14Aug1995.)



Theorem  uniqs 6100 
The union of a quotient set. (Contributed by NM, 9Dec2008.)

