Theorem List for Intuitionistic Logic Explorer - 6201-6300 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | iinerm 6201* |
The intersection of a nonempty family of equivalence relations is an
equivalence relation. (Contributed by Mario Carneiro, 27-Sep-2015.)
|
|
|
Theorem | riinerm 6202* |
The relative intersection of a family of equivalence relations is an
equivalence relation. (Contributed by Mario Carneiro, 27-Sep-2015.)
|
|
|
Theorem | erinxp 6203 |
A restricted equivalence relation is an equivalence relation.
(Contributed by Mario Carneiro, 10-Jul-2015.) (Revised by Mario
Carneiro, 12-Aug-2015.)
|
|
|
Theorem | ecinxp 6204 |
Restrict the relation in an equivalence class to a base set. (Contributed
by Mario Carneiro, 10-Jul-2015.)
|
|
|
Theorem | qsinxp 6205 |
Restrict the equivalence relation in a quotient set to the base set.
(Contributed by Mario Carneiro, 23-Feb-2015.)
|
|
|
Theorem | qsel 6206 |
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 6207* |
, a function lift, is
a subset of . (Contributed by
Mario Carneiro, 23-Dec-2016.)
|
|
|
Theorem | qliftrel 6208* |
, a function lift, is
a subset of . (Contributed by
Mario Carneiro, 23-Dec-2016.)
|
|
|
Theorem | qliftel 6209* |
Elementhood in the relation . (Contributed by Mario Carneiro,
23-Dec-2016.)
|
|
|
Theorem | qliftel1 6210* |
Elementhood in the relation . (Contributed by Mario Carneiro,
23-Dec-2016.)
|
|
|
Theorem | qliftfun 6211* |
The function is the
unique function defined by
, provided that the well-definedness condition
holds. (Contributed by Mario Carneiro, 23-Dec-2016.)
|
|
|
Theorem | qliftfund 6212* |
The function is the
unique function defined by
, provided that the well-definedness condition
holds. (Contributed by Mario Carneiro, 23-Dec-2016.)
|
|
|
Theorem | qliftfuns 6213* |
The function is the
unique function defined by
, provided that the well-definedness condition
holds.
(Contributed by Mario Carneiro, 23-Dec-2016.)
|
|
|
Theorem | qliftf 6214* |
The domain and range of the function . (Contributed by Mario
Carneiro, 23-Dec-2016.)
|
|
|
Theorem | qliftval 6215* |
The value of the function . (Contributed by Mario Carneiro,
23-Dec-2016.)
|
|
|
Theorem | ecoptocl 6216* |
Implicit substitution of class for equivalence class of ordered pair.
(Contributed by NM, 23-Jul-1995.)
|
|
|
Theorem | 2ecoptocl 6217* |
Implicit substitution of classes for equivalence classes of ordered
pairs. (Contributed by NM, 23-Jul-1995.)
|
|
|
Theorem | 3ecoptocl 6218* |
Implicit substitution of classes for equivalence classes of ordered
pairs. (Contributed by NM, 9-Aug-1995.)
|
|
|
Theorem | brecop 6219* |
Binary relation on a quotient set. Lemma for real number construction.
(Contributed by NM, 29-Jan-1996.)
|
|
|
Theorem | eroveu 6220* |
Lemma for eroprf 6222. (Contributed by Jeff Madsen, 10-Jun-2010.)
(Revised by Mario Carneiro, 9-Jul-2014.)
|
|
|
Theorem | erovlem 6221* |
Lemma for eroprf 6222. (Contributed by Jeff Madsen, 10-Jun-2010.)
(Revised by Mario Carneiro, 30-Dec-2014.)
|
|
|
Theorem | eroprf 6222* |
Functionality of an operation defined on equivalence classes.
(Contributed by Jeff Madsen, 10-Jun-2010.) (Revised by Mario Carneiro,
30-Dec-2014.)
|
|
|
Theorem | eroprf2 6223* |
Functionality of an operation defined on equivalence classes.
(Contributed by Jeff Madsen, 10-Jun-2010.)
|
|
|
Theorem | ecopoveq 6224* |
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, 16-Aug-1995.)
|
|
|
Theorem | ecopovsym 6225* |
Assuming the operation is commutative, show that the relation
,
specified by the first hypothesis, is symmetric.
(Contributed by NM, 27-Aug-1995.) (Revised by Mario Carneiro,
26-Apr-2015.)
|
|
|
Theorem | ecopovtrn 6226* |
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, 11-Feb-1996.) (Revised by Mario Carneiro,
26-Apr-2015.)
|
|
|
Theorem | ecopover 6227* |
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, 16-Feb-1996.) (Revised by Mario
Carneiro, 12-Aug-2015.)
|
|
|
Theorem | ecopovsymg 6228* |
Assuming the operation is commutative, show that the relation
,
specified by the first hypothesis, is symmetric.
(Contributed by Jim Kingdon, 1-Sep-2019.)
|
|
|
Theorem | ecopovtrng 6229* |
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, 1-Sep-2019.)
|
|
|
Theorem | ecopoverg 6230* |
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, 1-Sep-2019.)
|
|
|
Theorem | th3qlem1 6231* |
Lemma for Exercise 44 version of Theorem 3Q of [Enderton] p. 60. The
third hypothesis is the compatibility assumption. (Contributed by NM,
3-Aug-1995.) (Revised by Mario Carneiro, 9-Jul-2014.)
|
|
|
Theorem | th3qlem2 6232* |
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, 4-Aug-1995.) (Revised by
Mario Carneiro, 12-Aug-2015.)
|
|
|
Theorem | th3qcor 6233* |
Corollary of Theorem 3Q of [Enderton] p. 60.
(Contributed by NM,
12-Nov-1995.) (Revised by David Abernethy, 4-Jun-2013.)
|
|
|
Theorem | th3q 6234* |
Theorem 3Q of [Enderton] p. 60, extended to
operations on ordered
pairs. (Contributed by NM, 4-Aug-1995.) (Revised by Mario Carneiro,
19-Dec-2013.)
|
|
|
Theorem | oviec 6235* |
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, 4-Jun-2013.)
(Contributed by NM, 6-Aug-1995.) (Revised by Mario Carneiro,
4-Jun-2013.)
|
|
|
Theorem | ecovcom 6236* |
Lemma used to transfer a commutative law via an equivalence relation.
Most uses will want ecovicom 6237 instead. (Contributed by NM,
29-Aug-1995.) (Revised by David Abernethy, 4-Jun-2013.)
|
|
|
Theorem | ecovicom 6237* |
Lemma used to transfer a commutative law via an equivalence relation.
(Contributed by Jim Kingdon, 15-Sep-2019.)
|
|
|
Theorem | ecovass 6238* |
Lemma used to transfer an associative law via an equivalence relation.
In most cases ecoviass 6239 will be more useful. (Contributed by NM,
31-Aug-1995.) (Revised by David Abernethy, 4-Jun-2013.)
|
|
|
Theorem | ecoviass 6239* |
Lemma used to transfer an associative law via an equivalence relation.
(Contributed by Jim Kingdon, 16-Sep-2019.)
|
|
|
Theorem | ecovdi 6240* |
Lemma used to transfer a distributive law via an equivalence relation.
Most likely ecovidi 6241 will be more helpful. (Contributed by NM,
2-Sep-1995.) (Revised by David Abernethy, 4-Jun-2013.)
|
|
|
Theorem | ecovidi 6241* |
Lemma used to transfer a distributive law via an equivalence relation.
(Contributed by Jim Kingdon, 17-Sep-2019.)
|
|
|
2.6.25 Equinumerosity
|
|
Syntax | cen 6242 |
Extend class definition to include the equinumerosity relation
("approximately equals" symbol)
|
|
|
Syntax | cdom 6243 |
Extend class definition to include the dominance relation (curly
less-than-or-equal)
|
|
|
Syntax | cfn 6244 |
Extend class definition to include the class of all finite sets.
|
|
|
Definition | df-en 6245* |
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 6251. (Contributed by NM, 28-Mar-1998.)
|
|
|
Definition | df-dom 6246* |
Define the dominance relation. Compare Definition of [Enderton] p. 145.
Typical textbook definitions are derived as brdom 6254 and domen 6255.
(Contributed by NM, 28-Mar-1998.)
|
|
|
Definition | df-fin 6247* |
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 ax-inf2 10771. (Contributed by NM,
22-Aug-2008.)
|
|
|
Theorem | relen 6248 |
Equinumerosity is a relation. (Contributed by NM, 28-Mar-1998.)
|
|
|
Theorem | reldom 6249 |
Dominance is a relation. (Contributed by NM, 28-Mar-1998.)
|
|
|
Theorem | encv 6250 |
If two classes are equinumerous, both classes are sets. (Contributed by
AV, 21-Mar-2019.)
|
|
|
Theorem | bren 6251* |
Equinumerosity relation. (Contributed by NM, 15-Jun-1998.)
|
|
|
Theorem | brdomg 6252* |
Dominance relation. (Contributed by NM, 15-Jun-1998.)
|
|
|
Theorem | brdomi 6253* |
Dominance relation. (Contributed by Mario Carneiro, 26-Apr-2015.)
|
|
|
Theorem | brdom 6254* |
Dominance relation. (Contributed by NM, 15-Jun-1998.)
|
|
|
Theorem | domen 6255* |
Dominance in terms of equinumerosity. Example 1 of [Enderton] p. 146.
(Contributed by NM, 15-Jun-1998.)
|
|
|
Theorem | domeng 6256* |
Dominance in terms of equinumerosity, with the sethood requirement
expressed as an antecedent. Example 1 of [Enderton] p. 146.
(Contributed by NM, 24-Apr-2004.)
|
|
|
Theorem | f1oen3g 6257 |
The domain and range of a one-to-one, onto function are equinumerous.
This variation of f1oeng 6260 does not require the Axiom of Replacement.
(Contributed by NM, 13-Jan-2007.) (Revised by Mario Carneiro,
10-Sep-2015.)
|
|
|
Theorem | f1oen2g 6258 |
The domain and range of a one-to-one, onto function are equinumerous.
This variation of f1oeng 6260 does not require the Axiom of Replacement.
(Contributed by Mario Carneiro, 10-Sep-2015.)
|
|
|
Theorem | f1dom2g 6259 |
The domain of a one-to-one function is dominated by its codomain. This
variation of f1domg 6261 does not require the Axiom of Replacement.
(Contributed by Mario Carneiro, 24-Jun-2015.)
|
|
|
Theorem | f1oeng 6260 |
The domain and range of a one-to-one, onto function are equinumerous.
(Contributed by NM, 19-Jun-1998.)
|
|
|
Theorem | f1domg 6261 |
The domain of a one-to-one function is dominated by its codomain.
(Contributed by NM, 4-Sep-2004.)
|
|
|
Theorem | f1oen 6262 |
The domain and range of a one-to-one, onto function are equinumerous.
(Contributed by NM, 19-Jun-1998.)
|
|
|
Theorem | f1dom 6263 |
The domain of a one-to-one function is dominated by its codomain.
(Contributed by NM, 19-Jun-1998.)
|
|
|
Theorem | isfi 6264* |
Express " is
finite." Definition 10.29 of [TakeutiZaring] p. 91
(whose " " is a predicate instead of a class). (Contributed by
NM, 22-Aug-2008.)
|
|
|
Theorem | enssdom 6265 |
Equinumerosity implies dominance. (Contributed by NM, 31-Mar-1998.)
|
|
|
Theorem | endom 6266 |
Equinumerosity implies dominance. Theorem 15 of [Suppes] p. 94.
(Contributed by NM, 28-May-1998.)
|
|
|
Theorem | enrefg 6267 |
Equinumerosity is reflexive. Theorem 1 of [Suppes] p. 92. (Contributed
by NM, 18-Jun-1998.) (Revised by Mario Carneiro, 26-Apr-2015.)
|
|
|
Theorem | enref 6268 |
Equinumerosity is reflexive. Theorem 1 of [Suppes] p. 92. (Contributed
by NM, 25-Sep-2004.)
|
|
|
Theorem | eqeng 6269 |
Equality implies equinumerosity. (Contributed by NM, 26-Oct-2003.)
|
|
|
Theorem | domrefg 6270 |
Dominance is reflexive. (Contributed by NM, 18-Jun-1998.)
|
|
|
Theorem | en2d 6271* |
Equinumerosity inference from an implicit one-to-one onto function.
(Contributed by NM, 27-Jul-2004.) (Revised by Mario Carneiro,
12-May-2014.)
|
|
|
Theorem | en3d 6272* |
Equinumerosity inference from an implicit one-to-one onto function.
(Contributed by NM, 27-Jul-2004.) (Revised by Mario Carneiro,
12-May-2014.)
|
|
|
Theorem | en2i 6273* |
Equinumerosity inference from an implicit one-to-one onto function.
(Contributed by NM, 4-Jan-2004.)
|
|
|
Theorem | en3i 6274* |
Equinumerosity inference from an implicit one-to-one onto function.
(Contributed by NM, 19-Jul-2004.)
|
|
|
Theorem | dom2lem 6275* |
A mapping (first hypothesis) that is one-to-one (second hypothesis)
implies its domain is dominated by its codomain. (Contributed by NM,
24-Jul-2004.)
|
|
|
Theorem | dom2d 6276* |
A mapping (first hypothesis) that is one-to-one (second hypothesis)
implies its domain is dominated by its codomain. (Contributed by NM,
24-Jul-2004.) (Revised by Mario Carneiro, 20-May-2013.)
|
|
|
Theorem | dom3d 6277* |
A mapping (first hypothesis) that is one-to-one (second hypothesis)
implies its domain is dominated by its codomain. (Contributed by Mario
Carneiro, 20-May-2013.)
|
|
|
Theorem | dom2 6278* |
A mapping (first hypothesis) that is one-to-one (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, 26-Oct-2003.)
|
|
|
Theorem | dom3 6279* |
A mapping (first hypothesis) that is one-to-one (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,
20-May-2013.)
|
|
|
Theorem | idssen 6280 |
Equality implies equinumerosity. (Contributed by NM, 30-Apr-1998.)
(Revised by Mario Carneiro, 15-Nov-2014.)
|
|
|
Theorem | ssdomg 6281 |
A set dominates its subsets. Theorem 16 of [Suppes] p. 94. (Contributed
by NM, 19-Jun-1998.) (Revised by Mario Carneiro, 24-Jun-2015.)
|
|
|
Theorem | ener 6282 |
Equinumerosity is an equivalence relation. (Contributed by NM,
19-Mar-1998.) (Revised by Mario Carneiro, 15-Nov-2014.)
|
|
|
Theorem | ensymb 6283 |
Symmetry of equinumerosity. Theorem 2 of [Suppes] p. 92. (Contributed by
Mario Carneiro, 26-Apr-2015.)
|
|
|
Theorem | ensym 6284 |
Symmetry of equinumerosity. Theorem 2 of [Suppes] p. 92. (Contributed by
NM, 26-Oct-2003.) (Revised by Mario Carneiro, 26-Apr-2015.)
|
|
|
Theorem | ensymi 6285 |
Symmetry of equinumerosity. Theorem 2 of [Suppes] p. 92. (Contributed
by NM, 25-Sep-2004.)
|
|
|
Theorem | ensymd 6286 |
Symmetry of equinumerosity. Deduction form of ensym 6284. (Contributed
by David Moews, 1-May-2017.)
|
|
|
Theorem | entr 6287 |
Transitivity of equinumerosity. Theorem 3 of [Suppes] p. 92.
(Contributed by NM, 9-Jun-1998.)
|
|
|
Theorem | domtr 6288 |
Transitivity of dominance relation. Theorem 17 of [Suppes] p. 94.
(Contributed by NM, 4-Jun-1998.) (Revised by Mario Carneiro,
15-Nov-2014.)
|
|
|
Theorem | entri 6289 |
A chained equinumerosity inference. (Contributed by NM,
25-Sep-2004.)
|
|
|
Theorem | entr2i 6290 |
A chained equinumerosity inference. (Contributed by NM,
25-Sep-2004.)
|
|
|
Theorem | entr3i 6291 |
A chained equinumerosity inference. (Contributed by NM,
25-Sep-2004.)
|
|
|
Theorem | entr4i 6292 |
A chained equinumerosity inference. (Contributed by NM,
25-Sep-2004.)
|
|
|
Theorem | endomtr 6293 |
Transitivity of equinumerosity and dominance. (Contributed by NM,
7-Jun-1998.)
|
|
|
Theorem | domentr 6294 |
Transitivity of dominance and equinumerosity. (Contributed by NM,
7-Jun-1998.)
|
|
|
Theorem | f1imaeng 6295 |
A one-to-one function's image under a subset of its domain is equinumerous
to the subset. (Contributed by Mario Carneiro, 15-May-2015.)
|
|
|
Theorem | f1imaen2g 6296 |
A one-to-one function's image under a subset of its domain is equinumerous
to the subset. (This version of f1imaen 6297 does not need ax-setind 4280.)
(Contributed by Mario Carneiro, 16-Nov-2014.) (Revised by Mario Carneiro,
25-Jun-2015.)
|
|
|
Theorem | f1imaen 6297 |
A one-to-one function's image under a subset of its domain is
equinumerous to the subset. (Contributed by NM, 30-Sep-2004.)
|
|
|
Theorem | en0 6298 |
The empty set is equinumerous only to itself. Exercise 1 of
[TakeutiZaring] p. 88.
(Contributed by NM, 27-May-1998.)
|
|
|
Theorem | ensn1 6299 |
A singleton is equinumerous to ordinal one. (Contributed by NM,
4-Nov-2002.)
|
|
|
Theorem | ensn1g 6300 |
A singleton is equinumerous to ordinal one. (Contributed by NM,
23-Apr-2004.)
|
|