Theorem List for Intuitionistic Logic Explorer - 6001-6100 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | offres 6001 |
Pointwise combination commutes with restriction. (Contributed by Stefan
O'Rear, 24-Jan-2015.)
|
|
|
Theorem | ofmres 6002* |
Equivalent expressions for a restriction of the function operation map.
Unlike which is a proper class,
can
be a set by ofmresex 6003, allowing it to be used as a function or
structure argument. By ofmresval 5961, the restricted operation map
values are the same as the original values, allowing theorems for
to be reused. (Contributed by NM, 20-Oct-2014.)
|
|
|
Theorem | ofmresex 6003 |
Existence of a restriction of the function operation map. (Contributed
by NM, 20-Oct-2014.)
|
|
|
2.6.14 First and second members of an ordered
pair
|
|
Syntax | c1st 6004 |
Extend the definition of a class to include the first member an ordered
pair function.
|
|
|
Syntax | c2nd 6005 |
Extend the definition of a class to include the second member an ordered
pair function.
|
|
|
Definition | df-1st 6006 |
Define a function that extracts the first member, or abscissa, of an
ordered pair. Theorem op1st 6012 proves that it does this. For example,
( 3 , 4 ) = 3 . Equivalent to Definition
5.13 (i) of
[Monk1] p. 52 (compare op1sta 4990 and op1stb 4369). The notation is the same
as Monk's. (Contributed by NM, 9-Oct-2004.)
|
|
|
Definition | df-2nd 6007 |
Define a function that extracts the second member, or ordinate, of an
ordered pair. Theorem op2nd 6013 proves that it does this. For example,
3 , 4 ) = 4 . Equivalent to Definition 5.13 (ii)
of [Monk1] p. 52 (compare op2nda 4993 and op2ndb 4992). The notation is the
same as Monk's. (Contributed by NM, 9-Oct-2004.)
|
|
|
Theorem | 1stvalg 6008 |
The value of the function that extracts the first member of an ordered
pair. (Contributed by NM, 9-Oct-2004.) (Revised by Mario Carneiro,
8-Sep-2013.)
|
|
|
Theorem | 2ndvalg 6009 |
The value of the function that extracts the second member of an ordered
pair. (Contributed by NM, 9-Oct-2004.) (Revised by Mario Carneiro,
8-Sep-2013.)
|
|
|
Theorem | 1st0 6010 |
The value of the first-member function at the empty set. (Contributed by
NM, 23-Apr-2007.)
|
|
|
Theorem | 2nd0 6011 |
The value of the second-member function at the empty set. (Contributed by
NM, 23-Apr-2007.)
|
|
|
Theorem | op1st 6012 |
Extract the first member of an ordered pair. (Contributed by NM,
5-Oct-2004.)
|
|
|
Theorem | op2nd 6013 |
Extract the second member of an ordered pair. (Contributed by NM,
5-Oct-2004.)
|
|
|
Theorem | op1std 6014 |
Extract the first member of an ordered pair. (Contributed by Mario
Carneiro, 31-Aug-2015.)
|
|
|
Theorem | op2ndd 6015 |
Extract the second member of an ordered pair. (Contributed by Mario
Carneiro, 31-Aug-2015.)
|
|
|
Theorem | op1stg 6016 |
Extract the first member of an ordered pair. (Contributed by NM,
19-Jul-2005.)
|
|
|
Theorem | op2ndg 6017 |
Extract the second member of an ordered pair. (Contributed by NM,
19-Jul-2005.)
|
|
|
Theorem | ot1stg 6018 |
Extract the first member of an ordered triple. (Due to infrequent
usage, it isn't worthwhile at this point to define special extractors
for triples, so we reuse the ordered pair extractors for ot1stg 6018,
ot2ndg 6019, ot3rdgg 6020.) (Contributed by NM, 3-Apr-2015.) (Revised
by
Mario Carneiro, 2-May-2015.)
|
|
|
Theorem | ot2ndg 6019 |
Extract the second member of an ordered triple. (See ot1stg 6018 comment.)
(Contributed by NM, 3-Apr-2015.) (Revised by Mario Carneiro,
2-May-2015.)
|
|
|
Theorem | ot3rdgg 6020 |
Extract the third member of an ordered triple. (See ot1stg 6018 comment.)
(Contributed by NM, 3-Apr-2015.)
|
|
|
Theorem | 1stval2 6021 |
Alternate value of the function that extracts the first member of an
ordered pair. Definition 5.13 (i) of [Monk1] p. 52. (Contributed by
NM, 18-Aug-2006.)
|
|
|
Theorem | 2ndval2 6022 |
Alternate value of the function that extracts the second member of an
ordered pair. Definition 5.13 (ii) of [Monk1] p. 52. (Contributed by
NM, 18-Aug-2006.)
|
|
|
Theorem | fo1st 6023 |
The function
maps the universe onto the universe. (Contributed
by NM, 14-Oct-2004.) (Revised by Mario Carneiro, 8-Sep-2013.)
|
|
|
Theorem | fo2nd 6024 |
The function
maps the universe onto the universe. (Contributed
by NM, 14-Oct-2004.) (Revised by Mario Carneiro, 8-Sep-2013.)
|
|
|
Theorem | f1stres 6025 |
Mapping of a restriction of the (first member of an ordered
pair) function. (Contributed by NM, 11-Oct-2004.) (Revised by Mario
Carneiro, 8-Sep-2013.)
|
|
|
Theorem | f2ndres 6026 |
Mapping of a restriction of the (second member of an ordered
pair) function. (Contributed by NM, 7-Aug-2006.) (Revised by Mario
Carneiro, 8-Sep-2013.)
|
|
|
Theorem | fo1stresm 6027* |
Onto mapping of a restriction of the (first member of an ordered
pair) function. (Contributed by Jim Kingdon, 24-Jan-2019.)
|
|
|
Theorem | fo2ndresm 6028* |
Onto mapping of a restriction of the (second member of an
ordered pair) function. (Contributed by Jim Kingdon, 24-Jan-2019.)
|
|
|
Theorem | 1stcof 6029 |
Composition of the first member function with another function.
(Contributed by NM, 12-Oct-2007.)
|
|
|
Theorem | 2ndcof 6030 |
Composition of the second member function with another function.
(Contributed by FL, 15-Oct-2012.)
|
|
|
Theorem | xp1st 6031 |
Location of the first element of a Cartesian product. (Contributed by
Jeff Madsen, 2-Sep-2009.)
|
|
|
Theorem | xp2nd 6032 |
Location of the second element of a Cartesian product. (Contributed by
Jeff Madsen, 2-Sep-2009.)
|
|
|
Theorem | 1stexg 6033 |
Existence of the first member of a set. (Contributed by Jim Kingdon,
26-Jan-2019.)
|
|
|
Theorem | 2ndexg 6034 |
Existence of the first member of a set. (Contributed by Jim Kingdon,
26-Jan-2019.)
|
|
|
Theorem | elxp6 6035 |
Membership in a cross product. This version requires no quantifiers or
dummy variables. See also elxp4 4996. (Contributed by NM, 9-Oct-2004.)
|
|
|
Theorem | elxp7 6036 |
Membership in a cross product. This version requires no quantifiers or
dummy variables. See also elxp4 4996. (Contributed by NM, 19-Aug-2006.)
|
|
|
Theorem | oprssdmm 6037* |
Domain of closure of an operation. (Contributed by Jim Kingdon,
23-Oct-2023.)
|
|
|
Theorem | eqopi 6038 |
Equality with an ordered pair. (Contributed by NM, 15-Dec-2008.)
(Revised by Mario Carneiro, 23-Feb-2014.)
|
|
|
Theorem | xp2 6039* |
Representation of cross product based on ordered pair component
functions. (Contributed by NM, 16-Sep-2006.)
|
|
|
Theorem | unielxp 6040 |
The membership relation for a cross product is inherited by union.
(Contributed by NM, 16-Sep-2006.)
|
|
|
Theorem | 1st2nd2 6041 |
Reconstruction of a member of a cross product in terms of its ordered pair
components. (Contributed by NM, 20-Oct-2013.)
|
|
|
Theorem | xpopth 6042 |
An ordered pair theorem for members of cross products. (Contributed by
NM, 20-Jun-2007.)
|
|
|
Theorem | eqop 6043 |
Two ways to express equality with an ordered pair. (Contributed by NM,
3-Sep-2007.) (Proof shortened by Mario Carneiro, 26-Apr-2015.)
|
|
|
Theorem | eqop2 6044 |
Two ways to express equality with an ordered pair. (Contributed by NM,
25-Feb-2014.)
|
|
|
Theorem | op1steq 6045* |
Two ways of expressing that an element is the first member of an ordered
pair. (Contributed by NM, 22-Sep-2013.) (Revised by Mario Carneiro,
23-Feb-2014.)
|
|
|
Theorem | 2nd1st 6046 |
Swap the members of an ordered pair. (Contributed by NM, 31-Dec-2014.)
|
|
|
Theorem | 1st2nd 6047 |
Reconstruction of a member of a relation in terms of its ordered pair
components. (Contributed by NM, 29-Aug-2006.)
|
|
|
Theorem | 1stdm 6048 |
The first ordered pair component of a member of a relation belongs to the
domain of the relation. (Contributed by NM, 17-Sep-2006.)
|
|
|
Theorem | 2ndrn 6049 |
The second ordered pair component of a member of a relation belongs to the
range of the relation. (Contributed by NM, 17-Sep-2006.)
|
|
|
Theorem | 1st2ndbr 6050 |
Express an element of a relation as a relationship between first and
second components. (Contributed by Mario Carneiro, 22-Jun-2016.)
|
|
|
Theorem | releldm2 6051* |
Two ways of expressing membership in the domain of a relation.
(Contributed by NM, 22-Sep-2013.)
|
|
|
Theorem | reldm 6052* |
An expression for the domain of a relation. (Contributed by NM,
22-Sep-2013.)
|
|
|
Theorem | sbcopeq1a 6053 |
Equality theorem for substitution of a class for an ordered pair (analog
of sbceq1a 2891 that avoids the existential quantifiers of copsexg 4136).
(Contributed by NM, 19-Aug-2006.) (Revised by Mario Carneiro,
31-Aug-2015.)
|
|
|
Theorem | csbopeq1a 6054 |
Equality theorem for substitution of a class for an ordered pair
in (analog of csbeq1a 2983). (Contributed by NM,
19-Aug-2006.) (Revised by Mario Carneiro, 31-Aug-2015.)
|
|
|
Theorem | dfopab2 6055* |
A way to define an ordered-pair class abstraction without using
existential quantifiers. (Contributed by NM, 18-Aug-2006.) (Revised by
Mario Carneiro, 31-Aug-2015.)
|
|
|
Theorem | dfoprab3s 6056* |
A way to define an operation class abstraction without using existential
quantifiers. (Contributed by NM, 18-Aug-2006.) (Revised by Mario
Carneiro, 31-Aug-2015.)
|
|
|
Theorem | dfoprab3 6057* |
Operation class abstraction expressed without existential quantifiers.
(Contributed by NM, 16-Dec-2008.)
|
|
|
Theorem | dfoprab4 6058* |
Operation class abstraction expressed without existential quantifiers.
(Contributed by NM, 3-Sep-2007.) (Revised by Mario Carneiro,
31-Aug-2015.)
|
|
|
Theorem | dfoprab4f 6059* |
Operation class abstraction expressed without existential quantifiers.
(Unnecessary distinct variable restrictions were removed by David
Abernethy, 19-Jun-2012.) (Contributed by NM, 20-Dec-2008.) (Revised by
Mario Carneiro, 31-Aug-2015.)
|
|
|
Theorem | dfxp3 6060* |
Define the cross product of three classes. Compare df-xp 4515.
(Contributed by FL, 6-Nov-2013.) (Proof shortened by Mario Carneiro,
3-Nov-2015.)
|
|
|
Theorem | elopabi 6061* |
A consequence of membership in an ordered-pair class abstraction, using
ordered pair extractors. (Contributed by NM, 29-Aug-2006.)
|
|
|
Theorem | eloprabi 6062* |
A consequence of membership in an operation class abstraction, using
ordered pair extractors. (Contributed by NM, 6-Nov-2006.) (Revised by
David Abernethy, 19-Jun-2012.)
|
|
|
Theorem | mpomptsx 6063* |
Express a two-argument function as a one-argument function, or
vice-versa. (Contributed by Mario Carneiro, 24-Dec-2016.)
|
|
|
Theorem | mpompts 6064* |
Express a two-argument function as a one-argument function, or
vice-versa. (Contributed by Mario Carneiro, 24-Sep-2015.)
|
|
|
Theorem | dmmpossx 6065* |
The domain of a mapping is a subset of its base class. (Contributed by
Mario Carneiro, 9-Feb-2015.)
|
|
|
Theorem | fmpox 6066* |
Functionality, domain and codomain of a class given by the maps-to
notation, where is not constant but depends on .
(Contributed by NM, 29-Dec-2014.)
|
|
|
Theorem | fmpo 6067* |
Functionality, domain and range of a class given by the maps-to
notation. (Contributed by FL, 17-May-2010.)
|
|
|
Theorem | fnmpo 6068* |
Functionality and domain of a class given by the maps-to notation.
(Contributed by FL, 17-May-2010.)
|
|
|
Theorem | mpofvex 6069* |
Sufficient condition for an operation maps-to notation to be set-like.
(Contributed by Mario Carneiro, 3-Jul-2019.)
|
|
|
Theorem | fnmpoi 6070* |
Functionality and domain of a class given by the maps-to notation.
(Contributed by FL, 17-May-2010.)
|
|
|
Theorem | dmmpo 6071* |
Domain of a class given by the maps-to notation. (Contributed by FL,
17-May-2010.)
|
|
|
Theorem | mpofvexi 6072* |
Sufficient condition for an operation maps-to notation to be set-like.
(Contributed by Mario Carneiro, 3-Jul-2019.)
|
|
|
Theorem | ovmpoelrn 6073* |
An operation's value belongs to its range. (Contributed by AV,
27-Jan-2020.)
|
|
|
Theorem | dmmpoga 6074* |
Domain of an operation given by the maps-to notation, closed form of
dmmpo 6071. (Contributed by Alexander van der Vekens,
10-Feb-2019.)
|
|
|
Theorem | dmmpog 6075* |
Domain of an operation given by the maps-to notation, closed form of
dmmpo 6071. Caution: This theorem is only valid in the
very special case
where the value of the mapping is a constant! (Contributed by Alexander
van der Vekens, 1-Jun-2017.) (Proof shortened by AV, 10-Feb-2019.)
|
|
|
Theorem | mpoexxg 6076* |
Existence of an operation class abstraction (version for dependent
domains). (Contributed by Mario Carneiro, 30-Dec-2016.)
|
|
|
Theorem | mpoexg 6077* |
Existence of an operation class abstraction (special case).
(Contributed by FL, 17-May-2010.) (Revised by Mario Carneiro,
1-Sep-2015.)
|
|
|
Theorem | mpoexga 6078* |
If the domain of an operation given by maps-to notation is a set, the
operation is a set. (Contributed by NM, 12-Sep-2011.)
|
|
|
Theorem | mpoex 6079* |
If the domain of an operation given by maps-to notation is a set, the
operation is a set. (Contributed by Mario Carneiro, 20-Dec-2013.)
|
|
|
Theorem | fnmpoovd 6080* |
A function with a Cartesian product as domain is a mapping with two
arguments defined by its operation values. (Contributed by AV,
20-Feb-2019.) (Revised by AV, 3-Jul-2022.)
|
|
|
Theorem | fmpoco 6081* |
Composition of two functions. Variation of fmptco 5554 when the second
function has two arguments. (Contributed by Mario Carneiro,
8-Feb-2015.)
|
|
|
Theorem | oprabco 6082* |
Composition of a function with an operator abstraction. (Contributed by
Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro,
26-Sep-2015.)
|
|
|
Theorem | oprab2co 6083* |
Composition of operator abstractions. (Contributed by Jeff Madsen,
2-Sep-2009.) (Revised by David Abernethy, 23-Apr-2013.)
|
|
|
Theorem | df1st2 6084* |
An alternate possible definition of the function. (Contributed
by NM, 14-Oct-2004.) (Revised by Mario Carneiro, 31-Aug-2015.)
|
|
|
Theorem | df2nd2 6085* |
An alternate possible definition of the function. (Contributed
by NM, 10-Aug-2006.) (Revised by Mario Carneiro, 31-Aug-2015.)
|
|
|
Theorem | 1stconst 6086 |
The mapping of a restriction of the function to a constant
function. (Contributed by NM, 14-Dec-2008.)
|
|
|
Theorem | 2ndconst 6087 |
The mapping of a restriction of the function to a converse
constant function. (Contributed by NM, 27-Mar-2008.)
|
|
|
Theorem | dfmpo 6088* |
Alternate definition for the maps-to notation df-mpo 5747 (although it
requires that
be a set). (Contributed by NM, 19-Dec-2008.)
(Revised by Mario Carneiro, 31-Aug-2015.)
|
|
|
Theorem | cnvf1olem 6089 |
Lemma for cnvf1o 6090. (Contributed by Mario Carneiro,
27-Apr-2014.)
|
|
|
Theorem | cnvf1o 6090* |
Describe a function that maps the elements of a set to its converse
bijectively. (Contributed by Mario Carneiro, 27-Apr-2014.)
|
|
|
Theorem | f2ndf 6091 |
The (second
component of an ordered pair) function restricted to a
function is a
function from into
the codomain of .
(Contributed by Alexander van der Vekens, 4-Feb-2018.)
|
|
|
Theorem | fo2ndf 6092 |
The (second
component of an ordered pair) function restricted to
a function is
a function from onto
the range of .
(Contributed by Alexander van der Vekens, 4-Feb-2018.)
|
|
|
Theorem | f1o2ndf1 6093 |
The (second
component of an ordered pair) function restricted to
a one-to-one function is a one-to-one function from onto the
range of .
(Contributed by Alexander van der Vekens,
4-Feb-2018.)
|
|
|
Theorem | algrflem 6094 |
Lemma for algrf and related theorems. (Contributed by Mario Carneiro,
28-May-2014.) (Revised by Mario Carneiro, 30-Apr-2015.)
|
|
|
Theorem | algrflemg 6095 |
Lemma for algrf 11653 and related theorems. (Contributed by Mario
Carneiro,
28-May-2014.) (Revised by Jim Kingdon, 22-Jul-2021.)
|
|
|
Theorem | xporderlem 6096* |
Lemma for lexicographical ordering theorems. (Contributed by Scott
Fenton, 16-Mar-2011.)
|
|
|
Theorem | poxp 6097* |
A lexicographical ordering of two posets. (Contributed by Scott Fenton,
16-Mar-2011.) (Revised by Mario Carneiro, 7-Mar-2013.)
|
|
|
Theorem | spc2ed 6098* |
Existential specialization with 2 quantifiers, using implicit
substitution. (Contributed by Thierry Arnoux, 23-Aug-2017.)
|
|
|
Theorem | cnvoprab 6099* |
The converse of a class abstraction of nested ordered pairs.
(Contributed by Thierry Arnoux, 17-Aug-2017.)
|
|
|
Theorem | f1od2 6100* |
Describe an implicit one-to-one onto function of two variables.
(Contributed by Thierry Arnoux, 17-Aug-2017.)
|
|