Theorem List for Intuitionistic Logic Explorer - 6101-6200 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | nnawordex 6101* |
Equivalence for weak ordering of natural numbers. (Contributed by NM,
8-Nov-2002.) (Revised by Mario Carneiro, 15-Nov-2014.)
|
|
|
Theorem | nnm00 6102 |
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 6103 |
Extend the definition of a wff to include the equivalence predicate.
|
|
|
Syntax | cec 6104 |
Extend the definition of a class to include equivalence class.
|
|
|
Syntax | cqs 6105 |
Extend the definition of a class to include quotient set.
|
|
|
Definition | df-er 6106 |
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 6107 we derive a
more typical definition. We show that an equivalence relation is
reflexive, symmetric, and transitive in erref 6126, ersymb 6120, and ertr 6121.
(Contributed by NM, 4-Jun-1995.) (Revised by Mario Carneiro,
2-Nov-2015.)
|
|
|
Theorem | dfer2 6107* |
Alternate definition of equivalence predicate. (Contributed by NM,
3-Jan-1997.) (Revised by Mario Carneiro, 12-Aug-2015.)
|
|
|
Definition | df-ec 6108 |
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 6107). 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 6109. (Contributed by
NM, 23-Jul-1995.)
|
|
|
Theorem | dfec2 6109* |
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 6110 |
An equivalence class modulo a set is a set. (Contributed by NM,
24-Jul-1995.)
|
|
|
Theorem | ecexr 6111 |
An inhabited equivalence class implies the representative is a set.
(Contributed by Mario Carneiro, 9-Jul-2014.)
|
|
|
Definition | df-qs 6112* |
Define quotient set.
is usually an equivalence relation.
Definition of [Enderton] p. 58.
(Contributed by NM, 23-Jul-1995.)
|
|
|
Theorem | ereq1 6113 |
Equality theorem for equivalence predicate. (Contributed by NM,
4-Jun-1995.) (Revised by Mario Carneiro, 12-Aug-2015.)
|
|
|
Theorem | ereq2 6114 |
Equality theorem for equivalence predicate. (Contributed by Mario
Carneiro, 12-Aug-2015.)
|
|
|
Theorem | errel 6115 |
An equivalence relation is a relation. (Contributed by Mario Carneiro,
12-Aug-2015.)
|
|
|
Theorem | erdm 6116 |
The domain of an equivalence relation. (Contributed by Mario Carneiro,
12-Aug-2015.)
|
|
|
Theorem | ercl 6117 |
Elementhood in the field of an equivalence relation. (Contributed by
Mario Carneiro, 12-Aug-2015.)
|
|
|
Theorem | ersym 6118 |
An equivalence relation is symmetric. (Contributed by NM, 4-Jun-1995.)
(Revised by Mario Carneiro, 12-Aug-2015.)
|
|
|
Theorem | ercl2 6119 |
Elementhood in the field of an equivalence relation. (Contributed by
Mario Carneiro, 12-Aug-2015.)
|
|
|
Theorem | ersymb 6120 |
An equivalence relation is symmetric. (Contributed by NM, 30-Jul-1995.)
(Revised by Mario Carneiro, 12-Aug-2015.)
|
|
|
Theorem | ertr 6121 |
An equivalence relation is transitive. (Contributed by NM, 4-Jun-1995.)
(Revised by Mario Carneiro, 12-Aug-2015.)
|
|
|
Theorem | ertrd 6122 |
A transitivity relation for equivalences. (Contributed by Mario
Carneiro, 9-Jul-2014.)
|
|
|
Theorem | ertr2d 6123 |
A transitivity relation for equivalences. (Contributed by Mario
Carneiro, 9-Jul-2014.)
|
|
|
Theorem | ertr3d 6124 |
A transitivity relation for equivalences. (Contributed by Mario
Carneiro, 9-Jul-2014.)
|
|
|
Theorem | ertr4d 6125 |
A transitivity relation for equivalences. (Contributed by Mario
Carneiro, 9-Jul-2014.)
|
|
|
Theorem | erref 6126 |
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 6127 |
The converse of an equivalence relation is itself. (Contributed by
Mario Carneiro, 12-Aug-2015.)
|
|
|
Theorem | errn 6128 |
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 6129 |
An equivalence relation is a subset of the cartesian product of the field.
(Contributed by Mario Carneiro, 12-Aug-2015.)
|
|
|
Theorem | erex 6130 |
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 6131 |
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 6132* |
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 6133 |
Evaluate the incomparability relation. (Contributed by Mario Carneiro,
9-Jul-2014.)
|
|
|
Theorem | swoer 6134* |
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 6135* |
The incomparability equivalence relation is compatible with the
original order. (Contributed by Mario Carneiro, 31-Dec-2014.)
|
|
|
Theorem | swoord2 6136* |
The incomparability equivalence relation is compatible with the
original order. (Contributed by Mario Carneiro, 31-Dec-2014.)
|
|
|
Theorem | eqerlem 6137* |
Lemma for eqer 6138. (Contributed by NM, 17-Mar-2008.) (Proof
shortened
by Mario Carneiro, 6-Dec-2016.)
|
|
|
Theorem | eqer 6138* |
Equivalence relation involving equality of dependent classes
and . (Contributed by NM, 17-Mar-2008.) (Revised by Mario
Carneiro, 12-Aug-2015.)
|
|
|
Theorem | ider 6139 |
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 6140 |
The empty set is an equivalence relation on the empty set. (Contributed
by Mario Carneiro, 5-Sep-2015.)
|
|
|
Theorem | eceq1 6141 |
Equality theorem for equivalence class. (Contributed by NM,
23-Jul-1995.)
|
|
|
Theorem | eceq1d 6142 |
Equality theorem for equivalence class (deduction form). (Contributed
by Jim Kingdon, 31-Dec-2019.)
|
|
|
Theorem | eceq2 6143 |
Equality theorem for equivalence class. (Contributed by NM,
23-Jul-1995.)
|
|
|
Theorem | elecg 6144 |
Membership in an equivalence class. Theorem 72 of [Suppes] p. 82.
(Contributed by Mario Carneiro, 9-Jul-2014.)
|
|
|
Theorem | elec 6145 |
Membership in an equivalence class. Theorem 72 of [Suppes] p. 82.
(Contributed by NM, 23-Jul-1995.)
|
|
|
Theorem | relelec 6146 |
Membership in an equivalence class when is a relation.
(Contributed by Mario Carneiro, 11-Sep-2015.)
|
|
|
Theorem | ecss 6147 |
An equivalence class is a subset of the domain. (Contributed by NM,
6-Aug-1995.) (Revised by Mario Carneiro, 12-Aug-2015.)
|
|
|
Theorem | ecdmn0m 6148* |
A representative of an inhabited equivalence class belongs to the domain
of the equivalence relation. (Contributed by Jim Kingdon,
21-Aug-2019.)
|
|
|
Theorem | ereldm 6149 |
Equality of equivalence classes implies equivalence of domain
membership. (Contributed by NM, 28-Jan-1996.) (Revised by Mario
Carneiro, 12-Aug-2015.)
|
|
|
Theorem | erth 6150 |
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 6151 |
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 6152 |
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 6153 |
An equivalence class modulo the identity relation is a singleton.
(Contributed by NM, 24-Oct-2004.)
|
|
|
Theorem | qseq1 6154 |
Equality theorem for quotient set. (Contributed by NM, 23-Jul-1995.)
|
|
|
Theorem | qseq2 6155 |
Equality theorem for quotient set. (Contributed by NM, 23-Jul-1995.)
|
|
|
Theorem | elqsg 6156* |
Closed form of elqs 6157. (Contributed by Rodolfo Medina,
12-Oct-2010.)
|
|
|
Theorem | elqs 6157* |
Membership in a quotient set. (Contributed by NM, 23-Jul-1995.)
|
|
|
Theorem | elqsi 6158* |
Membership in a quotient set. (Contributed by NM, 23-Jul-1995.)
|
|
|
Theorem | ecelqsg 6159 |
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 6160 |
Membership of an equivalence class in a quotient set. (Contributed by
NM, 25-Jul-1995.) (Revised by Mario Carneiro, 9-Jul-2014.)
|
|
|
Theorem | ecopqsi 6161 |
"Closure" law for equivalence class of ordered pairs. (Contributed
by
NM, 25-Mar-1996.)
|
|
|
Theorem | qsexg 6162 |
A quotient set exists. (Contributed by FL, 19-May-2007.) (Revised by
Mario Carneiro, 9-Jul-2014.)
|
|
|
Theorem | qsex 6163 |
A quotient set exists. (Contributed by NM, 14-Aug-1995.)
|
|
|
Theorem | uniqs 6164 |
The union of a quotient set. (Contributed by NM, 9-Dec-2008.)
|
|
|
Theorem | qsss 6165 |
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 6166 |
The union of a quotient set. (Contributed by Mario Carneiro,
11-Jul-2014.)
|
|
|
Theorem | snec 6167 |
The singleton of an equivalence class. (Contributed by NM,
29-Jan-1999.) (Revised by Mario Carneiro, 9-Jul-2014.)
|
|
|
Theorem | ecqs 6168 |
Equivalence class in terms of quotient set. (Contributed by NM,
29-Jan-1999.)
|
|
|
Theorem | ecid 6169 |
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 6170 |
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 6171 |
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 6172* |
Implicit substitution of class for equivalence class. (Contributed by
Mario Carneiro, 9-Jul-2014.)
|
|
|
Theorem | ectocl 6173* |
Implicit substitution of class for equivalence class. (Contributed by
NM, 23-Jul-1995.) (Revised by Mario Carneiro, 9-Jul-2014.)
|
|
|
Theorem | elqsn0m 6174* |
An element of a quotient set is inhabited. (Contributed by Jim Kingdon,
21-Aug-2019.)
|
|
|
Theorem | elqsn0 6175 |
A quotient set doesn't contain the empty set. (Contributed by NM,
24-Aug-1995.)
|
|
|
Theorem | ecelqsdm 6176 |
Membership of an equivalence class in a quotient set. (Contributed by
NM, 30-Jul-1995.)
|
|
|
Theorem | xpiderm 6177* |
A square Cartesian product is an equivalence relation (in general it's
not a poset). (Contributed by Jim Kingdon, 22-Aug-2019.)
|
|
|
Theorem | iinerm 6178* |
The intersection of a nonempty family of equivalence relations is an
equivalence relation. (Contributed by Mario Carneiro, 27-Sep-2015.)
|
|
|
Theorem | riinerm 6179* |
The relative intersection of a family of equivalence relations is an
equivalence relation. (Contributed by Mario Carneiro, 27-Sep-2015.)
|
|
|
Theorem | erinxp 6180 |
A restricted equivalence relation is an equivalence relation.
(Contributed by Mario Carneiro, 10-Jul-2015.) (Revised by Mario
Carneiro, 12-Aug-2015.)
|
|
|
Theorem | ecinxp 6181 |
Restrict the relation in an equivalence class to a base set. (Contributed
by Mario Carneiro, 10-Jul-2015.)
|
|
|
Theorem | qsinxp 6182 |
Restrict the equivalence relation in a quotient set to the base set.
(Contributed by Mario Carneiro, 23-Feb-2015.)
|
|
|
Theorem | qsel 6183 |
If an element of a quotient set contains a given element, it is equal to
the equivalence class of the element. (Contributed by Mario Carneiro,
12-Aug-2015.)
|
|
|
Theorem | qliftlem 6184* |
, a function lift, is
a subset of . (Contributed by
Mario Carneiro, 23-Dec-2016.)
|
|
|
Theorem | qliftrel 6185* |
, a function lift, is
a subset of . (Contributed by
Mario Carneiro, 23-Dec-2016.)
|
|
|
Theorem | qliftel 6186* |
Elementhood in the relation . (Contributed by Mario Carneiro,
23-Dec-2016.)
|
|
|
Theorem | qliftel1 6187* |
Elementhood in the relation . (Contributed by Mario Carneiro,
23-Dec-2016.)
|
|
|
Theorem | qliftfun 6188* |
The function is the
unique function defined by
, provided that the well-definedness condition
holds. (Contributed by Mario Carneiro, 23-Dec-2016.)
|
|
|
Theorem | qliftfund 6189* |
The function is the
unique function defined by
, provided that the well-definedness condition
holds. (Contributed by Mario Carneiro, 23-Dec-2016.)
|
|
|
Theorem | qliftfuns 6190* |
The function is the
unique function defined by
, provided that the well-definedness condition
holds.
(Contributed by Mario Carneiro, 23-Dec-2016.)
|
|
|
Theorem | qliftf 6191* |
The domain and range of the function . (Contributed by Mario
Carneiro, 23-Dec-2016.)
|
|
|
Theorem | qliftval 6192* |
The value of the function . (Contributed by Mario Carneiro,
23-Dec-2016.)
|
|
|
Theorem | ecoptocl 6193* |
Implicit substitution of class for equivalence class of ordered pair.
(Contributed by NM, 23-Jul-1995.)
|
|
|
Theorem | 2ecoptocl 6194* |
Implicit substitution of classes for equivalence classes of ordered
pairs. (Contributed by NM, 23-Jul-1995.)
|
|
|
Theorem | 3ecoptocl 6195* |
Implicit substitution of classes for equivalence classes of ordered
pairs. (Contributed by NM, 9-Aug-1995.)
|
|
|
Theorem | brecop 6196* |
Binary relation on a quotient set. Lemma for real number construction.
(Contributed by NM, 29-Jan-1996.)
|
|
|
Theorem | eroveu 6197* |
Lemma for eroprf 6199. (Contributed by Jeff Madsen, 10-Jun-2010.)
(Revised by Mario Carneiro, 9-Jul-2014.)
|
|
|
Theorem | erovlem 6198* |
Lemma for eroprf 6199. (Contributed by Jeff Madsen, 10-Jun-2010.)
(Revised by Mario Carneiro, 30-Dec-2014.)
|
|
|
Theorem | eroprf 6199* |
Functionality of an operation defined on equivalence classes.
(Contributed by Jeff Madsen, 10-Jun-2010.) (Revised by Mario Carneiro,
30-Dec-2014.)
|
|
|
Theorem | eroprf2 6200* |
Functionality of an operation defined on equivalence classes.
(Contributed by Jeff Madsen, 10-Jun-2010.)
|
|