Theorem List for Intuitionistic Logic Explorer - 6501-6600 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | iinerm 6501* |
The intersection of a nonempty family of equivalence relations is an
equivalence relation. (Contributed by Mario Carneiro, 27-Sep-2015.)
|
|
|
Theorem | riinerm 6502* |
The relative intersection of a family of equivalence relations is an
equivalence relation. (Contributed by Mario Carneiro, 27-Sep-2015.)
|
|
|
Theorem | erinxp 6503 |
A restricted equivalence relation is an equivalence relation.
(Contributed by Mario Carneiro, 10-Jul-2015.) (Revised by Mario
Carneiro, 12-Aug-2015.)
|
|
|
Theorem | ecinxp 6504 |
Restrict the relation in an equivalence class to a base set. (Contributed
by Mario Carneiro, 10-Jul-2015.)
|
|
|
Theorem | qsinxp 6505 |
Restrict the equivalence relation in a quotient set to the base set.
(Contributed by Mario Carneiro, 23-Feb-2015.)
|
|
|
Theorem | qsel 6506 |
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 6507* |
, a function lift, is
a subset of . (Contributed by
Mario Carneiro, 23-Dec-2016.)
|
|
|
Theorem | qliftrel 6508* |
, a function lift, is
a subset of . (Contributed by
Mario Carneiro, 23-Dec-2016.)
|
|
|
Theorem | qliftel 6509* |
Elementhood in the relation . (Contributed by Mario Carneiro,
23-Dec-2016.)
|
|
|
Theorem | qliftel1 6510* |
Elementhood in the relation . (Contributed by Mario Carneiro,
23-Dec-2016.)
|
|
|
Theorem | qliftfun 6511* |
The function is the
unique function defined by
, provided that the well-definedness condition
holds. (Contributed by Mario Carneiro, 23-Dec-2016.)
|
|
|
Theorem | qliftfund 6512* |
The function is the
unique function defined by
, provided that the well-definedness condition
holds. (Contributed by Mario Carneiro, 23-Dec-2016.)
|
|
|
Theorem | qliftfuns 6513* |
The function is the
unique function defined by
, provided that the well-definedness condition
holds.
(Contributed by Mario Carneiro, 23-Dec-2016.)
|
|
|
Theorem | qliftf 6514* |
The domain and range of the function . (Contributed by Mario
Carneiro, 23-Dec-2016.)
|
|
|
Theorem | qliftval 6515* |
The value of the function . (Contributed by Mario Carneiro,
23-Dec-2016.)
|
|
|
Theorem | ecoptocl 6516* |
Implicit substitution of class for equivalence class of ordered pair.
(Contributed by NM, 23-Jul-1995.)
|
|
|
Theorem | 2ecoptocl 6517* |
Implicit substitution of classes for equivalence classes of ordered
pairs. (Contributed by NM, 23-Jul-1995.)
|
|
|
Theorem | 3ecoptocl 6518* |
Implicit substitution of classes for equivalence classes of ordered
pairs. (Contributed by NM, 9-Aug-1995.)
|
|
|
Theorem | brecop 6519* |
Binary relation on a quotient set. Lemma for real number construction.
(Contributed by NM, 29-Jan-1996.)
|
|
|
Theorem | eroveu 6520* |
Lemma for eroprf 6522. (Contributed by Jeff Madsen, 10-Jun-2010.)
(Revised by Mario Carneiro, 9-Jul-2014.)
|
|
|
Theorem | erovlem 6521* |
Lemma for eroprf 6522. (Contributed by Jeff Madsen, 10-Jun-2010.)
(Revised by Mario Carneiro, 30-Dec-2014.)
|
|
|
Theorem | eroprf 6522* |
Functionality of an operation defined on equivalence classes.
(Contributed by Jeff Madsen, 10-Jun-2010.) (Revised by Mario Carneiro,
30-Dec-2014.)
|
|
|
Theorem | eroprf2 6523* |
Functionality of an operation defined on equivalence classes.
(Contributed by Jeff Madsen, 10-Jun-2010.)
|
|
|
Theorem | ecopoveq 6524* |
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 6525* |
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 6526* |
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 6527* |
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 6528* |
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 6529* |
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 6530* |
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 6531* |
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 6532* |
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 6533* |
Corollary of Theorem 3Q of [Enderton] p. 60.
(Contributed by NM,
12-Nov-1995.) (Revised by David Abernethy, 4-Jun-2013.)
|
|
|
Theorem | th3q 6534* |
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 6535* |
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 6536* |
Lemma used to transfer a commutative law via an equivalence relation.
Most uses will want ecovicom 6537 instead. (Contributed by NM,
29-Aug-1995.) (Revised by David Abernethy, 4-Jun-2013.)
|
|
|
Theorem | ecovicom 6537* |
Lemma used to transfer a commutative law via an equivalence relation.
(Contributed by Jim Kingdon, 15-Sep-2019.)
|
|
|
Theorem | ecovass 6538* |
Lemma used to transfer an associative law via an equivalence relation.
In most cases ecoviass 6539 will be more useful. (Contributed by NM,
31-Aug-1995.) (Revised by David Abernethy, 4-Jun-2013.)
|
|
|
Theorem | ecoviass 6539* |
Lemma used to transfer an associative law via an equivalence relation.
(Contributed by Jim Kingdon, 16-Sep-2019.)
|
|
|
Theorem | ecovdi 6540* |
Lemma used to transfer a distributive law via an equivalence relation.
Most likely ecovidi 6541 will be more helpful. (Contributed by NM,
2-Sep-1995.) (Revised by David Abernethy, 4-Jun-2013.)
|
|
|
Theorem | ecovidi 6541* |
Lemma used to transfer a distributive law via an equivalence relation.
(Contributed by Jim Kingdon, 17-Sep-2019.)
|
|
|
2.6.25 The mapping operation
|
|
Syntax | cmap 6542 |
Extend the definition of a class to include the mapping operation. (Read
for , "the set of all functions that map
from to
.)
|
|
|
Syntax | cpm 6543 |
Extend the definition of a class to include the partial mapping operation.
(Read for , "the set of all partial functions
that map from
to .)
|
|
|
Definition | df-map 6544* |
Define the mapping operation or set exponentiation. The set of all
functions that map from to is
written (see
mapval 6554). Many authors write followed by as a superscript
for this operation and rely on context to avoid confusion other
exponentiation operations (e.g., Definition 10.42 of [TakeutiZaring]
p. 95). Other authors show as a prefixed superscript, which is
read " pre
" (e.g.,
definition of [Enderton] p. 52).
Definition 8.21 of [Eisenberg] p. 125
uses the notation Map(,
) for our . The up-arrow is used by
Donald Knuth
for iterated exponentiation (Science 194, 1235-1242, 1976). We
adopt
the first case of his notation (simple exponentiation) and subscript it
with m to distinguish it from other kinds of exponentiation.
(Contributed by NM, 8-Dec-2003.)
|
|
|
Definition | df-pm 6545* |
Define the partial mapping operation. A partial function from to
is a function
from a subset of to
. The set of all
partial functions from to is
written (see
pmvalg 6553). A notation for this operation apparently
does not appear in
the literature. We use to distinguish it from the less general
set exponentiation operation (df-map 6544) . See mapsspm 6576 for
its relationship to set exponentiation. (Contributed by NM,
15-Nov-2007.)
|
|
|
Theorem | mapprc 6546* |
When is a proper
class, the class of all functions mapping
to is empty.
Exercise 4.41 of [Mendelson] p. 255.
(Contributed
by NM, 8-Dec-2003.)
|
|
|
Theorem | pmex 6547* |
The class of all partial functions from one set to another is a set.
(Contributed by NM, 15-Nov-2007.)
|
|
|
Theorem | mapex 6548* |
The class of all functions mapping one set to another is a set. Remark
after Definition 10.24 of [Kunen] p. 31.
(Contributed by Raph Levien,
4-Dec-2003.)
|
|
|
Theorem | fnmap 6549 |
Set exponentiation has a universal domain. (Contributed by NM,
8-Dec-2003.) (Revised by Mario Carneiro, 8-Sep-2013.)
|
|
|
Theorem | fnpm 6550 |
Partial function exponentiation has a universal domain. (Contributed by
Mario Carneiro, 14-Nov-2013.)
|
|
|
Theorem | reldmmap 6551 |
Set exponentiation is a well-behaved binary operator. (Contributed by
Stefan O'Rear, 27-Feb-2015.)
|
|
|
Theorem | mapvalg 6552* |
The value of set exponentiation. is the set of all
functions that map from to .
Definition 10.24 of [Kunen]
p. 24. (Contributed by NM, 8-Dec-2003.) (Revised by Mario Carneiro,
8-Sep-2013.)
|
|
|
Theorem | pmvalg 6553* |
The value of the partial mapping operation.
is the set
of all partial functions that map from to . (Contributed by
NM, 15-Nov-2007.) (Revised by Mario Carneiro, 8-Sep-2013.)
|
|
|
Theorem | mapval 6554* |
The value of set exponentiation (inference version). is
the set of all functions that map from to . Definition
10.24 of [Kunen] p. 24. (Contributed by
NM, 8-Dec-2003.)
|
|
|
Theorem | elmapg 6555 |
Membership relation for set exponentiation. (Contributed by NM,
17-Oct-2006.) (Revised by Mario Carneiro, 15-Nov-2014.)
|
|
|
Theorem | elmapd 6556 |
Deduction form of elmapg 6555. (Contributed by BJ, 11-Apr-2020.)
|
|
|
Theorem | mapdm0 6557 |
The empty set is the only map with empty domain. (Contributed by Glauco
Siliprandi, 11-Oct-2020.) (Proof shortened by Thierry Arnoux,
3-Dec-2021.)
|
|
|
Theorem | elpmg 6558 |
The predicate "is a partial function." (Contributed by Mario
Carneiro,
14-Nov-2013.)
|
|
|
Theorem | elpm2g 6559 |
The predicate "is a partial function." (Contributed by NM,
31-Dec-2013.)
|
|
|
Theorem | elpm2r 6560 |
Sufficient condition for being a partial function. (Contributed by NM,
31-Dec-2013.)
|
|
|
Theorem | elpmi 6561 |
A partial function is a function. (Contributed by Mario Carneiro,
15-Sep-2015.)
|
|
|
Theorem | pmfun 6562 |
A partial function is a function. (Contributed by Mario Carneiro,
30-Jan-2014.) (Revised by Mario Carneiro, 26-Apr-2015.)
|
|
|
Theorem | elmapex 6563 |
Eliminate antecedent for mapping theorems: domain can be taken to be a
set. (Contributed by Stefan O'Rear, 8-Oct-2014.)
|
|
|
Theorem | elmapi 6564 |
A mapping is a function, forward direction only with superfluous
antecedent removed. (Contributed by Stefan O'Rear, 10-Oct-2014.)
|
|
|
Theorem | elmapfn 6565 |
A mapping is a function with the appropriate domain. (Contributed by AV,
6-Apr-2019.)
|
|
|
Theorem | elmapfun 6566 |
A mapping is always a function. (Contributed by Stefan O'Rear,
9-Oct-2014.) (Revised by Stefan O'Rear, 5-May-2015.)
|
|
|
Theorem | elmapssres 6567 |
A restricted mapping is a mapping. (Contributed by Stefan O'Rear,
9-Oct-2014.) (Revised by Mario Carneiro, 5-May-2015.)
|
|
|
Theorem | fpmg 6568 |
A total function is a partial function. (Contributed by Mario Carneiro,
31-Dec-2013.)
|
|
|
Theorem | pmss12g 6569 |
Subset relation for the set of partial functions. (Contributed by Mario
Carneiro, 31-Dec-2013.)
|
|
|
Theorem | pmresg 6570 |
Elementhood of a restricted function in the set of partial functions.
(Contributed by Mario Carneiro, 31-Dec-2013.)
|
|
|
Theorem | elmap 6571 |
Membership relation for set exponentiation. (Contributed by NM,
8-Dec-2003.)
|
|
|
Theorem | mapval2 6572* |
Alternate expression for the value of set exponentiation. (Contributed
by NM, 3-Nov-2007.)
|
|
|
Theorem | elpm 6573 |
The predicate "is a partial function." (Contributed by NM,
15-Nov-2007.) (Revised by Mario Carneiro, 14-Nov-2013.)
|
|
|
Theorem | elpm2 6574 |
The predicate "is a partial function." (Contributed by NM,
15-Nov-2007.) (Revised by Mario Carneiro, 31-Dec-2013.)
|
|
|
Theorem | fpm 6575 |
A total function is a partial function. (Contributed by NM,
15-Nov-2007.) (Revised by Mario Carneiro, 31-Dec-2013.)
|
|
|
Theorem | mapsspm 6576 |
Set exponentiation is a subset of partial maps. (Contributed by NM,
15-Nov-2007.) (Revised by Mario Carneiro, 27-Feb-2016.)
|
|
|
Theorem | pmsspw 6577 |
Partial maps are a subset of the power set of the Cartesian product of
its arguments. (Contributed by Mario Carneiro, 2-Jan-2017.)
|
|
|
Theorem | mapsspw 6578 |
Set exponentiation is a subset of the power set of the Cartesian product
of its arguments. (Contributed by NM, 8-Dec-2006.) (Revised by Mario
Carneiro, 26-Apr-2015.)
|
|
|
Theorem | fvmptmap 6579* |
Special case of fvmpt 5498 for operator theorems. (Contributed by NM,
27-Nov-2007.)
|
|
|
Theorem | map0e 6580 |
Set exponentiation with an empty exponent (ordinal number 0) is ordinal
number 1. Exercise 4.42(a) of [Mendelson] p. 255. (Contributed by NM,
10-Dec-2003.) (Revised by Mario Carneiro, 30-Apr-2015.)
|
|
|
Theorem | map0b 6581 |
Set exponentiation with an empty base is the empty set, provided the
exponent is nonempty. Theorem 96 of [Suppes] p. 89. (Contributed by
NM, 10-Dec-2003.) (Revised by Mario Carneiro, 26-Apr-2015.)
|
|
|
Theorem | map0g 6582 |
Set exponentiation is empty iff the base is empty and the exponent is
not empty. Theorem 97 of [Suppes] p. 89.
(Contributed by Mario
Carneiro, 30-Apr-2015.)
|
|
|
Theorem | map0 6583 |
Set exponentiation is empty iff the base is empty and the exponent is
not empty. Theorem 97 of [Suppes] p. 89.
(Contributed by NM,
10-Dec-2003.)
|
|
|
Theorem | mapsn 6584* |
The value of set exponentiation with a singleton exponent. Theorem 98
of [Suppes] p. 89. (Contributed by NM,
10-Dec-2003.)
|
|
|
Theorem | mapss 6585 |
Subset inheritance for set exponentiation. Theorem 99 of [Suppes]
p. 89. (Contributed by NM, 10-Dec-2003.) (Revised by Mario Carneiro,
26-Apr-2015.)
|
|
|
Theorem | fdiagfn 6586* |
Functionality of the diagonal map. (Contributed by Stefan O'Rear,
24-Jan-2015.)
|
|
|
Theorem | fvdiagfn 6587* |
Functionality of the diagonal map. (Contributed by Stefan O'Rear,
24-Jan-2015.)
|
|
|
Theorem | mapsnconst 6588 |
Every singleton map is a constant function. (Contributed by Stefan
O'Rear, 25-Mar-2015.)
|
|
|
Theorem | mapsncnv 6589* |
Expression for the inverse of the canonical map between a set and its
set of singleton functions. (Contributed by Stefan O'Rear,
21-Mar-2015.)
|
|
|
Theorem | mapsnf1o2 6590* |
Explicit bijection between a set and its singleton functions.
(Contributed by Stefan O'Rear, 21-Mar-2015.)
|
|
|
Theorem | mapsnf1o3 6591* |
Explicit bijection in the reverse of mapsnf1o2 6590. (Contributed by
Stefan O'Rear, 24-Mar-2015.)
|
|
|
2.6.26 Infinite Cartesian products
|
|
Syntax | cixp 6592 |
Extend class notation to include infinite Cartesian products.
|
|
|
Definition | df-ixp 6593* |
Definition of infinite Cartesian product of [Enderton] p. 54. Enderton
uses a bold "X" with
written underneath or
as a subscript, as
does Stoll p. 47. Some books use a capital pi, but we will reserve that
notation for products of numbers. Usually represents a class
expression containing free and thus can be thought of as
. Normally,
is not free in ,
although this is
not a requirement of the definition. (Contributed by NM,
28-Sep-2006.)
|
|
|
Theorem | dfixp 6594* |
Eliminate the expression in df-ixp 6593, under the
assumption that and are
disjoint. This way, we can say that
is bound in
even if it
appears free in .
(Contributed by Mario Carneiro, 12-Aug-2016.)
|
|
|
Theorem | ixpsnval 6595* |
The value of an infinite Cartesian product with a singleton.
(Contributed by AV, 3-Dec-2018.)
|
|
|
Theorem | elixp2 6596* |
Membership in an infinite Cartesian product. See df-ixp 6593 for
discussion of the notation. (Contributed by NM, 28-Sep-2006.)
|
|
|
Theorem | fvixp 6597* |
Projection of a factor of an indexed Cartesian product. (Contributed by
Mario Carneiro, 11-Jun-2016.)
|
|
|
Theorem | ixpfn 6598* |
A nuple is a function. (Contributed by FL, 6-Jun-2011.) (Revised by
Mario Carneiro, 31-May-2014.)
|
|
|
Theorem | elixp 6599* |
Membership in an infinite Cartesian product. (Contributed by NM,
28-Sep-2006.)
|
|
|
Theorem | elixpconst 6600* |
Membership in an infinite Cartesian product of a constant .
(Contributed by NM, 12-Apr-2008.)
|
|