Theorem List for Intuitionistic Logic Explorer - 5501-5600 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | funfvbrb 5501 |
Two ways to say that
is in the domain of .
(Contributed by
Mario Carneiro, 1-May-2014.)
|
|
|
Theorem | fvimacnvi 5502 |
A member of a preimage is a function value argument. (Contributed by NM,
4-May-2007.)
|
|
|
Theorem | fvimacnv 5503 |
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 5171 could probably be
strengthened to a biconditional." (Contributed by Raph Levien,
20-Nov-2006.)
|
|
|
Theorem | funimass3 5504 |
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 5503 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 5505* |
A subclass of a preimage in terms of function values. (Contributed by
NM, 15-May-2007.)
|
|
|
Theorem | funconstss 5506* |
Two ways of specifying that a function is constant on a subdomain.
(Contributed by NM, 8-Mar-2007.)
|
|
|
Theorem | elpreima 5507 |
Membership in the preimage of a set under a function. (Contributed by
Jeff Madsen, 2-Sep-2009.)
|
|
|
Theorem | fniniseg 5508 |
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 5509* |
Inverse images under functions expressed as abstractions. (Contributed
by Stefan O'Rear, 1-Feb-2015.)
|
|
|
Theorem | fniniseg2 5510* |
Inverse point images under functions expressed as abstractions.
(Contributed by Stefan O'Rear, 1-Feb-2015.)
|
|
|
Theorem | fnniniseg2 5511* |
Support sets of functions expressed as abstractions. (Contributed by
Stefan O'Rear, 1-Feb-2015.)
|
|
|
Theorem | rexsupp 5512* |
Existential quantification restricted to a support. (Contributed by
Stefan O'Rear, 23-Mar-2015.)
|
|
|
Theorem | unpreima 5513 |
Preimage of a union. (Contributed by Jeff Madsen, 2-Sep-2009.)
|
|
|
Theorem | inpreima 5514 |
Preimage of an intersection. (Contributed by Jeff Madsen, 2-Sep-2009.)
(Proof shortened by Mario Carneiro, 14-Jun-2016.)
|
|
|
Theorem | difpreima 5515 |
Preimage of a difference. (Contributed by Mario Carneiro,
14-Jun-2016.)
|
|
|
Theorem | respreima 5516 |
The preimage of a restricted function. (Contributed by Jeff Madsen,
2-Sep-2009.)
|
|
|
Theorem | fimacnv 5517 |
The preimage of the codomain of a mapping is the mapping's domain.
(Contributed by FL, 25-Jan-2007.)
|
|
|
Theorem | fnopfv 5518 |
Ordered pair with function value. Part of Theorem 4.3(i) of [Monk1]
p. 41. (Contributed by NM, 30-Sep-2004.)
|
|
|
Theorem | fvelrn 5519 |
A function's value belongs to its range. (Contributed by NM,
14-Oct-1996.)
|
|
|
Theorem | fnfvelrn 5520 |
A function's value belongs to its range. (Contributed by NM,
15-Oct-1996.)
|
|
|
Theorem | ffvelrn 5521 |
A function's value belongs to its codomain. (Contributed by NM,
12-Aug-1999.)
|
|
|
Theorem | ffvelrni 5522 |
A function's value belongs to its codomain. (Contributed by NM,
6-Apr-2005.)
|
|
|
Theorem | ffvelrnda 5523 |
A function's value belongs to its codomain. (Contributed by Mario
Carneiro, 29-Dec-2016.)
|
|
|
Theorem | ffvelrnd 5524 |
A function's value belongs to its codomain. (Contributed by Mario
Carneiro, 29-Dec-2016.)
|
|
|
Theorem | rexrn 5525* |
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 5526* |
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 5527* |
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 5528* |
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 5529* |
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 5530* |
A restricted quantifier over an image set. (Contributed by Mario
Carneiro, 20-Aug-2015.)
|
|
|
Theorem | rexrnmpt 5531* |
A restricted quantifier over an image set. (Contributed by Mario
Carneiro, 20-Aug-2015.)
|
|
|
Theorem | dff2 5532 |
Alternate definition of a mapping. (Contributed by NM, 14-Nov-2007.)
|
|
|
Theorem | dff3im 5533* |
Property of a mapping. (Contributed by Jim Kingdon, 4-Jan-2019.)
|
|
|
Theorem | dff4im 5534* |
Property of a mapping. (Contributed by Jim Kingdon, 4-Jan-2019.)
|
|
|
Theorem | dffo3 5535* |
An onto mapping expressed in terms of function values. (Contributed by
NM, 29-Oct-2006.)
|
|
|
Theorem | dffo4 5536* |
Alternate definition of an onto mapping. (Contributed by NM,
20-Mar-2007.)
|
|
|
Theorem | dffo5 5537* |
Alternate definition of an onto mapping. (Contributed by NM,
20-Mar-2007.)
|
|
|
Theorem | fmpt 5538* |
Functionality of the mapping operation. (Contributed by Mario Carneiro,
26-Jul-2013.) (Revised by Mario Carneiro, 31-Aug-2015.)
|
|
|
Theorem | f1ompt 5539* |
Express bijection for a mapping operation. (Contributed by Mario
Carneiro, 30-May-2015.) (Revised by Mario Carneiro, 4-Dec-2016.)
|
|
|
Theorem | fmpti 5540* |
Functionality of the mapping operation. (Contributed by NM,
19-Mar-2005.) (Revised by Mario Carneiro, 1-Sep-2015.)
|
|
|
Theorem | fvmptelrn 5541* |
The value of a function at a point of its domain belongs to its
codomain. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
|
|
|
Theorem | fmptd 5542* |
Domain and codomain of the mapping operation; deduction form.
(Contributed by Mario Carneiro, 13-Jan-2013.)
|
|
|
Theorem | fmpttd 5543* |
Version of fmptd 5542 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 5544* |
Domain and codomain of the mapping operation; deduction form.
(Contributed by Thierry Arnoux, 4-Jun-2017.)
|
|
|
Theorem | fmptdf 5545* |
A version of fmptd 5542 using bound-variable hypothesis instead of a
distinct variable condition for . (Contributed by Glauco
Siliprandi, 29-Jun-2017.)
|
|
|
Theorem | ffnfv 5546* |
A function maps to a class to which all values belong. (Contributed by
NM, 3-Dec-2003.)
|
|
|
Theorem | ffnfvf 5547 |
A function maps to a class to which all values belong. This version of
ffnfv 5546 uses bound-variable hypotheses instead of
distinct variable
conditions. (Contributed by NM, 28-Sep-2006.)
|
|
|
Theorem | fnfvrnss 5548* |
An upper bound for range determined by function values. (Contributed by
NM, 8-Oct-2004.)
|
|
|
Theorem | rnmptss 5549* |
The range of an operation given by the maps-to notation as a subset.
(Contributed by Thierry Arnoux, 24-Sep-2017.)
|
|
|
Theorem | fmpt2d 5550* |
Domain and codomain of the mapping operation; deduction form.
(Contributed by NM, 27-Dec-2014.)
|
|
|
Theorem | ffvresb 5551* |
A necessary and sufficient condition for a restricted function.
(Contributed by Mario Carneiro, 14-Nov-2013.)
|
|
|
Theorem | resflem 5552* |
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 5552 where
is
substituted for (in both the conclusion and the third hypothesis).
(Contributed by BJ, 4-Jul-2022.)
|
|
|
Theorem | f1oresrab 5553* |
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 5554* |
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 5555* |
Version of fmptco 5554 where needn't be distinct from .
(Contributed by NM, 27-Dec-2014.)
|
|
|
Theorem | fmptcos 5556* |
Composition of two functions expressed as mapping abstractions.
(Contributed by NM, 22-May-2006.) (Revised by Mario Carneiro,
31-Aug-2015.)
|
|
|
Theorem | cofmpt 5557* |
Express composition of a maps-to function with another function in a
maps-to notation. (Contributed by Thierry Arnoux, 29-Jun-2017.)
|
|
|
Theorem | fcompt 5558* |
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 5559 |
Composition with a constant function. (Contributed by Stefan O'Rear,
11-Mar-2015.)
|
|
|
Theorem | fsn 5560 |
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 5561 |
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 5562 |
A function that maps a singleton to a class is the singleton of an
ordered pair. (Contributed by NM, 19-May-2004.)
|
|
|
Theorem | xpsng 5563 |
The cross product of two singletons. (Contributed by Mario Carneiro,
30-Apr-2015.)
|
|
|
Theorem | xpsn 5564 |
The cross product of two singletons. (Contributed by NM,
4-Nov-2006.)
|
|
|
Theorem | dfmpt 5565 |
Alternate definition for the maps-to notation df-mpt 3961 (although it
requires that
be a set). (Contributed by NM, 24-Aug-2010.)
(Revised by Mario Carneiro, 30-Dec-2016.)
|
|
|
Theorem | fnasrn 5566 |
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 5567 |
Alternate definition for the maps-to notation df-mpt 3961 (which requires
that be a set).
(Contributed by Jim Kingdon, 9-Jan-2019.)
|
|
|
Theorem | fnasrng 5568 |
A function expressed as the range of another function. (Contributed by
Jim Kingdon, 9-Jan-2019.)
|
|
|
Theorem | ressnop0 5569 |
If is not in , then the restriction of a
singleton of
to is
null. (Contributed by Scott Fenton,
15-Apr-2011.)
|
|
|
Theorem | fpr 5570 |
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 5571 |
A function with a domain of two elements. (Contributed by FL,
2-Feb-2014.)
|
|
|
Theorem | ftpg 5572 |
A function with a domain of three elements. (Contributed by Alexander van
der Vekens, 4-Dec-2017.)
|
|
|
Theorem | ftp 5573 |
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 5574 |
A function restricted to a singleton. (Contributed by NM,
9-Oct-2004.)
|
|
|
Theorem | fressnfv 5575 |
The value of a function restricted to a singleton. (Contributed by NM,
9-Oct-2004.)
|
|
|
Theorem | fvconst 5576 |
The value of a constant function. (Contributed by NM, 30-May-1999.)
|
|
|
Theorem | fmptsn 5577* |
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 5578* |
Append an additional value to a function. (Contributed by NM,
6-Jun-2006.) (Revised by Mario Carneiro, 31-Aug-2015.)
|
|
|
Theorem | fmptapd 5579* |
Append an additional value to a function. (Contributed by Thierry
Arnoux, 3-Jan-2017.)
|
|
|
Theorem | fmptpr 5580* |
Express a pair function in maps-to notation. (Contributed by Thierry
Arnoux, 3-Jan-2017.)
|
|
|
Theorem | fvresi 5581 |
The value of a restricted identity function. (Contributed by NM,
19-May-2004.)
|
|
|
Theorem | fvunsng 5582 |
Remove an ordered pair not participating in a function value.
(Contributed by Jim Kingdon, 7-Jan-2019.)
|
|
|
Theorem | fvsn 5583 |
The value of a singleton of an ordered pair is the second member.
(Contributed by NM, 12-Aug-1994.)
|
|
|
Theorem | fvsng 5584 |
The value of a singleton of an ordered pair is the second member.
(Contributed by NM, 26-Oct-2012.)
|
|
|
Theorem | fvsnun1 5585 |
The value of a function with one of its ordered pairs replaced, at the
replaced ordered pair. See also fvsnun2 5586. (Contributed by NM,
23-Sep-2007.)
|
|
|
Theorem | fvsnun2 5586 |
The value of a function with one of its ordered pairs replaced, at
arguments other than the replaced one. See also fvsnun1 5585.
(Contributed by NM, 23-Sep-2007.)
|
|
|
Theorem | fnsnsplitss 5587 |
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 5588 |
Adjoining a point to a function gives a function. (Contributed by Stefan
O'Rear, 28-Feb-2015.)
|
|
|
Theorem | fsnunfv 5589 |
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 5590 |
Recover the original function from a point-added function. (Contributed
by Stefan O'Rear, 28-Feb-2015.)
|
|
|
Theorem | funresdfunsnss 5591 |
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 5592 |
The value of a function with a domain of two elements. (Contributed by
Jeff Madsen, 20-Jun-2010.)
|
|
|
Theorem | fvpr2 5593 |
The value of a function with a domain of two elements. (Contributed by
Jeff Madsen, 20-Jun-2010.)
|
|
|
Theorem | fvpr1g 5594 |
The value of a function with a domain of (at most) two elements.
(Contributed by Alexander van der Vekens, 3-Dec-2017.)
|
|
|
Theorem | fvpr2g 5595 |
The value of a function with a domain of (at most) two elements.
(Contributed by Alexander van der Vekens, 3-Dec-2017.)
|
|
|
Theorem | fvtp1g 5596 |
The value of a function with a domain of (at most) three elements.
(Contributed by Alexander van der Vekens, 4-Dec-2017.)
|
|
|
Theorem | fvtp2g 5597 |
The value of a function with a domain of (at most) three elements.
(Contributed by Alexander van der Vekens, 4-Dec-2017.)
|
|
|
Theorem | fvtp3g 5598 |
The value of a function with a domain of (at most) three elements.
(Contributed by Alexander van der Vekens, 4-Dec-2017.)
|
|
|
Theorem | fvtp1 5599 |
The first value of a function with a domain of three elements.
(Contributed by NM, 14-Sep-2011.)
|
|
|
Theorem | fvtp2 5600 |
The second value of a function with a domain of three elements.
(Contributed by NM, 14-Sep-2011.)
|
|