Theorem List for New Foundations Explorer - 5601-5700 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | ovg 5601* |
The value of an operation class abstraction. (Contributed by Jeff
Madsen, 10-Jun-2010.)
|
|
|
Theorem | ovres 5602 |
The value of a restricted operation. (Contributed by FL, 10-Nov-2006.)
|
|
|
Theorem | oprssov 5603 |
The value of a member of the domain of a subclass of an operation.
(Contributed by set.mm contributors, 23-Aug-2007.)
|
|
|
Theorem | fovrn 5604 |
A operations's value belongs to its codomain. (Contributed by set.mm
contributors, 27-Aug-2006.)
|
|
|
Theorem | fnrnov 5605* |
The range of an operation expressed as a collection of the operation's
values. (Contributed by set.mm contributors, 29-Oct-2006.)
|
|
|
Theorem | foov 5606* |
An onto mapping of an operation expressed in terms of operation values.
(Contributed by set.mm contributors, 29-Oct-2006.)
|
|
|
Theorem | fnovrn 5607 |
An operation's value belongs to its range. (Contributed by set.mm
contributors, 10-Feb-2007.)
|
|
|
Theorem | ovelrn 5608* |
A member of an operation's range is a value of the operation.
(Contributed by set.mm contributors, 7-Feb-2007.) (Revised by Mario
Carneiro, 30-Jan-2014.)
|
|
|
Theorem | funimassov 5609* |
Membership relation for the values of a function whose image is a
subclass. (Contributed by Mario Carneiro, 23-Dec-2013.)
|
|
|
Theorem | ovelimab 5610* |
Operation value in an image. (Contributed by Mario Carneiro,
23-Dec-2013.)
|
|
|
Theorem | ovconst2 5611 |
The value of a constant operation. (Contributed by set.mm contributors,
5-Nov-2006.)
|
|
|
Theorem | oprssdm 5612* |
Domain of closure of an operation. (Contributed by set.mm contributors,
24-Aug-1995.)
|
|
|
Theorem | ndmovg 5613 |
The value of an operation outside its domain. (Contributed by set.mm
contributors, 28-Mar-2008.)
|
|
|
Theorem | ndmovcl 5614* |
The closure of an operation outside its domain, when the domain includes
the empty set. This technical lemma can make the operation more
convenient to work in some cases. It is is dependent on our particular
definitions of operation value, function value, and ordered pair.
(Contributed by set.mm contributors, 24-Sep-2004.)
|
|
|
Theorem | ndmov 5615 |
The value of an operation outside its domain. (Contributed by set.mm
contributors, 24-Aug-1995.)
|
|
|
Theorem | ndmovrcl 5616 |
Reverse closure law, when an operation's domain doesn't contain the
empty set. (Contributed by set.mm contributors, 3-Feb-1996.)
|
|
|
Theorem | ndmovcom 5617 |
Any operation is commutative outside its domain. (Contributed by
set.mm contributors, 24-Aug-1995.)
|
|
|
Theorem | ndmovass 5618 |
Any operation is associative outside its domain, if the domain doesn't
contain the empty set. (Contributed by set.mm contributors,
24-Aug-1995.)
|
|
|
Theorem | ndmovdistr 5619 |
Any operation is distributive outside its domain, if the domain
doesn't contain the empty set. (Contributed by set.mm contributors,
24-Aug-1995.)
|
|
|
Theorem | ndmovord 5620 |
Elimination of redundant antecedents in an ordering law. (Contributed
by set.mm contributors, 7-Mar-1996.)
|
|
|
Theorem | ndmovordi 5621 |
Elimination of redundant antecedent in an ordering law. (Contributed by
set.mm contributors, 25-Jun-1998.)
|
|
|
Theorem | caovcld 5622* |
Convert an operation closure law to class notation. (Contributed by
Mario Carneiro, 26-May-2014.)
|
|
|
Theorem | caovcl 5623* |
Convert an operation closure law to class notation. (Contributed by
set.mm contributors, 4-Aug-1995.) (Revised by set.mm contributors,
26-May-2014.)
|
|
|
Theorem | caovcomg 5624* |
Convert an operation commutative law to class notation. (Contributed
by set.mm contributors, 1-Jun-2013.) (Revised by Mario Carneiro,
2-Jun-2013.)
|
|
|
Theorem | caovcom 5625* |
Convert an operation commutative law to class notation. (Contributed
by set.mm contributors, 26-Aug-1995.) (Revised by Mario Carneiro,
1-Jun-2013.)
|
|
|
Theorem | caovassg 5626* |
Convert an operation associative law to class notation. (Contributed
by set.mm contributors, 1-Jun-2013.) (Revised by Mario Carneiro,
2-Jun-2013.)
|
|
|
Theorem | caovass 5627* |
Convert an operation associative law to class notation. (Contributed
by set.mm contributors, 26-Aug-1995.) (Revised by Mario Carneiro,
1-Jun-2013.)
|
|
|
Theorem | caovcan 5628* |
Convert an operation cancellation law to class notation. (Contributed
by set.mm contributors, 20-Aug-1995.)
|
|
|
Theorem | caovord 5629* |
Convert an operation ordering law to class notation. (Contributed by
set.mm contributors, 19-Feb-1996.)
|
|
|
Theorem | caovord2 5630* |
Operation ordering law with commuted arguments. (Contributed by
set.mm contributors, 27-Feb-1996.)
|
|
|
Theorem | caovord3 5631* |
Ordering law. (Contributed by set.mm contributors, 29-Feb-1996.)
|
|
|
Theorem | caovdig 5632* |
Convert an operation distributive law to class notation. (Contributed
by set.mm contributors, 25-Aug-1995.) (Revised by Mario Carneiro,
26-Jul-2014.)
|
|
|
Theorem | caovdirg 5633* |
Convert an operation reverse distributive law to class notation.
(Contributed by set.mm contributors, 19-Oct-2014.)
|
|
|
Theorem | caovdi 5634* |
Convert an operation distributive law to class notation. (Contributed
by set.mm contributors, 25-Aug-1995.) (Revised by Mario Carneiro,
28-Jun-2013.)
|
|
|
Theorem | caov32 5635* |
Rearrange arguments in a commutative, associative operation.
(Contributed by set.mm contributors, 26-Aug-1995.)
|
|
|
Theorem | caov12 5636* |
Rearrange arguments in a commutative, associative operation.
(Contributed by set.mm contributors, 26-Aug-1995.)
|
|
|
Theorem | caov31 5637* |
Rearrange arguments in a commutative, associative operation.
(Contributed by set.mm contributors, 26-Aug-1995.)
|
|
|
Theorem | caov13 5638* |
Rearrange arguments in a commutative, associative operation.
(Contributed by set.mm contributors, 26-Aug-1995.)
|
|
|
Theorem | caov4 5639* |
Rearrange arguments in a commutative, associative operation.
(Contributed by set.mm contributors, 26-Aug-1995.)
|
|
|
Theorem | caov411 5640* |
Rearrange arguments in a commutative, associative operation.
(Contributed by set.mm contributors, 26-Aug-1995.)
|
|
|
Theorem | caov42 5641* |
Rearrange arguments in a commutative, associative operation.
(Contributed by set.mm contributors, 26-Aug-1995.)
|
|
|
Theorem | caovdir 5642* |
Reverse distributive law. (Contributed by set.mm contributors,
26-Aug-1995.)
|
|
|
Theorem | caovdilem 5643* |
Lemma used by real number construction. (Contributed by set.mm
contributors, 26-Aug-1995.)
|
|
|
Theorem | caovlem2 5644* |
Lemma used in real number construction. (Contributed by set.mm
contributors, 26-Aug-1995.)
|
|
|
Theorem | caovmo 5645* |
Uniqueness of inverse element in commutative, associative operation
with identity. Remark in proof of Proposition 9-2.4 of [Gleason]
p. 119. (Contributed by set.mm contributors, 4-Mar-1996.)
|
|
|
Theorem | oprabid2 5646* |
Identity law for operator abstractions. (Contributed by Scott Fenton,
19-Apr-2021.)
|
|
|
Theorem | oprabbi2i 5647* |
Biconditional for operators. (Contributed by Scott Fenton,
19-Apr-2021.)
|
|
|
Theorem | elovex12 5648 |
Eliminate antecedent for operator values: domain and range can be taken to
be a set. (Contributed by set.mm contributors, 25-Feb-2015.)
|
|
|
Theorem | elovex1 5649 |
Eliminate antecedent for operator values: domain can be taken to be a set.
(Contributed by set.mm contributors, 25-Feb-2015.)
|
|
|
Theorem | elovex2 5650 |
Eliminate antecedent for operator values: range can be taken to be a set.
(Contributed by set.mm contributors, 25-Feb-2015.)
|
|
|
2.3.9 "Maps to" notation
|
|
Syntax | cmpt 5651 |
Extend the definition of a class to include maps-to notation for defining
a function via a rule.
|
|
|
Definition | df-mpt 5652* |
Define maps-to notation for defining a function via a rule. Read as
"the function defined by the map from (in ) to
." The class expression is the value of the function
at and
normally contains the variable . Similar to the
definition of mapping in [ChoquetDD]
p. 2. (Contributed by SF,
5-Jan-2015.)
|
|
|
Syntax | cmpt2 5653 |
Extend the definition of a class to include maps-to notation for defining
an operation via a rule.
|
|
|
Definition | df-mpt2 5654* |
Define maps-to notation for defining an operation via a rule. Read as
"the operation defined by the map from (in ) to
." An extension of df-mpt 5652 for two arguments.
(Contributed by SF, 5-Jan-2015.)
|
|
|
Theorem | mpteq12f 5655 |
An equality theorem for the maps to notation. (Contributed by Mario
Carneiro, 16-Dec-2013.)
|
|
|
Theorem | mpteq12dv 5656* |
An equality inference for the maps to notation. (Contributed by set.mm
contributors, 24-Aug-2011.) (Revised by set.mm contributors,
16-Dec-2013.)
|
|
|
Theorem | mpteq12 5657* |
An equality theorem for the maps to notation. (Contributed by set.mm
contributors, 16-Dec-2013.)
|
|
|
Theorem | mpteq1 5658* |
An equality theorem for the maps to notation. (Contributed by Mario
Carneiro, 16-Dec-2013.)
|
|
|
Theorem | mpteq2ia 5659 |
An equality inference for the maps to notation. (Contributed by Mario
Carneiro, 16-Dec-2013.)
|
|
|
Theorem | mpteq2i 5660 |
An equality inference for the maps to notation. (Contributed by Mario
Carneiro, 16-Dec-2013.)
|
|
|
Theorem | mpt2eq123 5661* |
An equality theorem for the maps to notation. (Contributed by Mario
Carneiro, 16-Dec-2013.) (Revised by Mario Carneiro, 19-Mar-2015.)
|
|
|
Theorem | mpt2eq12 5662* |
An equality theorem for the maps to notation. (Contributed by Mario
Carneiro, 16-Dec-2013.)
|
|
|
Theorem | mpt2eq123dv 5663* |
An equality deduction for the maps to notation. (Contributed by set.mm
contributors, 12-Sep-2011.)
|
|
|
Theorem | mpt2eq123i 5664 |
An equality inference for the maps to notation. (Contributed by set.mm
contributors, 15-Jul-2013.)
|
|
|
Theorem | mpteq12i 5665 |
An equality inference for the maps to notation. (Contributed by Scott
Fenton, 27-Oct-2010.)
|
|
|
Theorem | mpteq2da 5666 |
Slightly more general equality inference for the maps to notation.
(Contributed by FL, 14-Sep-2013.) (Revised by Mario Carneiro,
16-Dec-2013.)
|
|
|
Theorem | mpteq2dva 5667* |
Slightly more general equality inference for the maps to notation.
(Contributed by Scott Fenton, 25-Apr-2012.)
|
|
|
Theorem | mpteq2dv 5668* |
An equality inference for the maps to notation. (Contributed by Mario
Carneiro, 23-Aug-2014.)
|
|
|
Theorem | mpt2eq3dva 5669* |
Slightly more general equality inference for the maps to notation.
(Contributed by set.mm contributors, 17-Oct-2013.) (Revised by set.mm
contributors, 16-Dec-2013.)
|
|
|
Theorem | mpt2eq3ia 5670 |
An equality inference for the maps to notation. (Contributed by Mario
Carneiro, 16-Dec-2013.)
|
|
|
Theorem | nfmpt 5671* |
Bound-variable hypothesis builder for the maps-to notation.
(Contributed by NM, 20-Feb-2013.)
|
|
|
Theorem | nfmpt1 5672 |
Bound-variable hypothesis builder for the maps-to notation.
(Contributed by FL, 17-Feb-2008.)
|
|
|
Theorem | nfmpt21 5673 |
Bound-variable hypothesis builder for an operation in maps-to notation.
(Contributed by NM, 27-Aug-2013.)
|
|
|
Theorem | nfmpt22 5674 |
Bound-variable hypothesis builder for an operation in maps-to notation.
(Contributed by NM, 27-Aug-2013.)
|
|
|
Theorem | nfmpt2 5675* |
Bound-variable hypothesis builder for the maps-to notation.
(Contributed by NM, 20-Feb-2013.)
|
|
|
Theorem | cbvmpt 5676* |
Rule to change the bound variable in a maps-to function, using implicit
substitution. This version has bound-variable hypotheses in place of
distinct variable conditions. (Contributed by NM, 11-Sep-2011.)
|
|
|
Theorem | cbvmptv 5677* |
Rule to change the bound variable in a maps-to function, using implicit
substitution. (Contributed by Mario Carneiro, 19-Feb-2013.)
|
|
|
Theorem | cbvmpt2x 5678* |
Rule to change the bound variable in a maps-to function, using implicit
substitution. This version of cbvmpt2 5679 allows to be a function
of .
(Contributed by NM, 29-Dec-2014.)
|
|
|
Theorem | cbvmpt2 5679* |
Rule to change the bound variable in a maps-to function, using implicit
substitution. (Contributed by NM, 17-Dec-2013.)
|
|
|
Theorem | cbvmpt2v 5680* |
Rule to change the bound variable in a maps-to function, using implicit
substitution. With a longer proof analogous to cbvmpt 5676, some distinct
variable requirements could be eliminated. (Contributed by NM,
11-Jun-2013.)
|
|
|
Theorem | fconstmpt 5681* |
Representation of a constant function using the mapping operation.
(Note that
cannot appear free in .) (Contributed by set.mm
contributors, 16-Nov-2013.)
|
|
|
Theorem | mptpreima 5682* |
The preimage of a function in maps-to notation. (Contributed by Stefan
O'Rear, 25-Jan-2015.)
|
|
|
Theorem | dmmpt 5683 |
The domain of the mapping operation in general. (Contributed by Mario
Carneiro, 13-Sep-2013.)
|
|
|
Theorem | dmmptg 5684* |
The domain of the mapping operation is the stated domain, if the
function value is always a set. (Contributed by Mario Carneiro,
9-Feb-2013.)
|
|
|
Theorem | dmmptss 5685* |
The domain of a mapping is a subset of its base class. (Contributed by
Scott Fenton, 17-Jun-2013.)
|
|
|
Theorem | rnmpt 5686* |
The range of a function in maps-to notation. (Contributed by Scott
Fenton, 21-Mar-2011.)
|
|
|
Theorem | funmpt 5687 |
A function in maps-to notation is a function. (Contributed by Mario
Carneiro, 13-Jan-2013.)
|
|
|
Theorem | mptfng 5688* |
The maps-to notation defines a function with domain. (Contributed by
Scott Fenton, 21-Mar-2011.)
|
|
|
Theorem | fnmpt 5689* |
The maps-to notation defines a function with domain. (Contributed by
set.mm contributors, 9-Apr-2013.)
|
|
|
Theorem | fnmpti 5690* |
Functionality and domain of an ordered-pair class abstraction.
(Contributed by NM, 29-Jan-2004.) (Revised by Mario Carneiro,
31-Aug-2015.)
|
|
|
Theorem | dmmpti 5691* |
Domain of an ordered-pair class abstraction that specifies a function.
(Contributed by NM, 6-Sep-2005.) (Revised by Mario Carneiro,
31-Aug-2015.)
|
|
|
Theorem | fmpt 5692* |
Functionality of the mapping operation. (Contributed by Mario Carneiro,
26-Jul-2013.) (Revised by Mario Carneiro, 31-Aug-2015.)
|
|
|
Theorem | fmpti 5693* |
Functionality of the mapping operation. (Contributed by NM,
19-Mar-2005.) (Revised by Mario Carneiro, 1-Sep-2015.)
|
|
|
Theorem | fmptd 5694* |
Domain and co-domain of the mapping operation; deduction form.
(Contributed by Mario Carneiro, 13-Jan-2013.)
|
|
|
Theorem | fmpt2d 5695* |
Domain and co-domain of the mapping operation; deduction form.
(Contributed by set.mm contributors, 9-Apr-2013.)
|
|
|
Theorem | resmpt 5696* |
Restriction of the mapping operation. (Contributed by Mario Carneiro,
15-Jul-2013.)
|
|
|
Theorem | resmpt2 5697* |
Restriction of the mapping operation. (Contributed by Mario Carneiro,
17-Dec-2013.)
|
|
|
Theorem | fvmptg 5698* |
Value of a function given in maps-to notation. Analogous to
fvopab4g 5388. (Contributed by set.mm contributors,
2-Oct-2007.)
(Revised by set.mm contributors, 4-Aug-2008.)
|
|
|
Theorem | fvmpti 5699* |
Value of a function given in maps-to notation. (Contributed by Mario
Carneiro, 23-Apr-2014.)
|
|
|
Theorem | fvmpt 5700* |
Value of a function given in maps-to notation. (Contributed by set.mm
contributors, 17-Aug-2011.)
|
|