Theorem List for Intuitionistic Logic Explorer - 6101-6200 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | nndcel 6101 |
Set membership between two natural numbers is decidable. (Contributed by
Jim Kingdon, 6-Sep-2019.)
|
DECID
|
|
Theorem | nnsseleq 6102 |
For natural numbers, inclusion is equivalent to membership or equality.
(Contributed by Jim Kingdon, 16-Sep-2021.)
|
|
|
Theorem | nndifsnid 6103 |
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 3531
from subset to equality but the proof relies on equality being
decidable. (Contributed by Jim Kingdon, 31-Aug-2021.)
|
|
|
Theorem | nnaordi 6104 |
Ordering property of addition. Proposition 8.4 of [TakeutiZaring]
p. 58, limited to natural numbers. (Contributed by NM, 3-Feb-1996.)
(Revised by Mario Carneiro, 15-Nov-2014.)
|
|
|
Theorem | nnaord 6105 |
Ordering property of addition. Proposition 8.4 of [TakeutiZaring] p. 58,
limited to natural numbers, and its converse. (Contributed by NM,
7-Mar-1996.) (Revised by Mario Carneiro, 15-Nov-2014.)
|
|
|
Theorem | nnaordr 6106 |
Ordering property of addition of natural numbers. (Contributed by NM,
9-Nov-2002.)
|
|
|
Theorem | nnaword 6107 |
Weak ordering property of addition. (Contributed by NM, 17-Sep-1995.)
(Revised by Mario Carneiro, 15-Nov-2014.)
|
|
|
Theorem | nnacan 6108 |
Cancellation law for addition of natural numbers. (Contributed by NM,
27-Oct-1995.) (Revised by Mario Carneiro, 15-Nov-2014.)
|
|
|
Theorem | nnaword1 6109 |
Weak ordering property of addition. (Contributed by NM, 9-Nov-2002.)
(Revised by Mario Carneiro, 15-Nov-2014.)
|
|
|
Theorem | nnaword2 6110 |
Weak ordering property of addition. (Contributed by NM, 9-Nov-2002.)
|
|
|
Theorem | nnawordi 6111 |
Adding to both sides of an inequality in (Contributed by Scott
Fenton, 16-Apr-2012.) (Revised by Mario Carneiro, 12-May-2012.)
|
|
|
Theorem | nnmordi 6112 |
Ordering property of multiplication. Half of Proposition 8.19 of
[TakeutiZaring] p. 63, limited to
natural numbers. (Contributed by NM,
18-Sep-1995.) (Revised by Mario Carneiro, 15-Nov-2014.)
|
|
|
Theorem | nnmord 6113 |
Ordering property of multiplication. Proposition 8.19 of [TakeutiZaring]
p. 63, limited to natural numbers. (Contributed by NM, 22-Jan-1996.)
(Revised by Mario Carneiro, 15-Nov-2014.)
|
|
|
Theorem | nnmword 6114 |
Weak ordering property of ordinal multiplication. (Contributed by Mario
Carneiro, 17-Nov-2014.)
|
|
|
Theorem | nnmcan 6115 |
Cancellation law for multiplication of natural numbers. (Contributed by
NM, 26-Oct-1995.) (Revised by Mario Carneiro, 15-Nov-2014.)
|
|
|
Theorem | 1onn 6116 |
One is a natural number. (Contributed by NM, 29-Oct-1995.)
|
|
|
Theorem | 2onn 6117 |
The ordinal 2 is a natural number. (Contributed by NM, 28-Sep-2004.)
|
|
|
Theorem | 3onn 6118 |
The ordinal 3 is a natural number. (Contributed by Mario Carneiro,
5-Jan-2016.)
|
|
|
Theorem | 4onn 6119 |
The ordinal 4 is a natural number. (Contributed by Mario Carneiro,
5-Jan-2016.)
|
|
|
Theorem | nnm1 6120 |
Multiply an element of by .
(Contributed by Mario
Carneiro, 17-Nov-2014.)
|
|
|
Theorem | nnm2 6121 |
Multiply an element of by
(Contributed by Scott Fenton,
18-Apr-2012.) (Revised by Mario Carneiro, 17-Nov-2014.)
|
|
|
Theorem | nn2m 6122 |
Multiply an element of by
(Contributed by Scott Fenton,
16-Apr-2012.) (Revised by Mario Carneiro, 17-Nov-2014.)
|
|
|
Theorem | nnaordex 6123* |
Equivalence for ordering. Compare Exercise 23 of [Enderton] p. 88.
(Contributed by NM, 5-Dec-1995.) (Revised by Mario Carneiro,
15-Nov-2014.)
|
|
|
Theorem | nnawordex 6124* |
Equivalence for weak ordering of natural numbers. (Contributed by NM,
8-Nov-2002.) (Revised by Mario Carneiro, 15-Nov-2014.)
|
|
|
Theorem | nnm00 6125 |
The product of two natural numbers is zero iff at least one of them is
zero. (Contributed by Jim Kingdon, 11-Nov-2004.)
|
|
|
2.6.24 Equivalence relations and
classes
|
|
Syntax | wer 6126 |
Extend the definition of a wff to include the equivalence predicate.
|
|
|
Syntax | cec 6127 |
Extend the definition of a class to include equivalence class.
|
|
|
Syntax | cqs 6128 |
Extend the definition of a class to include quotient set.
|
|
|
Definition | df-er 6129 |
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 6130 we derive a
more typical definition. We show that an equivalence relation is
reflexive, symmetric, and transitive in erref 6149, ersymb 6143, and ertr 6144.
(Contributed by NM, 4-Jun-1995.) (Revised by Mario Carneiro,
2-Nov-2015.)
|
|
|
Theorem | dfer2 6130* |
Alternate definition of equivalence predicate. (Contributed by NM,
3-Jan-1997.) (Revised by Mario Carneiro, 12-Aug-2015.)
|
|
|
Definition | df-ec 6131 |
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 6130). 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 6132. (Contributed by
NM, 23-Jul-1995.)
|
|
|
Theorem | dfec2 6132* |
Alternate definition of -coset of .
Definition 34 of
[Suppes] p. 81. (Contributed by NM,
3-Jan-1997.) (Proof shortened by
Mario Carneiro, 9-Jul-2014.)
|
|
|
Theorem | ecexg 6133 |
An equivalence class modulo a set is a set. (Contributed by NM,
24-Jul-1995.)
|
|
|
Theorem | ecexr 6134 |
An inhabited equivalence class implies the representative is a set.
(Contributed by Mario Carneiro, 9-Jul-2014.)
|
|
|
Definition | df-qs 6135* |
Define quotient set.
is usually an equivalence relation.
Definition of [Enderton] p. 58.
(Contributed by NM, 23-Jul-1995.)
|
|
|
Theorem | ereq1 6136 |
Equality theorem for equivalence predicate. (Contributed by NM,
4-Jun-1995.) (Revised by Mario Carneiro, 12-Aug-2015.)
|
|
|
Theorem | ereq2 6137 |
Equality theorem for equivalence predicate. (Contributed by Mario
Carneiro, 12-Aug-2015.)
|
|
|
Theorem | errel 6138 |
An equivalence relation is a relation. (Contributed by Mario Carneiro,
12-Aug-2015.)
|
|
|
Theorem | erdm 6139 |
The domain of an equivalence relation. (Contributed by Mario Carneiro,
12-Aug-2015.)
|
|
|
Theorem | ercl 6140 |
Elementhood in the field of an equivalence relation. (Contributed by
Mario Carneiro, 12-Aug-2015.)
|
|
|
Theorem | ersym 6141 |
An equivalence relation is symmetric. (Contributed by NM, 4-Jun-1995.)
(Revised by Mario Carneiro, 12-Aug-2015.)
|
|
|
Theorem | ercl2 6142 |
Elementhood in the field of an equivalence relation. (Contributed by
Mario Carneiro, 12-Aug-2015.)
|
|
|
Theorem | ersymb 6143 |
An equivalence relation is symmetric. (Contributed by NM, 30-Jul-1995.)
(Revised by Mario Carneiro, 12-Aug-2015.)
|
|
|
Theorem | ertr 6144 |
An equivalence relation is transitive. (Contributed by NM, 4-Jun-1995.)
(Revised by Mario Carneiro, 12-Aug-2015.)
|
|
|
Theorem | ertrd 6145 |
A transitivity relation for equivalences. (Contributed by Mario
Carneiro, 9-Jul-2014.)
|
|
|
Theorem | ertr2d 6146 |
A transitivity relation for equivalences. (Contributed by Mario
Carneiro, 9-Jul-2014.)
|
|
|
Theorem | ertr3d 6147 |
A transitivity relation for equivalences. (Contributed by Mario
Carneiro, 9-Jul-2014.)
|
|
|
Theorem | ertr4d 6148 |
A transitivity relation for equivalences. (Contributed by Mario
Carneiro, 9-Jul-2014.)
|
|
|
Theorem | erref 6149 |
An equivalence relation is reflexive on its field. Compare Theorem 3M
of [Enderton] p. 56. (Contributed by
Mario Carneiro, 6-May-2013.)
(Revised by Mario Carneiro, 12-Aug-2015.)
|
|
|
Theorem | ercnv 6150 |
The converse of an equivalence relation is itself. (Contributed by
Mario Carneiro, 12-Aug-2015.)
|
|
|
Theorem | errn 6151 |
The range and domain of an equivalence relation are equal. (Contributed
by Rodolfo Medina, 11-Oct-2010.) (Revised by Mario Carneiro,
12-Aug-2015.)
|
|
|
Theorem | erssxp 6152 |
An equivalence relation is a subset of the cartesian product of the field.
(Contributed by Mario Carneiro, 12-Aug-2015.)
|
|
|
Theorem | erex 6153 |
An equivalence relation is a set if its domain is a set. (Contributed by
Rodolfo Medina, 15-Oct-2010.) (Proof shortened by Mario Carneiro,
12-Aug-2015.)
|
|
|
Theorem | erexb 6154 |
An equivalence relation is a set if and only if its domain is a set.
(Contributed by Rodolfo Medina, 15-Oct-2010.) (Revised by Mario Carneiro,
12-Aug-2015.)
|
|
|
Theorem | iserd 6155* |
A reflexive, symmetric, transitive relation is an equivalence relation
on its domain. (Contributed by Mario Carneiro, 9-Jul-2014.) (Revised
by Mario Carneiro, 12-Aug-2015.)
|
|
|
Theorem | brdifun 6156 |
Evaluate the incomparability relation. (Contributed by Mario Carneiro,
9-Jul-2014.)
|
|
|
Theorem | swoer 6157* |
Incomparability under a strict weak partial order is an equivalence
relation. (Contributed by Mario Carneiro, 9-Jul-2014.) (Revised by
Mario Carneiro, 12-Aug-2015.)
|
|
|
Theorem | swoord1 6158* |
The incomparability equivalence relation is compatible with the
original order. (Contributed by Mario Carneiro, 31-Dec-2014.)
|
|
|
Theorem | swoord2 6159* |
The incomparability equivalence relation is compatible with the
original order. (Contributed by Mario Carneiro, 31-Dec-2014.)
|
|
|
Theorem | eqerlem 6160* |
Lemma for eqer 6161. (Contributed by NM, 17-Mar-2008.) (Proof
shortened
by Mario Carneiro, 6-Dec-2016.)
|
|
|
Theorem | eqer 6161* |
Equivalence relation involving equality of dependent classes
and . (Contributed by NM, 17-Mar-2008.) (Revised by Mario
Carneiro, 12-Aug-2015.)
|
|
|
Theorem | ider 6162 |
The identity relation is an equivalence relation. (Contributed by NM,
10-May-1998.) (Proof shortened by Andrew Salmon, 22-Oct-2011.) (Proof
shortened by Mario Carneiro, 9-Jul-2014.)
|
|
|
Theorem | 0er 6163 |
The empty set is an equivalence relation on the empty set. (Contributed
by Mario Carneiro, 5-Sep-2015.)
|
|
|
Theorem | eceq1 6164 |
Equality theorem for equivalence class. (Contributed by NM,
23-Jul-1995.)
|
|
|
Theorem | eceq1d 6165 |
Equality theorem for equivalence class (deduction form). (Contributed
by Jim Kingdon, 31-Dec-2019.)
|
|
|
Theorem | eceq2 6166 |
Equality theorem for equivalence class. (Contributed by NM,
23-Jul-1995.)
|
|
|
Theorem | elecg 6167 |
Membership in an equivalence class. Theorem 72 of [Suppes] p. 82.
(Contributed by Mario Carneiro, 9-Jul-2014.)
|
|
|
Theorem | elec 6168 |
Membership in an equivalence class. Theorem 72 of [Suppes] p. 82.
(Contributed by NM, 23-Jul-1995.)
|
|
|
Theorem | relelec 6169 |
Membership in an equivalence class when is a relation. (Contributed
by Mario Carneiro, 11-Sep-2015.)
|
|
|
Theorem | ecss 6170 |
An equivalence class is a subset of the domain. (Contributed by NM,
6-Aug-1995.) (Revised by Mario Carneiro, 12-Aug-2015.)
|
|
|
Theorem | ecdmn0m 6171* |
A representative of an inhabited equivalence class belongs to the domain
of the equivalence relation. (Contributed by Jim Kingdon,
21-Aug-2019.)
|
|
|
Theorem | ereldm 6172 |
Equality of equivalence classes implies equivalence of domain
membership. (Contributed by NM, 28-Jan-1996.) (Revised by Mario
Carneiro, 12-Aug-2015.)
|
|
|
Theorem | erth 6173 |
Basic property of equivalence relations. Theorem 73 of [Suppes] p. 82.
(Contributed by NM, 23-Jul-1995.) (Revised by Mario Carneiro,
6-Jul-2015.)
|
|
|
Theorem | erth2 6174 |
Basic property of equivalence relations. Compare Theorem 73 of [Suppes]
p. 82. Assumes membership of the second argument in the domain.
(Contributed by NM, 30-Jul-1995.) (Revised by Mario Carneiro,
6-Jul-2015.)
|
|
|
Theorem | erthi 6175 |
Basic property of equivalence relations. Part of Lemma 3N of [Enderton]
p. 57. (Contributed by NM, 30-Jul-1995.) (Revised by Mario Carneiro,
9-Jul-2014.)
|
|
|
Theorem | ecidsn 6176 |
An equivalence class modulo the identity relation is a singleton.
(Contributed by NM, 24-Oct-2004.)
|
|
|
Theorem | qseq1 6177 |
Equality theorem for quotient set. (Contributed by NM, 23-Jul-1995.)
|
|
|
Theorem | qseq2 6178 |
Equality theorem for quotient set. (Contributed by NM, 23-Jul-1995.)
|
|
|
Theorem | elqsg 6179* |
Closed form of elqs 6180. (Contributed by Rodolfo Medina,
12-Oct-2010.)
|
|
|
Theorem | elqs 6180* |
Membership in a quotient set. (Contributed by NM, 23-Jul-1995.)
|
|
|
Theorem | elqsi 6181* |
Membership in a quotient set. (Contributed by NM, 23-Jul-1995.)
|
|
|
Theorem | ecelqsg 6182 |
Membership of an equivalence class in a quotient set. (Contributed by
Jeff Madsen, 10-Jun-2010.) (Revised by Mario Carneiro, 9-Jul-2014.)
|
|
|
Theorem | ecelqsi 6183 |
Membership of an equivalence class in a quotient set. (Contributed by
NM, 25-Jul-1995.) (Revised by Mario Carneiro, 9-Jul-2014.)
|
|
|
Theorem | ecopqsi 6184 |
"Closure" law for equivalence class of ordered pairs. (Contributed
by
NM, 25-Mar-1996.)
|
|
|
Theorem | qsexg 6185 |
A quotient set exists. (Contributed by FL, 19-May-2007.) (Revised by
Mario Carneiro, 9-Jul-2014.)
|
|
|
Theorem | qsex 6186 |
A quotient set exists. (Contributed by NM, 14-Aug-1995.)
|
|
|
Theorem | uniqs 6187 |
The union of a quotient set. (Contributed by NM, 9-Dec-2008.)
|
|
|
Theorem | qsss 6188 |
A quotient set is a set of subsets of the base set. (Contributed by
Mario Carneiro, 9-Jul-2014.) (Revised by Mario Carneiro,
12-Aug-2015.)
|
|
|
Theorem | uniqs2 6189 |
The union of a quotient set. (Contributed by Mario Carneiro,
11-Jul-2014.)
|
|
|
Theorem | snec 6190 |
The singleton of an equivalence class. (Contributed by NM,
29-Jan-1999.) (Revised by Mario Carneiro, 9-Jul-2014.)
|
|
|
Theorem | ecqs 6191 |
Equivalence class in terms of quotient set. (Contributed by NM,
29-Jan-1999.)
|
|
|
Theorem | ecid 6192 |
A set is equal to its converse epsilon coset. (Note: converse epsilon
is not an equivalence relation.) (Contributed by NM, 13-Aug-1995.)
(Revised by Mario Carneiro, 9-Jul-2014.)
|
|
|
Theorem | ecidg 6193 |
A set is equal to its converse epsilon coset. (Note: converse epsilon
is not an equivalence relation.) (Contributed by Jim Kingdon,
8-Jan-2020.)
|
|
|
Theorem | qsid 6194 |
A set is equal to its quotient set mod converse epsilon. (Note:
converse epsilon is not an equivalence relation.) (Contributed by NM,
13-Aug-1995.) (Revised by Mario Carneiro, 9-Jul-2014.)
|
|
|
Theorem | ectocld 6195* |
Implicit substitution of class for equivalence class. (Contributed by
Mario Carneiro, 9-Jul-2014.)
|
|
|
Theorem | ectocl 6196* |
Implicit substitution of class for equivalence class. (Contributed by
NM, 23-Jul-1995.) (Revised by Mario Carneiro, 9-Jul-2014.)
|
|
|
Theorem | elqsn0m 6197* |
An element of a quotient set is inhabited. (Contributed by Jim Kingdon,
21-Aug-2019.)
|
|
|
Theorem | elqsn0 6198 |
A quotient set doesn't contain the empty set. (Contributed by NM,
24-Aug-1995.)
|
|
|
Theorem | ecelqsdm 6199 |
Membership of an equivalence class in a quotient set. (Contributed by
NM, 30-Jul-1995.)
|
|
|
Theorem | xpiderm 6200* |
A square Cartesian product is an equivalence relation (in general it's
not a poset). (Contributed by Jim Kingdon, 22-Aug-2019.)
|
|