Theorem List for Intuitionistic Logic Explorer - 5601-5700 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | fndmdif 5601* |
Two ways to express the locus of differences between two functions.
(Contributed by Stefan O'Rear, 17-Jan-2015.)
|
|
|
Theorem | fndmdifcom 5602 |
The difference set between two functions is commutative. (Contributed
by Stefan O'Rear, 17-Jan-2015.)
|
|
|
Theorem | fndmin 5603* |
Two ways to express the locus of equality between two functions.
(Contributed by Stefan O'Rear, 17-Jan-2015.)
|
|
|
Theorem | fneqeql 5604 |
Two functions are equal iff their equalizer is the whole domain.
(Contributed by Stefan O'Rear, 7-Mar-2015.)
|
|
|
Theorem | fneqeql2 5605 |
Two functions are equal iff their equalizer contains the whole domain.
(Contributed by Stefan O'Rear, 9-Mar-2015.)
|
|
|
Theorem | fnreseql 5606 |
Two functions are equal on a subset iff their equalizer contains that
subset. (Contributed by Stefan O'Rear, 7-Mar-2015.)
|
|
|
Theorem | chfnrn 5607* |
The range of a choice function (a function that chooses an element from
each member of its domain) is included in the union of its domain.
(Contributed by NM, 31-Aug-1999.)
|
|
|
Theorem | funfvop 5608 |
Ordered pair with function value. Part of Theorem 4.3(i) of [Monk1]
p. 41. (Contributed by NM, 14-Oct-1996.)
|
|
|
Theorem | funfvbrb 5609 |
Two ways to say that
is in the domain of .
(Contributed by
Mario Carneiro, 1-May-2014.)
|
|
|
Theorem | fvimacnvi 5610 |
A member of a preimage is a function value argument. (Contributed by NM,
4-May-2007.)
|
|
|
Theorem | fvimacnv 5611 |
The argument of a function value belongs to the preimage of any class
containing the function value. Raph Levien remarks: "This proof is
unsatisfying, because it seems to me that funimass2 5276 could probably be
strengthened to a biconditional." (Contributed by Raph Levien,
20-Nov-2006.)
|
|
|
Theorem | funimass3 5612 |
A kind of contraposition law that infers an image subclass from a
subclass of a preimage. Raph Levien remarks: "Likely this could
be
proved directly, and fvimacnv 5611 would be the special case of being
a singleton, but it works this way round too." (Contributed by
Raph
Levien, 20-Nov-2006.)
|
|
|
Theorem | funimass5 5613* |
A subclass of a preimage in terms of function values. (Contributed by
NM, 15-May-2007.)
|
|
|
Theorem | funconstss 5614* |
Two ways of specifying that a function is constant on a subdomain.
(Contributed by NM, 8-Mar-2007.)
|
|
|
Theorem | elpreima 5615 |
Membership in the preimage of a set under a function. (Contributed by
Jeff Madsen, 2-Sep-2009.)
|
|
|
Theorem | fniniseg 5616 |
Membership in the preimage of a singleton, under a function. (Contributed
by Mario Carneiro, 12-May-2014.) (Proof shortened by Mario Carneiro,
28-Apr-2015.)
|
|
|
Theorem | fncnvima2 5617* |
Inverse images under functions expressed as abstractions. (Contributed
by Stefan O'Rear, 1-Feb-2015.)
|
|
|
Theorem | fniniseg2 5618* |
Inverse point images under functions expressed as abstractions.
(Contributed by Stefan O'Rear, 1-Feb-2015.)
|
|
|
Theorem | fnniniseg2 5619* |
Support sets of functions expressed as abstractions. (Contributed by
Stefan O'Rear, 1-Feb-2015.)
|
|
|
Theorem | rexsupp 5620* |
Existential quantification restricted to a support. (Contributed by
Stefan O'Rear, 23-Mar-2015.)
|
|
|
Theorem | unpreima 5621 |
Preimage of a union. (Contributed by Jeff Madsen, 2-Sep-2009.)
|
|
|
Theorem | inpreima 5622 |
Preimage of an intersection. (Contributed by Jeff Madsen, 2-Sep-2009.)
(Proof shortened by Mario Carneiro, 14-Jun-2016.)
|
|
|
Theorem | difpreima 5623 |
Preimage of a difference. (Contributed by Mario Carneiro,
14-Jun-2016.)
|
|
|
Theorem | respreima 5624 |
The preimage of a restricted function. (Contributed by Jeff Madsen,
2-Sep-2009.)
|
|
|
Theorem | fimacnv 5625 |
The preimage of the codomain of a mapping is the mapping's domain.
(Contributed by FL, 25-Jan-2007.)
|
|
|
Theorem | fnopfv 5626 |
Ordered pair with function value. Part of Theorem 4.3(i) of [Monk1]
p. 41. (Contributed by NM, 30-Sep-2004.)
|
|
|
Theorem | fvelrn 5627 |
A function's value belongs to its range. (Contributed by NM,
14-Oct-1996.)
|
|
|
Theorem | fnfvelrn 5628 |
A function's value belongs to its range. (Contributed by NM,
15-Oct-1996.)
|
|
|
Theorem | ffvelrn 5629 |
A function's value belongs to its codomain. (Contributed by NM,
12-Aug-1999.)
|
|
|
Theorem | ffvelrni 5630 |
A function's value belongs to its codomain. (Contributed by NM,
6-Apr-2005.)
|
|
|
Theorem | ffvelrnda 5631 |
A function's value belongs to its codomain. (Contributed by Mario
Carneiro, 29-Dec-2016.)
|
|
|
Theorem | ffvelrnd 5632 |
A function's value belongs to its codomain. (Contributed by Mario
Carneiro, 29-Dec-2016.)
|
|
|
Theorem | rexrn 5633* |
Restricted existential quantification over the range of a function.
(Contributed by Mario Carneiro, 24-Dec-2013.) (Revised by Mario
Carneiro, 20-Aug-2014.)
|
|
|
Theorem | ralrn 5634* |
Restricted universal quantification over the range of a function.
(Contributed by Mario Carneiro, 24-Dec-2013.) (Revised by Mario
Carneiro, 20-Aug-2014.)
|
|
|
Theorem | elrnrexdm 5635* |
For any element in the range of a function there is an element in the
domain of the function for which the function value is the element of
the range. (Contributed by Alexander van der Vekens, 8-Dec-2017.)
|
|
|
Theorem | elrnrexdmb 5636* |
For any element in the range of a function there is an element in the
domain of the function for which the function value is the element of
the range. (Contributed by Alexander van der Vekens, 17-Dec-2017.)
|
|
|
Theorem | eldmrexrn 5637* |
For any element in the domain of a function there is an element in the
range of the function which is the function value for the element of the
domain. (Contributed by Alexander van der Vekens, 8-Dec-2017.)
|
|
|
Theorem | ralrnmpt 5638* |
A restricted quantifier over an image set. (Contributed by Mario
Carneiro, 20-Aug-2015.)
|
|
|
Theorem | rexrnmpt 5639* |
A restricted quantifier over an image set. (Contributed by Mario
Carneiro, 20-Aug-2015.)
|
|
|
Theorem | dff2 5640 |
Alternate definition of a mapping. (Contributed by NM, 14-Nov-2007.)
|
|
|
Theorem | dff3im 5641* |
Property of a mapping. (Contributed by Jim Kingdon, 4-Jan-2019.)
|
|
|
Theorem | dff4im 5642* |
Property of a mapping. (Contributed by Jim Kingdon, 4-Jan-2019.)
|
|
|
Theorem | dffo3 5643* |
An onto mapping expressed in terms of function values. (Contributed by
NM, 29-Oct-2006.)
|
|
|
Theorem | dffo4 5644* |
Alternate definition of an onto mapping. (Contributed by NM,
20-Mar-2007.)
|
|
|
Theorem | dffo5 5645* |
Alternate definition of an onto mapping. (Contributed by NM,
20-Mar-2007.)
|
|
|
Theorem | fmpt 5646* |
Functionality of the mapping operation. (Contributed by Mario Carneiro,
26-Jul-2013.) (Revised by Mario Carneiro, 31-Aug-2015.)
|
|
|
Theorem | f1ompt 5647* |
Express bijection for a mapping operation. (Contributed by Mario
Carneiro, 30-May-2015.) (Revised by Mario Carneiro, 4-Dec-2016.)
|
|
|
Theorem | fmpti 5648* |
Functionality of the mapping operation. (Contributed by NM,
19-Mar-2005.) (Revised by Mario Carneiro, 1-Sep-2015.)
|
|
|
Theorem | fvmptelrn 5649* |
The value of a function at a point of its domain belongs to its
codomain. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
|
|
|
Theorem | fmptd 5650* |
Domain and codomain of the mapping operation; deduction form.
(Contributed by Mario Carneiro, 13-Jan-2013.)
|
|
|
Theorem | fmpttd 5651* |
Version of fmptd 5650 with inlined definition. Domain and codomain
of the
mapping operation; deduction form. (Contributed by Glauco Siliprandi,
23-Oct-2021.) (Proof shortened by BJ, 16-Aug-2022.)
|
|
|
Theorem | fmpt3d 5652* |
Domain and codomain of the mapping operation; deduction form.
(Contributed by Thierry Arnoux, 4-Jun-2017.)
|
|
|
Theorem | fmptdf 5653* |
A version of fmptd 5650 using bound-variable hypothesis instead of a
distinct variable condition for . (Contributed by Glauco
Siliprandi, 29-Jun-2017.)
|
|
|
Theorem | ffnfv 5654* |
A function maps to a class to which all values belong. (Contributed by
NM, 3-Dec-2003.)
|
|
|
Theorem | ffnfvf 5655 |
A function maps to a class to which all values belong. This version of
ffnfv 5654 uses bound-variable hypotheses instead of
distinct variable
conditions. (Contributed by NM, 28-Sep-2006.)
|
|
|
Theorem | fnfvrnss 5656* |
An upper bound for range determined by function values. (Contributed by
NM, 8-Oct-2004.)
|
|
|
Theorem | rnmptss 5657* |
The range of an operation given by the maps-to notation as a subset.
(Contributed by Thierry Arnoux, 24-Sep-2017.)
|
|
|
Theorem | fmpt2d 5658* |
Domain and codomain of the mapping operation; deduction form.
(Contributed by NM, 27-Dec-2014.)
|
|
|
Theorem | ffvresb 5659* |
A necessary and sufficient condition for a restricted function.
(Contributed by Mario Carneiro, 14-Nov-2013.)
|
|
|
Theorem | resflem 5660* |
A lemma to bound the range of a restriction. The conclusion would also
hold with in place of (provided
does not
occur in ). If
that stronger result is needed, it is however
simpler to use the instance of resflem 5660 where
is
substituted for (in both the conclusion and the third hypothesis).
(Contributed by BJ, 4-Jul-2022.)
|
|
|
Theorem | f1oresrab 5661* |
Build a bijection between restricted abstract builders, given a
bijection between the base classes, deduction version. (Contributed by
Thierry Arnoux, 17-Aug-2018.)
|
|
|
Theorem | fmptco 5662* |
Composition of two functions expressed as ordered-pair class
abstractions. If has the equation ( x + 2 ) and the
equation ( 3 * z ) then has the equation ( 3 * ( x +
2 ) ) . (Contributed by FL, 21-Jun-2012.) (Revised by Mario Carneiro,
24-Jul-2014.)
|
|
|
Theorem | fmptcof 5663* |
Version of fmptco 5662 where needn't be distinct from .
(Contributed by NM, 27-Dec-2014.)
|
|
|
Theorem | fmptcos 5664* |
Composition of two functions expressed as mapping abstractions.
(Contributed by NM, 22-May-2006.) (Revised by Mario Carneiro,
31-Aug-2015.)
|
|
|
Theorem | cofmpt 5665* |
Express composition of a maps-to function with another function in a
maps-to notation. (Contributed by Thierry Arnoux, 29-Jun-2017.)
|
|
|
Theorem | fcompt 5666* |
Express composition of two functions as a maps-to applying both in
sequence. (Contributed by Stefan O'Rear, 5-Oct-2014.) (Proof shortened
by Mario Carneiro, 27-Dec-2014.)
|
|
|
Theorem | fcoconst 5667 |
Composition with a constant function. (Contributed by Stefan O'Rear,
11-Mar-2015.)
|
|
|
Theorem | fsn 5668 |
A function maps a singleton to a singleton iff it is the singleton of an
ordered pair. (Contributed by NM, 10-Dec-2003.)
|
|
|
Theorem | fsng 5669 |
A function maps a singleton to a singleton iff it is the singleton of an
ordered pair. (Contributed by NM, 26-Oct-2012.)
|
|
|
Theorem | fsn2 5670 |
A function that maps a singleton to a class is the singleton of an
ordered pair. (Contributed by NM, 19-May-2004.)
|
|
|
Theorem | xpsng 5671 |
The cross product of two singletons. (Contributed by Mario Carneiro,
30-Apr-2015.)
|
|
|
Theorem | xpsn 5672 |
The cross product of two singletons. (Contributed by NM,
4-Nov-2006.)
|
|
|
Theorem | dfmpt 5673 |
Alternate definition for the maps-to notation df-mpt 4052 (although it
requires that
be a set). (Contributed by NM, 24-Aug-2010.)
(Revised by Mario Carneiro, 30-Dec-2016.)
|
|
|
Theorem | fnasrn 5674 |
A function expressed as the range of another function. (Contributed by
Mario Carneiro, 22-Jun-2013.) (Proof shortened by Mario Carneiro,
31-Aug-2015.)
|
|
|
Theorem | dfmptg 5675 |
Alternate definition for the maps-to notation df-mpt 4052 (which requires
that be a set).
(Contributed by Jim Kingdon, 9-Jan-2019.)
|
|
|
Theorem | fnasrng 5676 |
A function expressed as the range of another function. (Contributed by
Jim Kingdon, 9-Jan-2019.)
|
|
|
Theorem | ressnop0 5677 |
If is not in , then the restriction of a
singleton of
to is
null. (Contributed by Scott Fenton,
15-Apr-2011.)
|
|
|
Theorem | fpr 5678 |
A function with a domain of two elements. (Contributed by Jeff Madsen,
20-Jun-2010.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)
|
|
|
Theorem | fprg 5679 |
A function with a domain of two elements. (Contributed by FL,
2-Feb-2014.)
|
|
|
Theorem | ftpg 5680 |
A function with a domain of three elements. (Contributed by Alexander van
der Vekens, 4-Dec-2017.)
|
|
|
Theorem | ftp 5681 |
A function with a domain of three elements. (Contributed by Stefan
O'Rear, 17-Oct-2014.) (Proof shortened by Alexander van der Vekens,
23-Jan-2018.)
|
|
|
Theorem | fnressn 5682 |
A function restricted to a singleton. (Contributed by NM,
9-Oct-2004.)
|
|
|
Theorem | fressnfv 5683 |
The value of a function restricted to a singleton. (Contributed by NM,
9-Oct-2004.)
|
|
|
Theorem | fvconst 5684 |
The value of a constant function. (Contributed by NM, 30-May-1999.)
|
|
|
Theorem | fmptsn 5685* |
Express a singleton function in maps-to notation. (Contributed by NM,
6-Jun-2006.) (Proof shortened by Andrew Salmon, 22-Oct-2011.) (Revised
by Stefan O'Rear, 28-Feb-2015.)
|
|
|
Theorem | fmptap 5686* |
Append an additional value to a function. (Contributed by NM,
6-Jun-2006.) (Revised by Mario Carneiro, 31-Aug-2015.)
|
|
|
Theorem | fmptapd 5687* |
Append an additional value to a function. (Contributed by Thierry
Arnoux, 3-Jan-2017.)
|
|
|
Theorem | fmptpr 5688* |
Express a pair function in maps-to notation. (Contributed by Thierry
Arnoux, 3-Jan-2017.)
|
|
|
Theorem | fvresi 5689 |
The value of a restricted identity function. (Contributed by NM,
19-May-2004.)
|
|
|
Theorem | fvunsng 5690 |
Remove an ordered pair not participating in a function value.
(Contributed by Jim Kingdon, 7-Jan-2019.)
|
|
|
Theorem | fvsn 5691 |
The value of a singleton of an ordered pair is the second member.
(Contributed by NM, 12-Aug-1994.)
|
|
|
Theorem | fvsng 5692 |
The value of a singleton of an ordered pair is the second member.
(Contributed by NM, 26-Oct-2012.)
|
|
|
Theorem | fvsnun1 5693 |
The value of a function with one of its ordered pairs replaced, at the
replaced ordered pair. See also fvsnun2 5694. (Contributed by NM,
23-Sep-2007.)
|
|
|
Theorem | fvsnun2 5694 |
The value of a function with one of its ordered pairs replaced, at
arguments other than the replaced one. See also fvsnun1 5693.
(Contributed by NM, 23-Sep-2007.)
|
|
|
Theorem | fnsnsplitss 5695 |
Split a function into a single point and all the rest. (Contributed by
Stefan O'Rear, 27-Feb-2015.) (Revised by Jim Kingdon, 20-Jan-2023.)
|
|
|
Theorem | fsnunf 5696 |
Adjoining a point to a function gives a function. (Contributed by Stefan
O'Rear, 28-Feb-2015.)
|
|
|
Theorem | fsnunfv 5697 |
Recover the added point from a point-added function. (Contributed by
Stefan O'Rear, 28-Feb-2015.) (Revised by NM, 18-May-2017.)
|
|
|
Theorem | fsnunres 5698 |
Recover the original function from a point-added function. (Contributed
by Stefan O'Rear, 28-Feb-2015.)
|
|
|
Theorem | funresdfunsnss 5699 |
Restricting a function to a domain without one element of the domain of
the function, and adding a pair of this element and the function value of
the element results in a subset of the function itself. (Contributed by
AV, 2-Dec-2018.) (Revised by Jim Kingdon, 21-Jan-2023.)
|
|
|
Theorem | fvpr1 5700 |
The value of a function with a domain of two elements. (Contributed by
Jeff Madsen, 20-Jun-2010.)
|
|