Type  Label  Description 
Statement 

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



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



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



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



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



Theorem  nnmcom 6206 
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 6207 
Distributive law for natural numbers (rightdistributivity). (Contributed
by Jim Kingdon, 3Dec2019.)



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



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



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



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



Theorem  nnsucuniel 6212 
Given an element of
the union of a natural number ,
is an element of itself. The reverse
direction holds
for all ordinals (sucunielr 4302). The forward direction for all
ordinals implies excluded middle (ordsucunielexmid 4322). (Contributed
by Jim Kingdon, 13Mar2022.)



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



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



Theorem  nntri2or2 6215 
A trichotomy law for natural numbers. (Contributed by Jim Kingdon,
15Sep2021.)



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

DECID


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

DECID


Theorem  nnsseleq 6218 
For natural numbers, inclusion is equivalent to membership or equality.
(Contributed by Jim Kingdon, 16Sep2021.)



Theorem  dcdifsnid 6219* 
If we remove a single element from a set with decidable equality then
put it back in, we end up with the original set. This strengthens
difsnss 3568 from subset to equality but the proof relies
on equality being
decidable. (Contributed by Jim Kingdon, 17Jun2022.)

DECID


Theorem  nndifsnid 6220 
If we remove a single element from a natural number then put it back in,
we end up with the original natural number. This strengthens difsnss 3568
from subset to equality but the proof relies on equality being
decidable. (Contributed by Jim Kingdon, 31Aug2021.)



Theorem  nnaordi 6221 
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 6222 
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 6223 
Ordering property of addition of natural numbers. (Contributed by NM,
9Nov2002.)



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



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



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



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



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



Theorem  nnmordi 6229 
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 6230 
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 6231 
Weak ordering property of ordinal multiplication. (Contributed by Mario
Carneiro, 17Nov2014.)



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



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



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



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



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



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



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



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



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



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



Theorem  nnm00 6242 
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 6243 
Extend the definition of a wff to include the equivalence predicate.



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



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



Definition  dfer 6246 
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 6247 we derive a
more typical definition. We show that an equivalence relation is
reflexive, symmetric, and transitive in erref 6266, ersymb 6260, and ertr 6261.
(Contributed by NM, 4Jun1995.) (Revised by Mario Carneiro,
2Nov2015.)



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



Definition  dfec 6248 
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 6247). 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 6249. (Contributed by
NM, 23Jul1995.)



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



Theorem  erref 6266 
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 6267 
The converse of an equivalence relation is itself. (Contributed by
Mario Carneiro, 12Aug2015.)



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



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



Theorem  erex 6270 
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 6271 
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 6272* 
A reflexive, symmetric, transitive relation is an equivalence relation
on its domain. (Contributed by Mario Carneiro, 9Jul2014.) (Revised
by Mario Carneiro, 12Aug2015.)



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



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



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



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



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



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



Theorem  ider 6279 
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 6280 
The empty set is an equivalence relation on the empty set. (Contributed
by Mario Carneiro, 5Sep2015.)



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



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



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



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



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



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



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



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



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



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



Theorem  erth2 6291 
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 6292 
Basic property of equivalence relations. Part of Lemma 3N of [Enderton]
p. 57. (Contributed by NM, 30Jul1995.) (Revised by Mario Carneiro,
9Jul2014.)



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



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



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



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



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



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



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



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

