Theorem List for Intuitionistic Logic Explorer - 5901-6000 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | ovmpoa 5901* |
Value of an operation given by a maps-to rule. (Contributed by NM,
19-Dec-2013.)
|
|
|
Theorem | ovmpodf 5902* |
Alternate deduction version of ovmpo 5906, suitable for iteration.
(Contributed by Mario Carneiro, 7-Jan-2017.)
|
|
|
Theorem | ovmpodv 5903* |
Alternate deduction version of ovmpo 5906, suitable for iteration.
(Contributed by Mario Carneiro, 7-Jan-2017.)
|
|
|
Theorem | ovmpodv2 5904* |
Alternate deduction version of ovmpo 5906, suitable for iteration.
(Contributed by Mario Carneiro, 7-Jan-2017.)
|
|
|
Theorem | ovmpog 5905* |
Value of an operation given by a maps-to rule. Special case.
(Contributed by NM, 14-Sep-1999.) (Revised by David Abernethy,
19-Jun-2012.)
|
|
|
Theorem | ovmpo 5906* |
Value of an operation given by a maps-to rule. Special case.
(Contributed by NM, 16-May-1995.) (Revised by David Abernethy,
19-Jun-2012.)
|
|
|
Theorem | ovi3 5907* |
The value of an operation class abstraction. Special case.
(Contributed by NM, 28-May-1995.) (Revised by Mario Carneiro,
29-Dec-2014.)
|
|
|
Theorem | ov6g 5908* |
The value of an operation class abstraction. Special case.
(Contributed by NM, 13-Nov-2006.)
|
|
|
Theorem | ovg 5909* |
The value of an operation class abstraction. (Contributed by Jeff
Madsen, 10-Jun-2010.)
|
|
|
Theorem | ovres 5910 |
The value of a restricted operation. (Contributed by FL, 10-Nov-2006.)
|
|
|
Theorem | ovresd 5911 |
Lemma for converting metric theorems to metric space theorems.
(Contributed by Mario Carneiro, 2-Oct-2015.)
|
|
|
Theorem | oprssov 5912 |
The value of a member of the domain of a subclass of an operation.
(Contributed by NM, 23-Aug-2007.)
|
|
|
Theorem | fovrn 5913 |
An operation's value belongs to its codomain. (Contributed by NM,
27-Aug-2006.)
|
|
|
Theorem | fovrnda 5914 |
An operation's value belongs to its codomain. (Contributed by Mario
Carneiro, 29-Dec-2016.)
|
|
|
Theorem | fovrnd 5915 |
An operation's value belongs to its codomain. (Contributed by Mario
Carneiro, 29-Dec-2016.)
|
|
|
Theorem | fnrnov 5916* |
The range of an operation expressed as a collection of the operation's
values. (Contributed by NM, 29-Oct-2006.)
|
|
|
Theorem | foov 5917* |
An onto mapping of an operation expressed in terms of operation values.
(Contributed by NM, 29-Oct-2006.)
|
|
|
Theorem | fnovrn 5918 |
An operation's value belongs to its range. (Contributed by NM,
10-Feb-2007.)
|
|
|
Theorem | ovelrn 5919* |
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 5920* |
Membership relation for the values of a function whose image is a
subclass. (Contributed by Mario Carneiro, 23-Dec-2013.)
|
|
|
Theorem | ovelimab 5921* |
Operation value in an image. (Contributed by Mario Carneiro,
23-Dec-2013.) (Revised by Mario Carneiro, 29-Jan-2014.)
|
|
|
Theorem | ovconst2 5922 |
The value of a constant operation. (Contributed by NM, 5-Nov-2006.)
|
|
|
Theorem | caovclg 5923* |
Convert an operation closure law to class notation. (Contributed by
Mario Carneiro, 26-May-2014.)
|
|
|
Theorem | caovcld 5924* |
Convert an operation closure law to class notation. (Contributed by
Mario Carneiro, 30-Dec-2014.)
|
|
|
Theorem | caovcl 5925* |
Convert an operation closure law to class notation. (Contributed by NM,
4-Aug-1995.) (Revised by Mario Carneiro, 26-May-2014.)
|
|
|
Theorem | caovcomg 5926* |
Convert an operation commutative law to class notation. (Contributed
by Mario Carneiro, 1-Jun-2013.)
|
|
|
Theorem | caovcomd 5927* |
Convert an operation commutative law to class notation. (Contributed
by Mario Carneiro, 30-Dec-2014.)
|
|
|
Theorem | caovcom 5928* |
Convert an operation commutative law to class notation. (Contributed
by NM, 26-Aug-1995.) (Revised by Mario Carneiro, 1-Jun-2013.)
|
|
|
Theorem | caovassg 5929* |
Convert an operation associative law to class notation. (Contributed
by Mario Carneiro, 1-Jun-2013.) (Revised by Mario Carneiro,
26-May-2014.)
|
|
|
Theorem | caovassd 5930* |
Convert an operation associative law to class notation. (Contributed
by Mario Carneiro, 30-Dec-2014.)
|
|
|
Theorem | caovass 5931* |
Convert an operation associative law to class notation. (Contributed
by NM, 26-Aug-1995.) (Revised by Mario Carneiro, 26-May-2014.)
|
|
|
Theorem | caovcang 5932* |
Convert an operation cancellation law to class notation. (Contributed
by NM, 20-Aug-1995.) (Revised by Mario Carneiro, 30-Dec-2014.)
|
|
|
Theorem | caovcand 5933* |
Convert an operation cancellation law to class notation. (Contributed
by Mario Carneiro, 30-Dec-2014.)
|
|
|
Theorem | caovcanrd 5934* |
Commute the arguments of an operation cancellation law. (Contributed
by Mario Carneiro, 30-Dec-2014.)
|
|
|
Theorem | caovcan 5935* |
Convert an operation cancellation law to class notation. (Contributed
by NM, 20-Aug-1995.)
|
|
|
Theorem | caovordig 5936* |
Convert an operation ordering law to class notation. (Contributed by
Mario Carneiro, 31-Dec-2014.)
|
|
|
Theorem | caovordid 5937* |
Convert an operation ordering law to class notation. (Contributed by
Mario Carneiro, 31-Dec-2014.)
|
|
|
Theorem | caovordg 5938* |
Convert an operation ordering law to class notation. (Contributed by
NM, 19-Feb-1996.) (Revised by Mario Carneiro, 30-Dec-2014.)
|
|
|
Theorem | caovordd 5939* |
Convert an operation ordering law to class notation. (Contributed by
Mario Carneiro, 30-Dec-2014.)
|
|
|
Theorem | caovord2d 5940* |
Operation ordering law with commuted arguments. (Contributed by Mario
Carneiro, 30-Dec-2014.)
|
|
|
Theorem | caovord3d 5941* |
Ordering law. (Contributed by Mario Carneiro, 30-Dec-2014.)
|
|
|
Theorem | caovord 5942* |
Convert an operation ordering law to class notation. (Contributed by
NM, 19-Feb-1996.)
|
|
|
Theorem | caovord2 5943* |
Operation ordering law with commuted arguments. (Contributed by NM,
27-Feb-1996.)
|
|
|
Theorem | caovord3 5944* |
Ordering law. (Contributed by NM, 29-Feb-1996.)
|
|
|
Theorem | caovdig 5945* |
Convert an operation distributive law to class notation. (Contributed
by NM, 25-Aug-1995.) (Revised by Mario Carneiro, 26-Jul-2014.)
|
|
|
Theorem | caovdid 5946* |
Convert an operation distributive law to class notation. (Contributed
by Mario Carneiro, 30-Dec-2014.)
|
|
|
Theorem | caovdir2d 5947* |
Convert an operation distributive law to class notation. (Contributed
by Mario Carneiro, 30-Dec-2014.)
|
|
|
Theorem | caovdirg 5948* |
Convert an operation reverse distributive law to class notation.
(Contributed by Mario Carneiro, 19-Oct-2014.)
|
|
|
Theorem | caovdird 5949* |
Convert an operation distributive law to class notation. (Contributed
by Mario Carneiro, 30-Dec-2014.)
|
|
|
Theorem | caovdi 5950* |
Convert an operation distributive law to class notation. (Contributed
by NM, 25-Aug-1995.) (Revised by Mario Carneiro, 28-Jun-2013.)
|
|
|
Theorem | caov32d 5951* |
Rearrange arguments in a commutative, associative operation.
(Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro,
30-Dec-2014.)
|
|
|
Theorem | caov12d 5952* |
Rearrange arguments in a commutative, associative operation.
(Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro,
30-Dec-2014.)
|
|
|
Theorem | caov31d 5953* |
Rearrange arguments in a commutative, associative operation.
(Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro,
30-Dec-2014.)
|
|
|
Theorem | caov13d 5954* |
Rearrange arguments in a commutative, associative operation.
(Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro,
30-Dec-2014.)
|
|
|
Theorem | caov4d 5955* |
Rearrange arguments in a commutative, associative operation.
(Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro,
30-Dec-2014.)
|
|
|
Theorem | caov411d 5956* |
Rearrange arguments in a commutative, associative operation.
(Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro,
30-Dec-2014.)
|
|
|
Theorem | caov42d 5957* |
Rearrange arguments in a commutative, associative operation.
(Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro,
30-Dec-2014.)
|
|
|
Theorem | caov32 5958* |
Rearrange arguments in a commutative, associative operation.
(Contributed by NM, 26-Aug-1995.)
|
|
|
Theorem | caov12 5959* |
Rearrange arguments in a commutative, associative operation.
(Contributed by NM, 26-Aug-1995.)
|
|
|
Theorem | caov31 5960* |
Rearrange arguments in a commutative, associative operation.
(Contributed by NM, 26-Aug-1995.)
|
|
|
Theorem | caov13 5961* |
Rearrange arguments in a commutative, associative operation.
(Contributed by NM, 26-Aug-1995.)
|
|
|
Theorem | caovdilemd 5962* |
Lemma used by real number construction. (Contributed by Jim Kingdon,
16-Sep-2019.)
|
|
|
Theorem | caovlem2d 5963* |
Rearrangement of expression involving multiplication () and
addition ().
(Contributed by Jim Kingdon, 3-Jan-2020.)
|
|
|
Theorem | caovimo 5964* |
Uniqueness of inverse element in commutative, associative operation with
identity. The identity element is . (Contributed by Jim Kingdon,
18-Sep-2019.)
|
|
|
Theorem | grprinvlem 5965* |
Lemma for grprinvd 5966. (Contributed by NM, 9-Aug-2013.)
|
|
|
Theorem | grprinvd 5966* |
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 5967* |
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.11 Maps-to notation
|
|
Theorem | elmpocl 5968* |
If a two-parameter class is inhabited, constrain the implicit pair.
(Contributed by Stefan O'Rear, 7-Mar-2015.)
|
|
|
Theorem | elmpocl1 5969* |
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 5970* |
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 5971* |
Utility lemma for two-parameter classes. (Contributed by Stefan O'Rear,
21-Jan-2015.)
|
|
|
Theorem | f1ocnvd 5972* |
Describe an implicit one-to-one onto function. (Contributed by Mario
Carneiro, 30-Apr-2015.)
|
|
|
Theorem | f1od 5973* |
Describe an implicit one-to-one onto function. (Contributed by Mario
Carneiro, 12-May-2014.)
|
|
|
Theorem | f1ocnv2d 5974* |
Describe an implicit one-to-one onto function. (Contributed by Mario
Carneiro, 30-Apr-2015.)
|
|
|
Theorem | f1o2d 5975* |
Describe an implicit one-to-one onto function. (Contributed by Mario
Carneiro, 12-May-2014.)
|
|
|
Theorem | f1opw2 5976* |
A one-to-one mapping induces a one-to-one mapping on power sets. This
version of f1opw 5977 avoids the Axiom of Replacement.
(Contributed by
Mario Carneiro, 26-Jun-2015.)
|
|
|
Theorem | f1opw 5977* |
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 5978* |
Formula building theorem for support restriction, on a function which
preserves zero. (Contributed by Stefan O'Rear, 9-Mar-2015.)
|
|
|
Theorem | suppssov1 5979* |
Formula building theorem for support restrictions: operator with left
annihilator. (Contributed by Stefan O'Rear, 9-Mar-2015.)
|
|
|
2.6.12 Function operation
|
|
Syntax | cof 5980 |
Extend class notation to include mapping of an operation to a function
operation.
|
|
|
Syntax | cofr 5981 |
Extend class notation to include mapping of a binary relation to a
function relation.
|
|
|
Definition | df-of 5982* |
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 5983* |
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 5984 |
Equality theorem for function operation. (Contributed by Mario
Carneiro, 20-Jul-2014.)
|
|
|
Theorem | ofreq 5985 |
Equality theorem for function relation. (Contributed by Mario Carneiro,
28-Jul-2014.)
|
|
|
Theorem | ofexg 5986 |
A function operation restricted to a set is a set. (Contributed by NM,
28-Jul-2014.)
|
|
|
Theorem | nfof 5987 |
Hypothesis builder for function operation. (Contributed by Mario
Carneiro, 20-Jul-2014.)
|
|
|
Theorem | nfofr 5988 |
Hypothesis builder for function relation. (Contributed by Mario
Carneiro, 28-Jul-2014.)
|
|
|
Theorem | offval 5989* |
Value of an operation applied to two functions. (Contributed by Mario
Carneiro, 20-Jul-2014.)
|
|
|
Theorem | ofrfval 5990* |
Value of a relation applied to two functions. (Contributed by Mario
Carneiro, 28-Jul-2014.)
|
|
|
Theorem | ofvalg 5991 |
Evaluate a function operation at a point. (Contributed by Mario
Carneiro, 20-Jul-2014.) (Revised by Jim Kingdon, 22-Nov-2023.)
|
|
|
Theorem | ofrval 5992 |
Exhibit a function relation at a point. (Contributed by Mario
Carneiro, 28-Jul-2014.)
|
|
|
Theorem | ofmresval 5993 |
Value of a restriction of the function operation map. (Contributed by
NM, 20-Oct-2014.)
|
|
|
Theorem | off 5994* |
The function operation produces a function. (Contributed by Mario
Carneiro, 20-Jul-2014.)
|
|
|
Theorem | offeq 5995* |
Convert an identity of the operation to the analogous identity on
the function operation. (Contributed by Jim Kingdon,
26-Nov-2023.)
|
|
|
Theorem | ofres 5996 |
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 5997* |
The function operation expressed as a mapping. (Contributed by Mario
Carneiro, 20-Jul-2014.)
|
|
|
Theorem | ofrfval2 5998* |
The function relation acting on maps. (Contributed by Mario Carneiro,
20-Jul-2014.)
|
|
|
Theorem | suppssof1 5999* |
Formula building theorem for support restrictions: vector operation with
left annihilator. (Contributed by Stefan O'Rear, 9-Mar-2015.)
|
|
|
Theorem | ofco 6000 |
The composition of a function operation with another function.
(Contributed by Mario Carneiro, 19-Dec-2014.)
|
|