Type  Label  Description 
Statement 

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



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



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



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



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



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



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



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

DECID


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

DECID


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



Theorem  nndifsnid 6111 
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 3538
from subset to equality but the proof relies on equality being
decidable. (Contributed by Jim Kingdon, 31Aug2021.)



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



Definition  dfec 6139 
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 6138). 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 6140. (Contributed by
NM, 23Jul1995.)



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



Theorem  qsss 6196 
A quotient set is a set of subsets of the base set. (Contributed by
Mario Carneiro, 9Jul2014.) (Revised by Mario Carneiro,
12Aug2015.)



Theorem  uniqs2 6197 
The union of a quotient set. (Contributed by Mario Carneiro,
11Jul2014.)



Theorem  snec 6198 
The singleton of an equivalence class. (Contributed by NM,
29Jan1999.) (Revised by Mario Carneiro, 9Jul2014.)



Theorem  ecqs 6199 
Equivalence class in terms of quotient set. (Contributed by NM,
29Jan1999.)



Theorem  ecid 6200 
A set is equal to its converse epsilon coset. (Note: converse epsilon
is not an equivalence relation.) (Contributed by NM, 13Aug1995.)
(Revised by Mario Carneiro, 9Jul2014.)

