Theorem List for Intuitionistic Logic Explorer - 5501-5600 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | fvmpt3i 5501* |
Value of a function given in maps-to notation, with a slightly different
sethood condition. (Contributed by Mario Carneiro, 11-Sep-2015.)
|
|
|
Theorem | fvmptd 5502* |
Deduction version of fvmpt 5498. (Contributed by Scott Fenton,
18-Feb-2013.) (Revised by Mario Carneiro, 31-Aug-2015.)
|
|
|
Theorem | mptrcl 5503* |
Reverse closure for a mapping: If the function value of a mapping has a
member, the argument belongs to the base class of the mapping.
(Contributed by AV, 4-Apr-2020.) (Revised by Jim Kingdon,
27-Mar-2023.)
|
|
|
Theorem | fvmpt2 5504* |
Value of a function given by the maps-to notation. (Contributed by FL,
21-Jun-2010.)
|
|
|
Theorem | fvmptssdm 5505* |
If all the values of the mapping are subsets of a class , then so
is any evaluation of the mapping at a value in the domain of the
mapping. (Contributed by Jim Kingdon, 3-Jan-2018.)
|
|
|
Theorem | mptfvex 5506* |
Sufficient condition for a maps-to notation to be set-like.
(Contributed by Mario Carneiro, 3-Jul-2019.)
|
|
|
Theorem | fvmpt2d 5507* |
Deduction version of fvmpt2 5504. (Contributed by Thierry Arnoux,
8-Dec-2016.)
|
|
|
Theorem | fvmptdf 5508* |
Alternate deduction version of fvmpt 5498, suitable for iteration.
(Contributed by Mario Carneiro, 7-Jan-2017.)
|
|
|
Theorem | fvmptdv 5509* |
Alternate deduction version of fvmpt 5498, suitable for iteration.
(Contributed by Mario Carneiro, 7-Jan-2017.)
|
|
|
Theorem | fvmptdv2 5510* |
Alternate deduction version of fvmpt 5498, suitable for iteration.
(Contributed by Mario Carneiro, 7-Jan-2017.)
|
|
|
Theorem | mpteqb 5511* |
Bidirectional equality theorem for a mapping abstraction. Equivalent to
eqfnfv 5518. (Contributed by Mario Carneiro,
14-Nov-2014.)
|
|
|
Theorem | fvmptt 5512* |
Closed theorem form of fvmpt 5498. (Contributed by Scott Fenton,
21-Feb-2013.) (Revised by Mario Carneiro, 11-Sep-2015.)
|
|
|
Theorem | fvmptf 5513* |
Value of a function given by an ordered-pair class abstraction. This
version of fvmptg 5497 uses bound-variable hypotheses instead of
distinct
variable conditions. (Contributed by NM, 8-Nov-2005.) (Revised by
Mario Carneiro, 15-Oct-2016.)
|
|
|
Theorem | fvmptd3 5514* |
Deduction version of fvmpt 5498. (Contributed by Glauco Siliprandi,
23-Oct-2021.)
|
|
|
Theorem | elfvmptrab1 5515* |
Implications for the value of a function defined by the maps-to notation
with a class abstraction as a result having an element. Here, the base
set of the class abstraction depends on the argument of the function.
(Contributed by Alexander van der Vekens, 15-Jul-2018.)
|
|
|
Theorem | elfvmptrab 5516* |
Implications for the value of a function defined by the maps-to notation
with a class abstraction as a result having an element. (Contributed by
Alexander van der Vekens, 15-Jul-2018.)
|
|
|
Theorem | fvopab6 5517* |
Value of a function given by ordered-pair class abstraction.
(Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro,
11-Sep-2015.)
|
|
|
Theorem | eqfnfv 5518* |
Equality of functions is determined by their values. Special case of
Exercise 4 of [TakeutiZaring] p.
28 (with domain equality omitted).
(Contributed by NM, 3-Aug-1994.) (Proof shortened by Andrew Salmon,
22-Oct-2011.) (Proof shortened by Mario Carneiro, 31-Aug-2015.)
|
|
|
Theorem | eqfnfv2 5519* |
Equality of functions is determined by their values. Exercise 4 of
[TakeutiZaring] p. 28.
(Contributed by NM, 3-Aug-1994.) (Revised by
Mario Carneiro, 31-Aug-2015.)
|
|
|
Theorem | eqfnfv3 5520* |
Derive equality of functions from equality of their values.
(Contributed by Jeff Madsen, 2-Sep-2009.)
|
|
|
Theorem | eqfnfvd 5521* |
Deduction for equality of functions. (Contributed by Mario Carneiro,
24-Jul-2014.)
|
|
|
Theorem | eqfnfv2f 5522* |
Equality of functions is determined by their values. Special case of
Exercise 4 of [TakeutiZaring] p.
28 (with domain equality omitted).
This version of eqfnfv 5518 uses bound-variable hypotheses instead of
distinct variable conditions. (Contributed by NM, 29-Jan-2004.)
|
|
|
Theorem | eqfunfv 5523* |
Equality of functions is determined by their values. (Contributed by
Scott Fenton, 19-Jun-2011.)
|
|
|
Theorem | fvreseq 5524* |
Equality of restricted functions is determined by their values.
(Contributed by NM, 3-Aug-1994.)
|
|
|
Theorem | fndmdif 5525* |
Two ways to express the locus of differences between two functions.
(Contributed by Stefan O'Rear, 17-Jan-2015.)
|
|
|
Theorem | fndmdifcom 5526 |
The difference set between two functions is commutative. (Contributed
by Stefan O'Rear, 17-Jan-2015.)
|
|
|
Theorem | fndmin 5527* |
Two ways to express the locus of equality between two functions.
(Contributed by Stefan O'Rear, 17-Jan-2015.)
|
|
|
Theorem | fneqeql 5528 |
Two functions are equal iff their equalizer is the whole domain.
(Contributed by Stefan O'Rear, 7-Mar-2015.)
|
|
|
Theorem | fneqeql2 5529 |
Two functions are equal iff their equalizer contains the whole domain.
(Contributed by Stefan O'Rear, 9-Mar-2015.)
|
|
|
Theorem | fnreseql 5530 |
Two functions are equal on a subset iff their equalizer contains that
subset. (Contributed by Stefan O'Rear, 7-Mar-2015.)
|
|
|
Theorem | chfnrn 5531* |
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 5532 |
Ordered pair with function value. Part of Theorem 4.3(i) of [Monk1]
p. 41. (Contributed by NM, 14-Oct-1996.)
|
|
|
Theorem | funfvbrb 5533 |
Two ways to say that
is in the domain of .
(Contributed by
Mario Carneiro, 1-May-2014.)
|
|
|
Theorem | fvimacnvi 5534 |
A member of a preimage is a function value argument. (Contributed by NM,
4-May-2007.)
|
|
|
Theorem | fvimacnv 5535 |
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 5201 could probably be
strengthened to a biconditional." (Contributed by Raph Levien,
20-Nov-2006.)
|
|
|
Theorem | funimass3 5536 |
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 5535 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 5537* |
A subclass of a preimage in terms of function values. (Contributed by
NM, 15-May-2007.)
|
|
|
Theorem | funconstss 5538* |
Two ways of specifying that a function is constant on a subdomain.
(Contributed by NM, 8-Mar-2007.)
|
|
|
Theorem | elpreima 5539 |
Membership in the preimage of a set under a function. (Contributed by
Jeff Madsen, 2-Sep-2009.)
|
|
|
Theorem | fniniseg 5540 |
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 5541* |
Inverse images under functions expressed as abstractions. (Contributed
by Stefan O'Rear, 1-Feb-2015.)
|
|
|
Theorem | fniniseg2 5542* |
Inverse point images under functions expressed as abstractions.
(Contributed by Stefan O'Rear, 1-Feb-2015.)
|
|
|
Theorem | fnniniseg2 5543* |
Support sets of functions expressed as abstractions. (Contributed by
Stefan O'Rear, 1-Feb-2015.)
|
|
|
Theorem | rexsupp 5544* |
Existential quantification restricted to a support. (Contributed by
Stefan O'Rear, 23-Mar-2015.)
|
|
|
Theorem | unpreima 5545 |
Preimage of a union. (Contributed by Jeff Madsen, 2-Sep-2009.)
|
|
|
Theorem | inpreima 5546 |
Preimage of an intersection. (Contributed by Jeff Madsen, 2-Sep-2009.)
(Proof shortened by Mario Carneiro, 14-Jun-2016.)
|
|
|
Theorem | difpreima 5547 |
Preimage of a difference. (Contributed by Mario Carneiro,
14-Jun-2016.)
|
|
|
Theorem | respreima 5548 |
The preimage of a restricted function. (Contributed by Jeff Madsen,
2-Sep-2009.)
|
|
|
Theorem | fimacnv 5549 |
The preimage of the codomain of a mapping is the mapping's domain.
(Contributed by FL, 25-Jan-2007.)
|
|
|
Theorem | fnopfv 5550 |
Ordered pair with function value. Part of Theorem 4.3(i) of [Monk1]
p. 41. (Contributed by NM, 30-Sep-2004.)
|
|
|
Theorem | fvelrn 5551 |
A function's value belongs to its range. (Contributed by NM,
14-Oct-1996.)
|
|
|
Theorem | fnfvelrn 5552 |
A function's value belongs to its range. (Contributed by NM,
15-Oct-1996.)
|
|
|
Theorem | ffvelrn 5553 |
A function's value belongs to its codomain. (Contributed by NM,
12-Aug-1999.)
|
|
|
Theorem | ffvelrni 5554 |
A function's value belongs to its codomain. (Contributed by NM,
6-Apr-2005.)
|
|
|
Theorem | ffvelrnda 5555 |
A function's value belongs to its codomain. (Contributed by Mario
Carneiro, 29-Dec-2016.)
|
|
|
Theorem | ffvelrnd 5556 |
A function's value belongs to its codomain. (Contributed by Mario
Carneiro, 29-Dec-2016.)
|
|
|
Theorem | rexrn 5557* |
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 5558* |
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 5559* |
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 5560* |
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 5561* |
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 5562* |
A restricted quantifier over an image set. (Contributed by Mario
Carneiro, 20-Aug-2015.)
|
|
|
Theorem | rexrnmpt 5563* |
A restricted quantifier over an image set. (Contributed by Mario
Carneiro, 20-Aug-2015.)
|
|
|
Theorem | dff2 5564 |
Alternate definition of a mapping. (Contributed by NM, 14-Nov-2007.)
|
|
|
Theorem | dff3im 5565* |
Property of a mapping. (Contributed by Jim Kingdon, 4-Jan-2019.)
|
|
|
Theorem | dff4im 5566* |
Property of a mapping. (Contributed by Jim Kingdon, 4-Jan-2019.)
|
|
|
Theorem | dffo3 5567* |
An onto mapping expressed in terms of function values. (Contributed by
NM, 29-Oct-2006.)
|
|
|
Theorem | dffo4 5568* |
Alternate definition of an onto mapping. (Contributed by NM,
20-Mar-2007.)
|
|
|
Theorem | dffo5 5569* |
Alternate definition of an onto mapping. (Contributed by NM,
20-Mar-2007.)
|
|
|
Theorem | fmpt 5570* |
Functionality of the mapping operation. (Contributed by Mario Carneiro,
26-Jul-2013.) (Revised by Mario Carneiro, 31-Aug-2015.)
|
|
|
Theorem | f1ompt 5571* |
Express bijection for a mapping operation. (Contributed by Mario
Carneiro, 30-May-2015.) (Revised by Mario Carneiro, 4-Dec-2016.)
|
|
|
Theorem | fmpti 5572* |
Functionality of the mapping operation. (Contributed by NM,
19-Mar-2005.) (Revised by Mario Carneiro, 1-Sep-2015.)
|
|
|
Theorem | fvmptelrn 5573* |
The value of a function at a point of its domain belongs to its
codomain. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
|
|
|
Theorem | fmptd 5574* |
Domain and codomain of the mapping operation; deduction form.
(Contributed by Mario Carneiro, 13-Jan-2013.)
|
|
|
Theorem | fmpttd 5575* |
Version of fmptd 5574 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 5576* |
Domain and codomain of the mapping operation; deduction form.
(Contributed by Thierry Arnoux, 4-Jun-2017.)
|
|
|
Theorem | fmptdf 5577* |
A version of fmptd 5574 using bound-variable hypothesis instead of a
distinct variable condition for . (Contributed by Glauco
Siliprandi, 29-Jun-2017.)
|
|
|
Theorem | ffnfv 5578* |
A function maps to a class to which all values belong. (Contributed by
NM, 3-Dec-2003.)
|
|
|
Theorem | ffnfvf 5579 |
A function maps to a class to which all values belong. This version of
ffnfv 5578 uses bound-variable hypotheses instead of
distinct variable
conditions. (Contributed by NM, 28-Sep-2006.)
|
|
|
Theorem | fnfvrnss 5580* |
An upper bound for range determined by function values. (Contributed by
NM, 8-Oct-2004.)
|
|
|
Theorem | rnmptss 5581* |
The range of an operation given by the maps-to notation as a subset.
(Contributed by Thierry Arnoux, 24-Sep-2017.)
|
|
|
Theorem | fmpt2d 5582* |
Domain and codomain of the mapping operation; deduction form.
(Contributed by NM, 27-Dec-2014.)
|
|
|
Theorem | ffvresb 5583* |
A necessary and sufficient condition for a restricted function.
(Contributed by Mario Carneiro, 14-Nov-2013.)
|
|
|
Theorem | resflem 5584* |
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 5584 where
is
substituted for (in both the conclusion and the third hypothesis).
(Contributed by BJ, 4-Jul-2022.)
|
|
|
Theorem | f1oresrab 5585* |
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 5586* |
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 5587* |
Version of fmptco 5586 where needn't be distinct from .
(Contributed by NM, 27-Dec-2014.)
|
|
|
Theorem | fmptcos 5588* |
Composition of two functions expressed as mapping abstractions.
(Contributed by NM, 22-May-2006.) (Revised by Mario Carneiro,
31-Aug-2015.)
|
|
|
Theorem | cofmpt 5589* |
Express composition of a maps-to function with another function in a
maps-to notation. (Contributed by Thierry Arnoux, 29-Jun-2017.)
|
|
|
Theorem | fcompt 5590* |
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 5591 |
Composition with a constant function. (Contributed by Stefan O'Rear,
11-Mar-2015.)
|
|
|
Theorem | fsn 5592 |
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 5593 |
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 5594 |
A function that maps a singleton to a class is the singleton of an
ordered pair. (Contributed by NM, 19-May-2004.)
|
|
|
Theorem | xpsng 5595 |
The cross product of two singletons. (Contributed by Mario Carneiro,
30-Apr-2015.)
|
|
|
Theorem | xpsn 5596 |
The cross product of two singletons. (Contributed by NM,
4-Nov-2006.)
|
|
|
Theorem | dfmpt 5597 |
Alternate definition for the maps-to notation df-mpt 3991 (although it
requires that
be a set). (Contributed by NM, 24-Aug-2010.)
(Revised by Mario Carneiro, 30-Dec-2016.)
|
|
|
Theorem | fnasrn 5598 |
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 5599 |
Alternate definition for the maps-to notation df-mpt 3991 (which requires
that be a set).
(Contributed by Jim Kingdon, 9-Jan-2019.)
|
|
|
Theorem | fnasrng 5600 |
A function expressed as the range of another function. (Contributed by
Jim Kingdon, 9-Jan-2019.)
|
|