Type  Label  Description 
Statement 

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



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



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



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



Theorem  ecid 6105 
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.)



Theorem  ecidg 6106 
A set is equal to its converse epsilon coset. (Note: converse epsilon
is not an equivalence relation.) (Contributed by Jim Kingdon,
8Jan2020.)



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



Theorem  ectocld 6108* 
Implicit substitution of class for equivalence class. (Contributed by
Mario Carneiro, 9Jul2014.)



Theorem  ectocl 6109* 
Implicit substitution of class for equivalence class. (Contributed by
NM, 23Jul1995.) (Revised by Mario Carneiro, 9Jul2014.)



Theorem  elqsn0m 6110* 
An element of a quotient set is inhabited. (Contributed by Jim Kingdon,
21Aug2019.)



Theorem  elqsn0 6111 
A quotient set doesn't contain the empty set. (Contributed by NM,
24Aug1995.)



Theorem  ecelqsdm 6112 
Membership of an equivalence class in a quotient set. (Contributed by
NM, 30Jul1995.)



Theorem  xpiderm 6113* 
A square Cartesian product is an equivalence relation (in general it's
not a poset). (Contributed by Jim Kingdon, 22Aug2019.)



Theorem  iinerm 6114* 
The intersection of a nonempty family of equivalence relations is an
equivalence relation. (Contributed by Mario Carneiro, 27Sep2015.)



Theorem  riinerm 6115* 
The relative intersection of a family of equivalence relations is an
equivalence relation. (Contributed by Mario Carneiro, 27Sep2015.)



Theorem  erinxp 6116 
A restricted equivalence relation is an equivalence relation.
(Contributed by Mario Carneiro, 10Jul2015.) (Revised by Mario
Carneiro, 12Aug2015.)



Theorem  ecinxp 6117 
Restrict the relation in an equivalence class to a base set. (Contributed
by Mario Carneiro, 10Jul2015.)



Theorem  qsinxp 6118 
Restrict the equivalence relation in a quotient set to the base set.
(Contributed by Mario Carneiro, 23Feb2015.)



Theorem  qsel 6119 
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,
12Aug2015.)



Theorem  qliftlem 6120* 
, a function lift, is
a subset of . (Contributed by
Mario Carneiro, 23Dec2016.)



Theorem  qliftrel 6121* 
, a function lift, is
a subset of . (Contributed by
Mario Carneiro, 23Dec2016.)



Theorem  qliftel 6122* 
Elementhood in the relation . (Contributed by Mario Carneiro,
23Dec2016.)



Theorem  qliftel1 6123* 
Elementhood in the relation . (Contributed by Mario Carneiro,
23Dec2016.)



Theorem  qliftfun 6124* 
The function is the
unique function defined by
, provided that the
welldefinedness condition
holds. (Contributed by Mario Carneiro, 23Dec2016.)



Theorem  qliftfund 6125* 
The function is the
unique function defined by
, provided that the
welldefinedness condition
holds. (Contributed by Mario Carneiro, 23Dec2016.)



Theorem  qliftfuns 6126* 
The function is the
unique function defined by
, provided that the
welldefinedness condition
holds. (Contributed by Mario Carneiro, 23Dec2016.)



Theorem  qliftf 6127* 
The domain and range of the function . (Contributed by Mario
Carneiro, 23Dec2016.)



Theorem  qliftval 6128* 
The value of the function . (Contributed by Mario Carneiro,
23Dec2016.)



Theorem  ecoptocl 6129* 
Implicit substitution of class for equivalence class of ordered pair.
(Contributed by NM, 23Jul1995.)



Theorem  2ecoptocl 6130* 
Implicit substitution of classes for equivalence classes of ordered
pairs. (Contributed by NM, 23Jul1995.)



Theorem  3ecoptocl 6131* 
Implicit substitution of classes for equivalence classes of ordered
pairs. (Contributed by NM, 9Aug1995.)



Theorem  brecop 6132* 
Binary relation on a quotient set. Lemma for real number construction.
(Contributed by NM, 29Jan1996.)



Theorem  eroveu 6133* 
Lemma for eroprf 6135. (Contributed by Jeff Madsen, 10Jun2010.)
(Revised by Mario Carneiro, 9Jul2014.)



Theorem  erovlem 6134* 
Lemma for eroprf 6135. (Contributed by Jeff Madsen, 10Jun2010.)
(Revised by Mario Carneiro, 30Dec2014.)



Theorem  eroprf 6135* 
Functionality of an operation defined on equivalence classes.
(Contributed by Jeff Madsen, 10Jun2010.) (Revised by Mario Carneiro,
30Dec2014.)



Theorem  eroprf2 6136* 
Functionality of an operation defined on equivalence classes.
(Contributed by Jeff Madsen, 10Jun2010.)



Theorem  ecopoveq 6137* 
This is the first of several theorems about equivalence relations of
the kind used in construction of fractions and signed reals, involving
operations on equivalent classes of ordered pairs. This theorem
expresses the relation (specified by the hypothesis) in terms
of its operation . (Contributed by NM, 16Aug1995.)



Theorem  ecopovsym 6138* 
Assuming the operation is commutative, show that the relation
,
specified by the first hypothesis, is symmetric.
(Contributed by NM, 27Aug1995.) (Revised by Mario Carneiro,
26Apr2015.)



Theorem  ecopovtrn 6139* 
Assuming that operation is commutative (second hypothesis),
closed (third hypothesis), associative (fourth hypothesis), and has
the cancellation property (fifth hypothesis), show that the relation
,
specified by the first hypothesis, is transitive.
(Contributed by NM, 11Feb1996.) (Revised by Mario Carneiro,
26Apr2015.)



Theorem  ecopover 6140* 
Assuming that operation is commutative (second hypothesis),
closed (third hypothesis), associative (fourth hypothesis), and has
the cancellation property (fifth hypothesis), show that the relation
,
specified by the first hypothesis, is an equivalence
relation. (Contributed by NM, 16Feb1996.) (Revised by Mario
Carneiro, 12Aug2015.)



Theorem  ecopovsymg 6141* 
Assuming the operation is commutative, show that the relation
,
specified by the first hypothesis, is symmetric.
(Contributed by Jim Kingdon, 1Sep2019.)



Theorem  ecopovtrng 6142* 
Assuming that operation is commutative (second hypothesis),
closed (third hypothesis), associative (fourth hypothesis), and has
the cancellation property (fifth hypothesis), show that the relation
,
specified by the first hypothesis, is transitive.
(Contributed by Jim Kingdon, 1Sep2019.)



Theorem  ecopoverg 6143* 
Assuming that operation is commutative (second hypothesis),
closed (third hypothesis), associative (fourth hypothesis), and has
the cancellation property (fifth hypothesis), show that the relation
,
specified by the first hypothesis, is an equivalence
relation. (Contributed by Jim Kingdon, 1Sep2019.)



Theorem  th3qlem1 6144* 
Lemma for Exercise 44 version of Theorem 3Q of [Enderton] p. 60. The
third hypothesis is the compatibility assumption. (Contributed by NM,
3Aug1995.) (Revised by Mario Carneiro, 9Jul2014.)



Theorem  th3qlem2 6145* 
Lemma for Exercise 44 version of Theorem 3Q of [Enderton] p. 60,
extended to operations on ordered pairs. The fourth hypothesis is the
compatibility assumption. (Contributed by NM, 4Aug1995.) (Revised by
Mario Carneiro, 12Aug2015.)



Theorem  th3qcor 6146* 
Corollary of Theorem 3Q of [Enderton] p. 60.
(Contributed by NM,
12Nov1995.) (Revised by David Abernethy, 4Jun2013.)



Theorem  th3q 6147* 
Theorem 3Q of [Enderton] p. 60, extended to
operations on ordered
pairs. (Contributed by NM, 4Aug1995.) (Revised by Mario Carneiro,
19Dec2013.)



Theorem  oviec 6148* 
Express an operation on equivalence classes of ordered pairs in terms of
equivalence class of operations on ordered pairs. See iset.mm for
additional comments describing the hypotheses. (Unnecessary distinct
variable restrictions were removed by David Abernethy, 4Jun2013.)
(Contributed by NM, 6Aug1995.) (Revised by Mario Carneiro,
4Jun2013.)



Theorem  ecovcom 6149* 
Lemma used to transfer a commutative law via an equivalence relation.
Most uses will want ecovicom 6150 instead. (Contributed by NM,
29Aug1995.) (Revised by David Abernethy, 4Jun2013.)



Theorem  ecovicom 6150* 
Lemma used to transfer a commutative law via an equivalence relation.
(Contributed by Jim Kingdon, 15Sep2019.)



Theorem  ecovass 6151* 
Lemma used to transfer an associative law via an equivalence relation.
In most cases ecoviass 6152 will be more useful. (Contributed by NM,
31Aug1995.) (Revised by David Abernethy, 4Jun2013.)



Theorem  ecoviass 6152* 
Lemma used to transfer an associative law via an equivalence relation.
(Contributed by Jim Kingdon, 16Sep2019.)



Theorem  ecovdi 6153* 
Lemma used to transfer a distributive law via an equivalence relation.
Most likely ecovidi 6154 will be more helpful. (Contributed by NM,
2Sep1995.) (Revised by David Abernethy, 4Jun2013.)



Theorem  ecovidi 6154* 
Lemma used to transfer a distributive law via an equivalence relation.
(Contributed by Jim Kingdon, 17Sep2019.)



2.6.25 Equinumerosity


Syntax  cen 6155 
Extend class definition to include the equinumerosity relation
("approximately equals" symbol)



Syntax  cdom 6156 
Extend class definition to include the dominance relation (curly
lessthanorequal)



Syntax  cfn 6157 
Extend class definition to include the class of all finite sets.



Definition  dfen 6158* 
Define the equinumerosity relation. Definition of [Enderton] p. 129.
We define
to be a binary relation rather than a connective, so
its arguments must be sets to be meaningful. This is acceptable because
we do not consider equinumerosity for proper classes. We derive the
usual definition as bren 6164. (Contributed by NM, 28Mar1998.)



Definition  dfdom 6159* 
Define the dominance relation. Compare Definition of [Enderton]
p. 145. Typical textbook definitions are derived as brdom 6167 and
domen 6168. (Contributed by NM, 28Mar1998.)



Definition  dffin 6160* 
Define the (proper) class of all finite sets. Similar to Definition
10.29 of [TakeutiZaring] p. 91,
whose "Fin(a)" corresponds to
our " ". This definition is
meaningful whether or not we
accept the Axiom of Infinity axinf2 9436. (Contributed by NM,
22Aug2008.)



Theorem  relen 6161 
Equinumerosity is a relation. (Contributed by NM, 28Mar1998.)



Theorem  reldom 6162 
Dominance is a relation. (Contributed by NM, 28Mar1998.)



Theorem  encv 6163 
If two classes are equinumerous, both classes are sets. (Contributed by
AV, 21Mar2019.)



Theorem  bren 6164* 
Equinumerosity relation. (Contributed by NM, 15Jun1998.)



Theorem  brdomg 6165* 
Dominance relation. (Contributed by NM, 15Jun1998.)



Theorem  brdomi 6166* 
Dominance relation. (Contributed by Mario Carneiro, 26Apr2015.)



Theorem  brdom 6167* 
Dominance relation. (Contributed by NM, 15Jun1998.)



Theorem  domen 6168* 
Dominance in terms of equinumerosity. Example 1 of [Enderton] p. 146.
(Contributed by NM, 15Jun1998.)



Theorem  domeng 6169* 
Dominance in terms of equinumerosity, with the sethood requirement
expressed as an antecedent. Example 1 of [Enderton] p. 146.
(Contributed by NM, 24Apr2004.)



Theorem  f1oen3g 6170 
The domain and range of a onetoone, onto function are equinumerous.
This variation of f1oeng 6173 does not require the Axiom of Replacement.
(Contributed by NM, 13Jan2007.) (Revised by Mario Carneiro,
10Sep2015.)



Theorem  f1oen2g 6171 
The domain and range of a onetoone, onto function are equinumerous.
This variation of f1oeng 6173 does not require the Axiom of Replacement.
(Contributed by Mario Carneiro, 10Sep2015.)



Theorem  f1dom2g 6172 
The domain of a onetoone function is dominated by its codomain. This
variation of f1domg 6174 does not require the Axiom of Replacement.
(Contributed by Mario Carneiro, 24Jun2015.)



Theorem  f1oeng 6173 
The domain and range of a onetoone, onto function are equinumerous.
(Contributed by NM, 19Jun1998.)



Theorem  f1domg 6174 
The domain of a onetoone function is dominated by its codomain.
(Contributed by NM, 4Sep2004.)



Theorem  f1oen 6175 
The domain and range of a onetoone, onto function are equinumerous.
(Contributed by NM, 19Jun1998.)



Theorem  f1dom 6176 
The domain of a onetoone function is dominated by its codomain.
(Contributed by NM, 19Jun1998.)



Theorem  isfi 6177* 
Express " is
finite." Definition 10.29 of [TakeutiZaring] p. 91
(whose " " is a predicate instead of a class). (Contributed by
NM, 22Aug2008.)



Theorem  enssdom 6178 
Equinumerosity implies dominance. (Contributed by NM, 31Mar1998.)



Theorem  endom 6179 
Equinumerosity implies dominance. Theorem 15 of [Suppes] p. 94.
(Contributed by NM, 28May1998.)



Theorem  enrefg 6180 
Equinumerosity is reflexive. Theorem 1 of [Suppes] p. 92. (Contributed
by NM, 18Jun1998.) (Revised by Mario Carneiro, 26Apr2015.)



Theorem  enref 6181 
Equinumerosity is reflexive. Theorem 1 of [Suppes] p. 92. (Contributed
by NM, 25Sep2004.)



Theorem  eqeng 6182 
Equality implies equinumerosity. (Contributed by NM, 26Oct2003.)



Theorem  domrefg 6183 
Dominance is reflexive. (Contributed by NM, 18Jun1998.)



Theorem  en2d 6184* 
Equinumerosity inference from an implicit onetoone onto function.
(Contributed by NM, 27Jul2004.) (Revised by Mario Carneiro,
12May2014.)



Theorem  en3d 6185* 
Equinumerosity inference from an implicit onetoone onto function.
(Contributed by NM, 27Jul2004.) (Revised by Mario Carneiro,
12May2014.)



Theorem  en2i 6186* 
Equinumerosity inference from an implicit onetoone onto function.
(Contributed by NM, 4Jan2004.)



Theorem  en3i 6187* 
Equinumerosity inference from an implicit onetoone onto function.
(Contributed by NM, 19Jul2004.)



Theorem  dom2lem 6188* 
A mapping (first hypothesis) that is onetoone (second hypothesis)
implies its domain is dominated by its codomain. (Contributed by NM,
24Jul2004.)



Theorem  dom2d 6189* 
A mapping (first hypothesis) that is onetoone (second hypothesis)
implies its domain is dominated by its codomain. (Contributed by NM,
24Jul2004.) (Revised by Mario Carneiro, 20May2013.)



Theorem  dom3d 6190* 
A mapping (first hypothesis) that is onetoone (second hypothesis)
implies its domain is dominated by its codomain. (Contributed by Mario
Carneiro, 20May2013.)



Theorem  dom2 6191* 
A mapping (first hypothesis) that is onetoone (second hypothesis)
implies its domain is dominated by its codomain. and can be
read and , as can be inferred from their
distinct variable conditions. (Contributed by NM, 26Oct2003.)



Theorem  dom3 6192* 
A mapping (first hypothesis) that is onetoone (second hypothesis)
implies its domain is dominated by its codomain. and can be
read and , as can be inferred from their
distinct variable conditions. (Contributed by Mario Carneiro,
20May2013.)



Theorem  idssen 6193 
Equality implies equinumerosity. (Contributed by NM, 30Apr1998.)
(Revised by Mario Carneiro, 15Nov2014.)



Theorem  ssdomg 6194 
A set dominates its subsets. Theorem 16 of [Suppes] p. 94.
(Contributed by NM, 19Jun1998.) (Revised by Mario Carneiro,
24Jun2015.)



Theorem  ener 6195 
Equinumerosity is an equivalence relation. (Contributed by NM,
19Mar1998.) (Revised by Mario Carneiro, 15Nov2014.)



Theorem  ensymb 6196 
Symmetry of equinumerosity. Theorem 2 of [Suppes] p. 92. (Contributed by
Mario Carneiro, 26Apr2015.)



Theorem  ensym 6197 
Symmetry of equinumerosity. Theorem 2 of [Suppes] p. 92. (Contributed by
NM, 26Oct2003.) (Revised by Mario Carneiro, 26Apr2015.)



Theorem  ensymi 6198 
Symmetry of equinumerosity. Theorem 2 of [Suppes] p. 92. (Contributed
by NM, 25Sep2004.)



Theorem  ensymd 6199 
Symmetry of equinumerosity. Deduction form of ensym 6197. (Contributed
by David Moews, 1May2017.)



Theorem  entr 6200 
Transitivity of equinumerosity. Theorem 3 of [Suppes] p. 92.
(Contributed by NM, 9Jun1998.)

