Type  Label  Description 
Statement 

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



Theorem  qsid 6202 
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 6203* 
Implicit substitution of class for equivalence class. (Contributed by
Mario Carneiro, 9Jul2014.)



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



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



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



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



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



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



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



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



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



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



Theorem  qsel 6214 
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 6215* 
, a function lift, is
a subset of . (Contributed by
Mario Carneiro, 23Dec2016.)



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



Theorem  ecopoveq 6232* 
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 6233* 
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 6234* 
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 6235* 
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 6236* 
Assuming the operation is commutative, show that the relation
,
specified by the first hypothesis, is symmetric.
(Contributed by Jim Kingdon, 1Sep2019.)



Theorem  ecopovtrng 6237* 
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 6238* 
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 6239* 
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 6240* 
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 6241* 
Corollary of Theorem 3Q of [Enderton] p. 60.
(Contributed by NM,
12Nov1995.) (Revised by David Abernethy, 4Jun2013.)



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



Theorem  oviec 6243* 
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 6244* 
Lemma used to transfer a commutative law via an equivalence relation.
Most uses will want ecovicom 6245 instead. (Contributed by NM,
29Aug1995.) (Revised by David Abernethy, 4Jun2013.)



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



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



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



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



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



2.6.25 Equinumerosity


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



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



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



Definition  dfen 6253* 
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 6259. (Contributed by NM, 28Mar1998.)



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



Definition  dffin 6255* 
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 10488. (Contributed by NM,
22Aug2008.)



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



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



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



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



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



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



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



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



Theorem  domeng 6264* 
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 6265 
The domain and range of a onetoone, onto function are equinumerous.
This variation of f1oeng 6268 does not require the Axiom of Replacement.
(Contributed by NM, 13Jan2007.) (Revised by Mario Carneiro,
10Sep2015.)



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



Theorem  dom2d 6284* 
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 6285* 
A mapping (first hypothesis) that is onetoone (second hypothesis)
implies its domain is dominated by its codomain. (Contributed by Mario
Carneiro, 20May2013.)



Theorem  dom2 6286* 
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 6287* 
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 6288 
Equality implies equinumerosity. (Contributed by NM, 30Apr1998.)
(Revised by Mario Carneiro, 15Nov2014.)



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



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



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



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



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



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



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



Theorem  domtr 6296 
Transitivity of dominance relation. Theorem 17 of [Suppes] p. 94.
(Contributed by NM, 4Jun1998.) (Revised by Mario Carneiro,
15Nov2014.)



Theorem  entri 6297 
A chained equinumerosity inference. (Contributed by NM,
25Sep2004.)



Theorem  entr2i 6298 
A chained equinumerosity inference. (Contributed by NM,
25Sep2004.)



Theorem  entr3i 6299 
A chained equinumerosity inference. (Contributed by NM,
25Sep2004.)



Theorem  entr4i 6300 
A chained equinumerosity inference. (Contributed by NM,
25Sep2004.)

