Theorem List for Intuitionistic Logic Explorer - 6001-6100 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | caov32d 6001* |
Rearrange arguments in a commutative, associative operation.
(Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro,
30-Dec-2014.)
|
|
|
Theorem | caov12d 6002* |
Rearrange arguments in a commutative, associative operation.
(Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro,
30-Dec-2014.)
|
|
|
Theorem | caov31d 6003* |
Rearrange arguments in a commutative, associative operation.
(Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro,
30-Dec-2014.)
|
|
|
Theorem | caov13d 6004* |
Rearrange arguments in a commutative, associative operation.
(Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro,
30-Dec-2014.)
|
|
|
Theorem | caov4d 6005* |
Rearrange arguments in a commutative, associative operation.
(Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro,
30-Dec-2014.)
|
|
|
Theorem | caov411d 6006* |
Rearrange arguments in a commutative, associative operation.
(Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro,
30-Dec-2014.)
|
|
|
Theorem | caov42d 6007* |
Rearrange arguments in a commutative, associative operation.
(Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro,
30-Dec-2014.)
|
|
|
Theorem | caov32 6008* |
Rearrange arguments in a commutative, associative operation.
(Contributed by NM, 26-Aug-1995.)
|
|
|
Theorem | caov12 6009* |
Rearrange arguments in a commutative, associative operation.
(Contributed by NM, 26-Aug-1995.)
|
|
|
Theorem | caov31 6010* |
Rearrange arguments in a commutative, associative operation.
(Contributed by NM, 26-Aug-1995.)
|
|
|
Theorem | caov13 6011* |
Rearrange arguments in a commutative, associative operation.
(Contributed by NM, 26-Aug-1995.)
|
|
|
Theorem | caovdilemd 6012* |
Lemma used by real number construction. (Contributed by Jim Kingdon,
16-Sep-2019.)
|
|
|
Theorem | caovlem2d 6013* |
Rearrangement of expression involving multiplication () and
addition ().
(Contributed by Jim Kingdon, 3-Jan-2020.)
|
|
|
Theorem | caovimo 6014* |
Uniqueness of inverse element in commutative, associative operation with
identity. The identity element is . (Contributed by Jim Kingdon,
18-Sep-2019.)
|
|
|
Theorem | grprinvlem 6015* |
Lemma for grprinvd 6016. (Contributed by NM, 9-Aug-2013.)
|
|
|
Theorem | grprinvd 6016* |
Deduce right inverse from left inverse and left identity in an
associative structure (such as a group). (Contributed by NM,
10-Aug-2013.) (Proof shortened by Mario Carneiro, 6-Jan-2015.)
|
|
|
Theorem | grpridd 6017* |
Deduce right identity from left inverse and left identity in an
associative structure (such as a group). (Contributed by NM,
10-Aug-2013.) (Proof shortened by Mario Carneiro, 6-Jan-2015.)
|
|
|
2.6.12 Maps-to notation
|
|
Theorem | elmpocl 6018* |
If a two-parameter class is inhabited, constrain the implicit pair.
(Contributed by Stefan O'Rear, 7-Mar-2015.)
|
|
|
Theorem | elmpocl1 6019* |
If a two-parameter class is inhabited, the first argument is in its
nominal domain. (Contributed by FL, 15-Oct-2012.) (Revised by Stefan
O'Rear, 7-Mar-2015.)
|
|
|
Theorem | elmpocl2 6020* |
If a two-parameter class is inhabited, the second argument is in its
nominal domain. (Contributed by FL, 15-Oct-2012.) (Revised by Stefan
O'Rear, 7-Mar-2015.)
|
|
|
Theorem | elovmpo 6021* |
Utility lemma for two-parameter classes. (Contributed by Stefan O'Rear,
21-Jan-2015.)
|
|
|
Theorem | f1ocnvd 6022* |
Describe an implicit one-to-one onto function. (Contributed by Mario
Carneiro, 30-Apr-2015.)
|
|
|
Theorem | f1od 6023* |
Describe an implicit one-to-one onto function. (Contributed by Mario
Carneiro, 12-May-2014.)
|
|
|
Theorem | f1ocnv2d 6024* |
Describe an implicit one-to-one onto function. (Contributed by Mario
Carneiro, 30-Apr-2015.)
|
|
|
Theorem | f1o2d 6025* |
Describe an implicit one-to-one onto function. (Contributed by Mario
Carneiro, 12-May-2014.)
|
|
|
Theorem | f1opw2 6026* |
A one-to-one mapping induces a one-to-one mapping on power sets. This
version of f1opw 6027 avoids the Axiom of Replacement.
(Contributed by
Mario Carneiro, 26-Jun-2015.)
|
|
|
Theorem | f1opw 6027* |
A one-to-one mapping induces a one-to-one mapping on power sets.
(Contributed by Stefan O'Rear, 18-Nov-2014.) (Revised by Mario
Carneiro, 26-Jun-2015.)
|
|
|
Theorem | suppssfv 6028* |
Formula building theorem for support restriction, on a function which
preserves zero. (Contributed by Stefan O'Rear, 9-Mar-2015.)
|
|
|
Theorem | suppssov1 6029* |
Formula building theorem for support restrictions: operator with left
annihilator. (Contributed by Stefan O'Rear, 9-Mar-2015.)
|
|
|
2.6.13 Function operation
|
|
Syntax | cof 6030 |
Extend class notation to include mapping of an operation to a function
operation.
|
|
|
Syntax | cofr 6031 |
Extend class notation to include mapping of a binary relation to a
function relation.
|
|
|
Definition | df-of 6032* |
Define the function operation map. The definition is designed so that
if is a binary
operation, then is the analogous operation
on functions which corresponds to applying pointwise to the values
of the functions. (Contributed by Mario Carneiro, 20-Jul-2014.)
|
|
|
Definition | df-ofr 6033* |
Define the function relation map. The definition is designed so that if
is a binary
relation, then is the analogous relation on
functions which is true when each element of the left function relates
to the corresponding element of the right function. (Contributed by
Mario Carneiro, 28-Jul-2014.)
|
|
|
Theorem | ofeq 6034 |
Equality theorem for function operation. (Contributed by Mario
Carneiro, 20-Jul-2014.)
|
|
|
Theorem | ofreq 6035 |
Equality theorem for function relation. (Contributed by Mario Carneiro,
28-Jul-2014.)
|
|
|
Theorem | ofexg 6036 |
A function operation restricted to a set is a set. (Contributed by NM,
28-Jul-2014.)
|
|
|
Theorem | nfof 6037 |
Hypothesis builder for function operation. (Contributed by Mario
Carneiro, 20-Jul-2014.)
|
|
|
Theorem | nfofr 6038 |
Hypothesis builder for function relation. (Contributed by Mario
Carneiro, 28-Jul-2014.)
|
|
|
Theorem | offval 6039* |
Value of an operation applied to two functions. (Contributed by Mario
Carneiro, 20-Jul-2014.)
|
|
|
Theorem | ofrfval 6040* |
Value of a relation applied to two functions. (Contributed by Mario
Carneiro, 28-Jul-2014.)
|
|
|
Theorem | ofvalg 6041 |
Evaluate a function operation at a point. (Contributed by Mario
Carneiro, 20-Jul-2014.) (Revised by Jim Kingdon, 22-Nov-2023.)
|
|
|
Theorem | ofrval 6042 |
Exhibit a function relation at a point. (Contributed by Mario
Carneiro, 28-Jul-2014.)
|
|
|
Theorem | ofmresval 6043 |
Value of a restriction of the function operation map. (Contributed by
NM, 20-Oct-2014.)
|
|
|
Theorem | off 6044* |
The function operation produces a function. (Contributed by Mario
Carneiro, 20-Jul-2014.)
|
|
|
Theorem | offeq 6045* |
Convert an identity of the operation to the analogous identity on
the function operation. (Contributed by Jim Kingdon,
26-Nov-2023.)
|
|
|
Theorem | ofres 6046 |
Restrict the operands of a function operation to the same domain as that
of the operation itself. (Contributed by Mario Carneiro,
15-Sep-2014.)
|
|
|
Theorem | offval2 6047* |
The function operation expressed as a mapping. (Contributed by Mario
Carneiro, 20-Jul-2014.)
|
|
|
Theorem | ofrfval2 6048* |
The function relation acting on maps. (Contributed by Mario Carneiro,
20-Jul-2014.)
|
|
|
Theorem | suppssof1 6049* |
Formula building theorem for support restrictions: vector operation with
left annihilator. (Contributed by Stefan O'Rear, 9-Mar-2015.)
|
|
|
Theorem | ofco 6050 |
The composition of a function operation with another function.
(Contributed by Mario Carneiro, 19-Dec-2014.)
|
|
|
Theorem | offveqb 6051* |
Equivalent expressions for equality with a function operation.
(Contributed by NM, 9-Oct-2014.) (Proof shortened by Mario Carneiro,
5-Dec-2016.)
|
|
|
Theorem | ofc12 6052 |
Function operation on two constant functions. (Contributed by Mario
Carneiro, 28-Jul-2014.)
|
|
|
Theorem | caofref 6053* |
Transfer a reflexive law to the function relation. (Contributed by
Mario Carneiro, 28-Jul-2014.)
|
|
|
Theorem | caofinvl 6054* |
Transfer a left inverse law to the function operation. (Contributed
by NM, 22-Oct-2014.)
|
|
|
Theorem | caofcom 6055* |
Transfer a commutative law to the function operation. (Contributed by
Mario Carneiro, 26-Jul-2014.)
|
|
|
Theorem | caofrss 6056* |
Transfer a relation subset law to the function relation. (Contributed
by Mario Carneiro, 28-Jul-2014.)
|
|
|
Theorem | caoftrn 6057* |
Transfer a transitivity law to the function relation. (Contributed by
Mario Carneiro, 28-Jul-2014.)
|
|
|
2.6.14 Functions (continued)
|
|
Theorem | resfunexgALT 6058 |
The restriction of a function to a set exists. Compare Proposition 6.17
of [TakeutiZaring] p. 28. This
version has a shorter proof than
resfunexg 5688 but requires ax-pow 4135 and ax-un 4393. (Contributed by NM,
7-Apr-1995.) (Proof modification is discouraged.)
(New usage is discouraged.)
|
|
|
Theorem | cofunexg 6059 |
Existence of a composition when the first member is a function.
(Contributed by NM, 8-Oct-2007.)
|
|
|
Theorem | cofunex2g 6060 |
Existence of a composition when the second member is one-to-one.
(Contributed by NM, 8-Oct-2007.)
|
|
|
Theorem | fnexALT 6061 |
If the domain of a function is a set, the function is a set. Theorem
6.16(1) of [TakeutiZaring] p. 28.
This theorem is derived using the Axiom
of Replacement in the form of funimaexg 5254. This version of fnex 5689
uses
ax-pow 4135 and ax-un 4393, whereas fnex 5689
does not. (Contributed by NM,
14-Aug-1994.) (Proof modification is discouraged.)
(New usage is discouraged.)
|
|
|
Theorem | funrnex 6062 |
If the domain of a function exists, so does its range. Part of Theorem
4.15(v) of [Monk1] p. 46. This theorem is
derived using the Axiom of
Replacement in the form of funex 5690. (Contributed by NM, 11-Nov-1995.)
|
|
|
Theorem | fornex 6063 |
If the domain of an onto function exists, so does its codomain.
(Contributed by NM, 23-Jul-2004.)
|
|
|
Theorem | f1dmex 6064 |
If the codomain of a one-to-one function exists, so does its domain. This
can be thought of as a form of the Axiom of Replacement. (Contributed by
NM, 4-Sep-2004.)
|
|
|
Theorem | abrexex 6065* |
Existence of a class abstraction of existentially restricted sets.
is normally a free-variable parameter in the class expression
substituted for , which can be thought of as . This
simple-looking theorem is actually quite powerful and appears to involve
the Axiom of Replacement in an intrinsic way, as can be seen by tracing
back through the path mptexg 5692, funex 5690, fnex 5689, resfunexg 5688, and
funimaexg 5254. See also abrexex2 6072. (Contributed by NM, 16-Oct-2003.)
(Proof shortened by Mario Carneiro, 31-Aug-2015.)
|
|
|
Theorem | abrexexg 6066* |
Existence of a class abstraction of existentially restricted sets.
is normally a free-variable parameter in . The antecedent assures
us that is a
set. (Contributed by NM, 3-Nov-2003.)
|
|
|
Theorem | iunexg 6067* |
The existence of an indexed union. is normally a free-variable
parameter in .
(Contributed by NM, 23-Mar-2006.)
|
|
|
Theorem | abrexex2g 6068* |
Existence of an existentially restricted class abstraction.
(Contributed by Jeff Madsen, 2-Sep-2009.)
|
|
|
Theorem | opabex3d 6069* |
Existence of an ordered pair abstraction, deduction version.
(Contributed by Alexander van der Vekens, 19-Oct-2017.)
|
|
|
Theorem | opabex3 6070* |
Existence of an ordered pair abstraction. (Contributed by Jeff Madsen,
2-Sep-2009.)
|
|
|
Theorem | iunex 6071* |
The existence of an indexed union. is normally a free-variable
parameter in the class expression substituted for , which can be
read informally as . (Contributed by NM, 13-Oct-2003.)
|
|
|
Theorem | abrexex2 6072* |
Existence of an existentially restricted class abstraction. is
normally has free-variable parameters and . See also
abrexex 6065. (Contributed by NM, 12-Sep-2004.)
|
|
|
Theorem | abexssex 6073* |
Existence of a class abstraction with an existentially quantified
expression. Both and can be
free in .
(Contributed
by NM, 29-Jul-2006.)
|
|
|
Theorem | abexex 6074* |
A condition where a class builder continues to exist after its wff is
existentially quantified. (Contributed by NM, 4-Mar-2007.)
|
|
|
Theorem | oprabexd 6075* |
Existence of an operator abstraction. (Contributed by Jeff Madsen,
2-Sep-2009.)
|
|
|
Theorem | oprabex 6076* |
Existence of an operation class abstraction. (Contributed by NM,
19-Oct-2004.)
|
|
|
Theorem | oprabex3 6077* |
Existence of an operation class abstraction (special case).
(Contributed by NM, 19-Oct-2004.)
|
|
|
Theorem | oprabrexex2 6078* |
Existence of an existentially restricted operation abstraction.
(Contributed by Jeff Madsen, 11-Jun-2010.)
|
|
|
Theorem | ab2rexex 6079* |
Existence of a class abstraction of existentially restricted sets.
Variables and
are normally
free-variable parameters in the
class expression substituted for , which can be thought of as
. See comments for abrexex 6065. (Contributed by NM,
20-Sep-2011.)
|
|
|
Theorem | ab2rexex2 6080* |
Existence of an existentially restricted class abstraction.
normally has free-variable parameters , , and .
Compare abrexex2 6072. (Contributed by NM, 20-Sep-2011.)
|
|
|
Theorem | xpexgALT 6081 |
The cross product of two sets is a set. Proposition 6.2 of
[TakeutiZaring] p. 23. This
version is proven using Replacement; see
xpexg 4700 for a version that uses the Power Set axiom
instead.
(Contributed by Mario Carneiro, 20-May-2013.)
(Proof modification is discouraged.) (New usage is discouraged.)
|
|
|
Theorem | offval3 6082* |
General value of with no assumptions on functionality
of and . (Contributed by Stefan
O'Rear, 24-Jan-2015.)
|
|
|
Theorem | offres 6083 |
Pointwise combination commutes with restriction. (Contributed by Stefan
O'Rear, 24-Jan-2015.)
|
|
|
Theorem | ofmres 6084* |
Equivalent expressions for a restriction of the function operation map.
Unlike which is a proper class,
can
be a set by ofmresex 6085, allowing it to be used as a function or
structure argument. By ofmresval 6043, 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 6085 |
Existence of a restriction of the function operation map. (Contributed
by NM, 20-Oct-2014.)
|
|
|
2.6.15 First and second members of an ordered
pair
|
|
Syntax | c1st 6086 |
Extend the definition of a class to include the first member an ordered
pair function.
|
|
|
Syntax | c2nd 6087 |
Extend the definition of a class to include the second member an ordered
pair function.
|
|
|
Definition | df-1st 6088 |
Define a function that extracts the first member, or abscissa, of an
ordered pair. Theorem op1st 6094 proves that it does this. For example,
( 3 , 4 ) = 3 . Equivalent to Definition
5.13 (i) of
[Monk1] p. 52 (compare op1sta 5067 and op1stb 4438). The notation is the same
as Monk's. (Contributed by NM, 9-Oct-2004.)
|
|
|
Definition | df-2nd 6089 |
Define a function that extracts the second member, or ordinate, of an
ordered pair. Theorem op2nd 6095 proves that it does this. For example,
3 , 4 ) = 4 . Equivalent to Definition 5.13 (ii)
of [Monk1] p. 52 (compare op2nda 5070 and op2ndb 5069). The notation is the
same as Monk's. (Contributed by NM, 9-Oct-2004.)
|
|
|
Theorem | 1stvalg 6090 |
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 6091 |
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 6092 |
The value of the first-member function at the empty set. (Contributed by
NM, 23-Apr-2007.)
|
|
|
Theorem | 2nd0 6093 |
The value of the second-member function at the empty set. (Contributed by
NM, 23-Apr-2007.)
|
|
|
Theorem | op1st 6094 |
Extract the first member of an ordered pair. (Contributed by NM,
5-Oct-2004.)
|
|
|
Theorem | op2nd 6095 |
Extract the second member of an ordered pair. (Contributed by NM,
5-Oct-2004.)
|
|
|
Theorem | op1std 6096 |
Extract the first member of an ordered pair. (Contributed by Mario
Carneiro, 31-Aug-2015.)
|
|
|
Theorem | op2ndd 6097 |
Extract the second member of an ordered pair. (Contributed by Mario
Carneiro, 31-Aug-2015.)
|
|
|
Theorem | op1stg 6098 |
Extract the first member of an ordered pair. (Contributed by NM,
19-Jul-2005.)
|
|
|
Theorem | op2ndg 6099 |
Extract the second member of an ordered pair. (Contributed by NM,
19-Jul-2005.)
|
|
|
Theorem | ot1stg 6100 |
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 6100,
ot2ndg 6101, ot3rdgg 6102.) (Contributed by NM, 3-Apr-2015.) (Revised
by
Mario Carneiro, 2-May-2015.)
|
|