Theorem List for Intuitionistic Logic Explorer - 6001-6100 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | ovelrn 6001* |
A member of an operation's range is a value of the operation.
(Contributed by NM, 7-Feb-2007.) (Revised by Mario Carneiro,
30-Jan-2014.)
|
|
|
Theorem | funimassov 6002* |
Membership relation for the values of a function whose image is a
subclass. (Contributed by Mario Carneiro, 23-Dec-2013.)
|
|
|
Theorem | ovelimab 6003* |
Operation value in an image. (Contributed by Mario Carneiro,
23-Dec-2013.) (Revised by Mario Carneiro, 29-Jan-2014.)
|
|
|
Theorem | ovconst2 6004 |
The value of a constant operation. (Contributed by NM, 5-Nov-2006.)
|
|
|
Theorem | caovclg 6005* |
Convert an operation closure law to class notation. (Contributed by
Mario Carneiro, 26-May-2014.)
|
|
|
Theorem | caovcld 6006* |
Convert an operation closure law to class notation. (Contributed by
Mario Carneiro, 30-Dec-2014.)
|
|
|
Theorem | caovcl 6007* |
Convert an operation closure law to class notation. (Contributed by NM,
4-Aug-1995.) (Revised by Mario Carneiro, 26-May-2014.)
|
|
|
Theorem | caovcomg 6008* |
Convert an operation commutative law to class notation. (Contributed
by Mario Carneiro, 1-Jun-2013.)
|
|
|
Theorem | caovcomd 6009* |
Convert an operation commutative law to class notation. (Contributed
by Mario Carneiro, 30-Dec-2014.)
|
|
|
Theorem | caovcom 6010* |
Convert an operation commutative law to class notation. (Contributed
by NM, 26-Aug-1995.) (Revised by Mario Carneiro, 1-Jun-2013.)
|
|
|
Theorem | caovassg 6011* |
Convert an operation associative law to class notation. (Contributed
by Mario Carneiro, 1-Jun-2013.) (Revised by Mario Carneiro,
26-May-2014.)
|
|
|
Theorem | caovassd 6012* |
Convert an operation associative law to class notation. (Contributed
by Mario Carneiro, 30-Dec-2014.)
|
|
|
Theorem | caovass 6013* |
Convert an operation associative law to class notation. (Contributed
by NM, 26-Aug-1995.) (Revised by Mario Carneiro, 26-May-2014.)
|
|
|
Theorem | caovcang 6014* |
Convert an operation cancellation law to class notation. (Contributed
by NM, 20-Aug-1995.) (Revised by Mario Carneiro, 30-Dec-2014.)
|
|
|
Theorem | caovcand 6015* |
Convert an operation cancellation law to class notation. (Contributed
by Mario Carneiro, 30-Dec-2014.)
|
|
|
Theorem | caovcanrd 6016* |
Commute the arguments of an operation cancellation law. (Contributed
by Mario Carneiro, 30-Dec-2014.)
|
|
|
Theorem | caovcan 6017* |
Convert an operation cancellation law to class notation. (Contributed
by NM, 20-Aug-1995.)
|
|
|
Theorem | caovordig 6018* |
Convert an operation ordering law to class notation. (Contributed by
Mario Carneiro, 31-Dec-2014.)
|
|
|
Theorem | caovordid 6019* |
Convert an operation ordering law to class notation. (Contributed by
Mario Carneiro, 31-Dec-2014.)
|
|
|
Theorem | caovordg 6020* |
Convert an operation ordering law to class notation. (Contributed by
NM, 19-Feb-1996.) (Revised by Mario Carneiro, 30-Dec-2014.)
|
|
|
Theorem | caovordd 6021* |
Convert an operation ordering law to class notation. (Contributed by
Mario Carneiro, 30-Dec-2014.)
|
|
|
Theorem | caovord2d 6022* |
Operation ordering law with commuted arguments. (Contributed by Mario
Carneiro, 30-Dec-2014.)
|
|
|
Theorem | caovord3d 6023* |
Ordering law. (Contributed by Mario Carneiro, 30-Dec-2014.)
|
|
|
Theorem | caovord 6024* |
Convert an operation ordering law to class notation. (Contributed by
NM, 19-Feb-1996.)
|
|
|
Theorem | caovord2 6025* |
Operation ordering law with commuted arguments. (Contributed by NM,
27-Feb-1996.)
|
|
|
Theorem | caovord3 6026* |
Ordering law. (Contributed by NM, 29-Feb-1996.)
|
|
|
Theorem | caovdig 6027* |
Convert an operation distributive law to class notation. (Contributed
by NM, 25-Aug-1995.) (Revised by Mario Carneiro, 26-Jul-2014.)
|
|
|
Theorem | caovdid 6028* |
Convert an operation distributive law to class notation. (Contributed
by Mario Carneiro, 30-Dec-2014.)
|
|
|
Theorem | caovdir2d 6029* |
Convert an operation distributive law to class notation. (Contributed
by Mario Carneiro, 30-Dec-2014.)
|
|
|
Theorem | caovdirg 6030* |
Convert an operation reverse distributive law to class notation.
(Contributed by Mario Carneiro, 19-Oct-2014.)
|
|
|
Theorem | caovdird 6031* |
Convert an operation distributive law to class notation. (Contributed
by Mario Carneiro, 30-Dec-2014.)
|
|
|
Theorem | caovdi 6032* |
Convert an operation distributive law to class notation. (Contributed
by NM, 25-Aug-1995.) (Revised by Mario Carneiro, 28-Jun-2013.)
|
|
|
Theorem | caov32d 6033* |
Rearrange arguments in a commutative, associative operation.
(Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro,
30-Dec-2014.)
|
|
|
Theorem | caov12d 6034* |
Rearrange arguments in a commutative, associative operation.
(Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro,
30-Dec-2014.)
|
|
|
Theorem | caov31d 6035* |
Rearrange arguments in a commutative, associative operation.
(Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro,
30-Dec-2014.)
|
|
|
Theorem | caov13d 6036* |
Rearrange arguments in a commutative, associative operation.
(Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro,
30-Dec-2014.)
|
|
|
Theorem | caov4d 6037* |
Rearrange arguments in a commutative, associative operation.
(Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro,
30-Dec-2014.)
|
|
|
Theorem | caov411d 6038* |
Rearrange arguments in a commutative, associative operation.
(Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro,
30-Dec-2014.)
|
|
|
Theorem | caov42d 6039* |
Rearrange arguments in a commutative, associative operation.
(Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro,
30-Dec-2014.)
|
|
|
Theorem | caov32 6040* |
Rearrange arguments in a commutative, associative operation.
(Contributed by NM, 26-Aug-1995.)
|
|
|
Theorem | caov12 6041* |
Rearrange arguments in a commutative, associative operation.
(Contributed by NM, 26-Aug-1995.)
|
|
|
Theorem | caov31 6042* |
Rearrange arguments in a commutative, associative operation.
(Contributed by NM, 26-Aug-1995.)
|
|
|
Theorem | caov13 6043* |
Rearrange arguments in a commutative, associative operation.
(Contributed by NM, 26-Aug-1995.)
|
|
|
Theorem | caovdilemd 6044* |
Lemma used by real number construction. (Contributed by Jim Kingdon,
16-Sep-2019.)
|
|
|
Theorem | caovlem2d 6045* |
Rearrangement of expression involving multiplication () and
addition ().
(Contributed by Jim Kingdon, 3-Jan-2020.)
|
|
|
Theorem | caovimo 6046* |
Uniqueness of inverse element in commutative, associative operation with
identity. The identity element is . (Contributed by Jim Kingdon,
18-Sep-2019.)
|
|
|
2.6.12 Maps-to notation
|
|
Theorem | elmpocl 6047* |
If a two-parameter class is inhabited, constrain the implicit pair.
(Contributed by Stefan O'Rear, 7-Mar-2015.)
|
|
|
Theorem | elmpocl1 6048* |
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 6049* |
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 6050* |
Utility lemma for two-parameter classes. (Contributed by Stefan O'Rear,
21-Jan-2015.)
|
|
|
Theorem | f1ocnvd 6051* |
Describe an implicit one-to-one onto function. (Contributed by Mario
Carneiro, 30-Apr-2015.)
|
|
|
Theorem | f1od 6052* |
Describe an implicit one-to-one onto function. (Contributed by Mario
Carneiro, 12-May-2014.)
|
|
|
Theorem | f1ocnv2d 6053* |
Describe an implicit one-to-one onto function. (Contributed by Mario
Carneiro, 30-Apr-2015.)
|
|
|
Theorem | f1o2d 6054* |
Describe an implicit one-to-one onto function. (Contributed by Mario
Carneiro, 12-May-2014.)
|
|
|
Theorem | f1opw2 6055* |
A one-to-one mapping induces a one-to-one mapping on power sets. This
version of f1opw 6056 avoids the Axiom of Replacement.
(Contributed by
Mario Carneiro, 26-Jun-2015.)
|
|
|
Theorem | f1opw 6056* |
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 6057* |
Formula building theorem for support restriction, on a function which
preserves zero. (Contributed by Stefan O'Rear, 9-Mar-2015.)
|
|
|
Theorem | suppssov1 6058* |
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 6059 |
Extend class notation to include mapping of an operation to a function
operation.
|
|
|
Syntax | cofr 6060 |
Extend class notation to include mapping of a binary relation to a
function relation.
|
|
|
Definition | df-of 6061* |
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 6062* |
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 6063 |
Equality theorem for function operation. (Contributed by Mario
Carneiro, 20-Jul-2014.)
|
|
|
Theorem | ofreq 6064 |
Equality theorem for function relation. (Contributed by Mario Carneiro,
28-Jul-2014.)
|
|
|
Theorem | ofexg 6065 |
A function operation restricted to a set is a set. (Contributed by NM,
28-Jul-2014.)
|
|
|
Theorem | nfof 6066 |
Hypothesis builder for function operation. (Contributed by Mario
Carneiro, 20-Jul-2014.)
|
|
|
Theorem | nfofr 6067 |
Hypothesis builder for function relation. (Contributed by Mario
Carneiro, 28-Jul-2014.)
|
|
|
Theorem | offval 6068* |
Value of an operation applied to two functions. (Contributed by Mario
Carneiro, 20-Jul-2014.)
|
|
|
Theorem | ofrfval 6069* |
Value of a relation applied to two functions. (Contributed by Mario
Carneiro, 28-Jul-2014.)
|
|
|
Theorem | ofvalg 6070 |
Evaluate a function operation at a point. (Contributed by Mario
Carneiro, 20-Jul-2014.) (Revised by Jim Kingdon, 22-Nov-2023.)
|
|
|
Theorem | ofrval 6071 |
Exhibit a function relation at a point. (Contributed by Mario
Carneiro, 28-Jul-2014.)
|
|
|
Theorem | ofmresval 6072 |
Value of a restriction of the function operation map. (Contributed by
NM, 20-Oct-2014.)
|
|
|
Theorem | off 6073* |
The function operation produces a function. (Contributed by Mario
Carneiro, 20-Jul-2014.)
|
|
|
Theorem | offeq 6074* |
Convert an identity of the operation to the analogous identity on
the function operation. (Contributed by Jim Kingdon,
26-Nov-2023.)
|
|
|
Theorem | ofres 6075 |
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 6076* |
The function operation expressed as a mapping. (Contributed by Mario
Carneiro, 20-Jul-2014.)
|
|
|
Theorem | ofrfval2 6077* |
The function relation acting on maps. (Contributed by Mario Carneiro,
20-Jul-2014.)
|
|
|
Theorem | suppssof1 6078* |
Formula building theorem for support restrictions: vector operation with
left annihilator. (Contributed by Stefan O'Rear, 9-Mar-2015.)
|
|
|
Theorem | ofco 6079 |
The composition of a function operation with another function.
(Contributed by Mario Carneiro, 19-Dec-2014.)
|
|
|
Theorem | offveqb 6080* |
Equivalent expressions for equality with a function operation.
(Contributed by NM, 9-Oct-2014.) (Proof shortened by Mario Carneiro,
5-Dec-2016.)
|
|
|
Theorem | ofc12 6081 |
Function operation on two constant functions. (Contributed by Mario
Carneiro, 28-Jul-2014.)
|
|
|
Theorem | caofref 6082* |
Transfer a reflexive law to the function relation. (Contributed by
Mario Carneiro, 28-Jul-2014.)
|
|
|
Theorem | caofinvl 6083* |
Transfer a left inverse law to the function operation. (Contributed
by NM, 22-Oct-2014.)
|
|
|
Theorem | caofcom 6084* |
Transfer a commutative law to the function operation. (Contributed by
Mario Carneiro, 26-Jul-2014.)
|
|
|
Theorem | caofrss 6085* |
Transfer a relation subset law to the function relation. (Contributed
by Mario Carneiro, 28-Jul-2014.)
|
|
|
Theorem | caoftrn 6086* |
Transfer a transitivity law to the function relation. (Contributed by
Mario Carneiro, 28-Jul-2014.)
|
|
|
2.6.14 Functions (continued)
|
|
Theorem | resfunexgALT 6087 |
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 5717 but requires ax-pow 4160 and ax-un 4418. (Contributed by NM,
7-Apr-1995.) (Proof modification is discouraged.)
(New usage is discouraged.)
|
|
|
Theorem | cofunexg 6088 |
Existence of a composition when the first member is a function.
(Contributed by NM, 8-Oct-2007.)
|
|
|
Theorem | cofunex2g 6089 |
Existence of a composition when the second member is one-to-one.
(Contributed by NM, 8-Oct-2007.)
|
|
|
Theorem | fnexALT 6090 |
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 5282. This version of fnex 5718
uses
ax-pow 4160 and ax-un 4418, whereas fnex 5718
does not. (Contributed by NM,
14-Aug-1994.) (Proof modification is discouraged.)
(New usage is discouraged.)
|
|
|
Theorem | funexw 6091 |
Weak version of funex 5719 that holds without ax-coll 4104. If the domain and
codomain of a function exist, so does the function. (Contributed by Rohan
Ridenour, 13-Aug-2023.)
|
|
|
Theorem | mptexw 6092* |
Weak version of mptex 5722 that holds without ax-coll 4104. If the domain
and codomain of a function given by maps-to notation are sets, the
function is a set. (Contributed by Rohan Ridenour, 13-Aug-2023.)
|
|
|
Theorem | funrnex 6093 |
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 5719. (Contributed by NM, 11-Nov-1995.)
|
|
|
Theorem | fornex 6094 |
If the domain of an onto function exists, so does its codomain.
(Contributed by NM, 23-Jul-2004.)
|
|
|
Theorem | f1dmex 6095 |
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 6096* |
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 5721, funex 5719, fnex 5718, resfunexg 5717, and
funimaexg 5282. See also abrexex2 6103. (Contributed by NM, 16-Oct-2003.)
(Proof shortened by Mario Carneiro, 31-Aug-2015.)
|
|
|
Theorem | abrexexg 6097* |
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 6098* |
The existence of an indexed union. is normally a free-variable
parameter in .
(Contributed by NM, 23-Mar-2006.)
|
|
|
Theorem | abrexex2g 6099* |
Existence of an existentially restricted class abstraction.
(Contributed by Jeff Madsen, 2-Sep-2009.)
|
|
|
Theorem | opabex3d 6100* |
Existence of an ordered pair abstraction, deduction version.
(Contributed by Alexander van der Vekens, 19-Oct-2017.)
|
|