Theorem List for Intuitionistic Logic Explorer - 5601-5700 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | mptrcl 5601* |
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 5602* |
Value of a function given by the maps-to notation. (Contributed by FL,
21-Jun-2010.)
|
    
      |
|
Theorem | fvmptssdm 5603* |
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 5604* |
Sufficient condition for a maps-to notation to be set-like.
(Contributed by Mario Carneiro, 3-Jul-2019.)
|
    
    
  |
|
Theorem | fvmpt2d 5605* |
Deduction version of fvmpt2 5602. (Contributed by Thierry Arnoux,
8-Dec-2016.)
|
     
           |
|
Theorem | fvmptdf 5606* |
Alternate deduction version of fvmpt 5596, suitable for iteration.
(Contributed by Mario Carneiro, 7-Jan-2017.)
|
             
       
     |
|
Theorem | fvmptdv 5607* |
Alternate deduction version of fvmpt 5596, suitable for iteration.
(Contributed by Mario Carneiro, 7-Jan-2017.)
|
             
   
     |
|
Theorem | fvmptdv2 5608* |
Alternate deduction version of fvmpt 5596, suitable for iteration.
(Contributed by Mario Carneiro, 7-Jan-2017.)
|
           
         |
|
Theorem | mpteqb 5609* |
Bidirectional equality theorem for a mapping abstraction. Equivalent to
eqfnfv 5616. (Contributed by Mario Carneiro,
14-Nov-2014.)
|
      

   |
|
Theorem | fvmptt 5610* |
Closed theorem form of fvmpt 5596. (Contributed by Scott Fenton,
21-Feb-2013.) (Revised by Mario Carneiro, 11-Sep-2015.)
|
    
            |
|
Theorem | fvmptf 5611* |
Value of a function given by an ordered-pair class abstraction. This
version of fvmptg 5595 uses bound-variable hypotheses instead of
distinct
variable conditions. (Contributed by NM, 8-Nov-2005.) (Revised by
Mario Carneiro, 15-Oct-2016.)
|
    
         
  |
|
Theorem | fvmptd3 5612* |
Deduction version of fvmpt 5596. (Contributed by Glauco Siliprandi,
23-Oct-2021.)
|
  
 
          |
|
Theorem | elfvmptrab1 5613* |
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.)
|
    ![]_ ]_](_urbrack.gif)   
  ![]_ ]_](_urbrack.gif)
 
    
  ![]_ ]_](_urbrack.gif)    |
|
Theorem | elfvmptrab 5614* |
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 5615* |
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 5616* |
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 5617* |
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 5618* |
Derive equality of functions from equality of their values.
(Contributed by Jeff Madsen, 2-Sep-2009.)
|
      
   
         |
|
Theorem | eqfnfvd 5619* |
Deduction for equality of functions. (Contributed by Mario Carneiro,
24-Jul-2014.)
|
     
             |
|
Theorem | eqfnfv2f 5620* |
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 5616 uses bound-variable hypotheses instead of
distinct variable conditions. (Contributed by NM, 29-Jan-2004.)
|
       
            |
|
Theorem | eqfunfv 5621* |
Equality of functions is determined by their values. (Contributed by
Scott Fenton, 19-Jun-2011.)
|
   
      
        |
|
Theorem | fvreseq 5622* |
Equality of restricted functions is determined by their values.
(Contributed by NM, 3-Aug-1994.)
|
          
           |
|
Theorem | fnmptfvd 5623* |
A function with a given domain is a mapping defined by its function
values. (Contributed by AV, 1-Mar-2019.)
|
  
          
          |
|
Theorem | fndmdif 5624* |
Two ways to express the locus of differences between two functions.
(Contributed by Stefan O'Rear, 17-Jan-2015.)
|
  
  
           |
|
Theorem | fndmdifcom 5625 |
The difference set between two functions is commutative. (Contributed
by Stefan O'Rear, 17-Jan-2015.)
|
  
  
   |
|
Theorem | fndmin 5626* |
Two ways to express the locus of equality between two functions.
(Contributed by Stefan O'Rear, 17-Jan-2015.)
|
  
  
           |
|
Theorem | fneqeql 5627 |
Two functions are equal iff their equalizer is the whole domain.
(Contributed by Stefan O'Rear, 7-Mar-2015.)
|
         |
|
Theorem | fneqeql2 5628 |
Two functions are equal iff their equalizer contains the whole domain.
(Contributed by Stefan O'Rear, 9-Mar-2015.)
|
   
     |
|
Theorem | fnreseql 5629 |
Two functions are equal on a subset iff their equalizer contains that
subset. (Contributed by Stefan O'Rear, 7-Mar-2015.)
|
 
     
     |
|
Theorem | chfnrn 5630* |
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 5631 |
Ordered pair with function value. Part of Theorem 4.3(i) of [Monk1]
p. 41. (Contributed by NM, 14-Oct-1996.)
|
            |
|
Theorem | funfvbrb 5632 |
Two ways to say that
is in the domain of .
(Contributed by
Mario Carneiro, 1-May-2014.)
|
           |
|
Theorem | fvimacnvi 5633 |
A member of a preimage is a function value argument. (Contributed by NM,
4-May-2007.)
|
       
      |
|
Theorem | fvimacnv 5634 |
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 5296 could probably be
strengthened to a biconditional." (Contributed by Raph Levien,
20-Nov-2006.)
|
       
        |
|
Theorem | funimass3 5635 |
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 5634 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 5636* |
A subclass of a preimage in terms of function values. (Contributed by
NM, 15-May-2007.)
|
 
       
       |
|
Theorem | funconstss 5637* |
Two ways of specifying that a function is constant on a subdomain.
(Contributed by NM, 8-Mar-2007.)
|
 
      
          |
|
Theorem | elpreima 5638 |
Membership in the preimage of a set under a function. (Contributed by
Jeff Madsen, 2-Sep-2009.)
|
           
    |
|
Theorem | fniniseg 5639 |
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 5640* |
Inverse images under functions expressed as abstractions. (Contributed
by Stefan O'Rear, 1-Feb-2015.)
|
     

       |
|
Theorem | fniniseg2 5641* |
Inverse point images under functions expressed as abstractions.
(Contributed by Stefan O'Rear, 1-Feb-2015.)
|
            
   |
|
Theorem | fnniniseg2 5642* |
Support sets of functions expressed as abstractions. (Contributed by
Stefan O'Rear, 1-Feb-2015.)
|
                  |
|
Theorem | rexsupp 5643* |
Existential quantification restricted to a support. (Contributed by
Stefan O'Rear, 23-Mar-2015.)
|
             
         |
|
Theorem | unpreima 5644 |
Preimage of a union. (Contributed by Jeff Madsen, 2-Sep-2009.)
|
                      |
|
Theorem | inpreima 5645 |
Preimage of an intersection. (Contributed by Jeff Madsen, 2-Sep-2009.)
(Proof shortened by Mario Carneiro, 14-Jun-2016.)
|
                      |
|
Theorem | difpreima 5646 |
Preimage of a difference. (Contributed by Mario Carneiro,
14-Jun-2016.)
|
                      |
|
Theorem | respreima 5647 |
The preimage of a restricted function. (Contributed by Jeff Madsen,
2-Sep-2009.)
|
                 |
|
Theorem | fimacnv 5648 |
The preimage of the codomain of a mapping is the mapping's domain.
(Contributed by FL, 25-Jan-2007.)
|
            |
|
Theorem | fnopfv 5649 |
Ordered pair with function value. Part of Theorem 4.3(i) of [Monk1]
p. 41. (Contributed by NM, 30-Sep-2004.)
|
            |
|
Theorem | fvelrn 5650 |
A function's value belongs to its range. (Contributed by NM,
14-Oct-1996.)
|
      
  |
|
Theorem | fnfvelrn 5651 |
A function's value belongs to its range. (Contributed by NM,
15-Oct-1996.)
|
      
  |
|
Theorem | ffvelcdm 5652 |
A function's value belongs to its codomain. (Contributed by NM,
12-Aug-1999.)
|
      
      |
|
Theorem | ffvelcdmi 5653 |
A function's value belongs to its codomain. (Contributed by NM,
6-Apr-2005.)
|
        
  |
|
Theorem | ffvelcdmda 5654 |
A function's value belongs to its codomain. (Contributed by Mario
Carneiro, 29-Dec-2016.)
|
            
  |
|
Theorem | ffvelcdmd 5655 |
A function's value belongs to its codomain. (Contributed by Mario
Carneiro, 29-Dec-2016.)
|
               |
|
Theorem | rexrn 5656* |
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 5657* |
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 5658* |
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 5659* |
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 5660* |
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 5661* |
A restricted quantifier over an image set. (Contributed by Mario
Carneiro, 20-Aug-2015.)
|
  
            |
|
Theorem | rexrnmpt 5662* |
A restricted quantifier over an image set. (Contributed by Mario
Carneiro, 20-Aug-2015.)
|
  
            |
|
Theorem | dff2 5663 |
Alternate definition of a mapping. (Contributed by NM, 14-Nov-2007.)
|
     
     |
|
Theorem | dff3im 5664* |
Property of a mapping. (Contributed by Jim Kingdon, 4-Jan-2019.)
|
      
  
     |
|
Theorem | dff4im 5665* |
Property of a mapping. (Contributed by Jim Kingdon, 4-Jan-2019.)
|
      
  
     |
|
Theorem | dffo3 5666* |
An onto mapping expressed in terms of function values. (Contributed by
NM, 29-Oct-2006.)
|
                   |
|
Theorem | dffo4 5667* |
Alternate definition of an onto mapping. (Contributed by NM,
20-Mar-2007.)
|
                 |
|
Theorem | dffo5 5668* |
Alternate definition of an onto mapping. (Contributed by NM,
20-Mar-2007.)
|
                 |
|
Theorem | fmpt 5669* |
Functionality of the mapping operation. (Contributed by Mario Carneiro,
26-Jul-2013.) (Revised by Mario Carneiro, 31-Aug-2015.)
|
   
      |
|
Theorem | f1ompt 5670* |
Express bijection for a mapping operation. (Contributed by Mario
Carneiro, 30-May-2015.) (Revised by Mario Carneiro, 4-Dec-2016.)
|
          
   |
|
Theorem | fmpti 5671* |
Functionality of the mapping operation. (Contributed by NM,
19-Mar-2005.) (Revised by Mario Carneiro, 1-Sep-2015.)
|
  
      |
|
Theorem | fvmptelcdm 5672* |
The value of a function at a point of its domain belongs to its
codomain. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
|
 
           |
|
Theorem | fmptd 5673* |
Domain and codomain of the mapping operation; deduction form.
(Contributed by Mario Carneiro, 13-Jan-2013.)
|
             |
|
Theorem | fmpttd 5674* |
Version of fmptd 5673 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 5675* |
Domain and codomain of the mapping operation; deduction form.
(Contributed by Thierry Arnoux, 4-Jun-2017.)
|
     
         |
|
Theorem | fmptdf 5676* |
A version of fmptd 5673 using bound-variable hypothesis instead of a
distinct variable condition for . (Contributed by Glauco
Siliprandi, 29-Jun-2017.)
|
     
         |
|
Theorem | ffnfv 5677* |
A function maps to a class to which all values belong. (Contributed by
NM, 3-Dec-2003.)
|
              |
|
Theorem | ffnfvf 5678 |
A function maps to a class to which all values belong. This version of
ffnfv 5677 uses bound-variable hypotheses instead of
distinct variable
conditions. (Contributed by NM, 28-Sep-2006.)
|
                    |
|
Theorem | fnfvrnss 5679* |
An upper bound for range determined by function values. (Contributed by
NM, 8-Oct-2004.)
|
      

  |
|
Theorem | rnmptss 5680* |
The range of an operation given by the maps-to notation as a subset.
(Contributed by Thierry Arnoux, 24-Sep-2017.)
|
   
  |
|
Theorem | fmpt2d 5681* |
Domain and codomain of the mapping operation; deduction form.
(Contributed by NM, 27-Dec-2014.)
|
                       |
|
Theorem | ffvresb 5682* |
A necessary and sufficient condition for a restricted function.
(Contributed by Mario Carneiro, 14-Nov-2013.)
|
         
   
    |
|
Theorem | resflem 5683* |
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 5683 where 
 is
substituted for (in both the conclusion and the third hypothesis).
(Contributed by BJ, 4-Jul-2022.)
|
                         |
|
Theorem | f1oresrab 5684* |
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 5685* |
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 5686* |
Version of fmptco 5685 where needn't be distinct from .
(Contributed by NM, 27-Dec-2014.)
|
           
        |
|
Theorem | fmptcos 5687* |
Composition of two functions expressed as mapping abstractions.
(Contributed by NM, 22-May-2006.) (Revised by Mario Carneiro,
31-Aug-2015.)
|
                 ![]_ ]_](_urbrack.gif)    |
|
Theorem | cofmpt 5688* |
Express composition of a maps-to function with another function in a
maps-to notation. (Contributed by Thierry Arnoux, 29-Jun-2017.)
|
       
               |
|
Theorem | fcompt 5689* |
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 5690 |
Composition with a constant function. (Contributed by Stefan O'Rear,
11-Mar-2015.)
|
    
              |
|
Theorem | fsn 5691 |
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 5692 |
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 5693 |
A function that maps a singleton to a class is the singleton of an
ordered pair. (Contributed by NM, 19-May-2004.)
|
                        |
|
Theorem | xpsng 5694 |
The cross product of two singletons. (Contributed by Mario Carneiro,
30-Apr-2015.)
|
                |
|
Theorem | xpsn 5695 |
The cross product of two singletons. (Contributed by NM,
4-Nov-2006.)
|
            |
|
Theorem | dfmpt 5696 |
Alternate definition for the maps-to notation df-mpt 4068 (although it
requires that
be a set). (Contributed by NM, 24-Aug-2010.)
(Revised by Mario Carneiro, 30-Dec-2016.)
|
         |
|
Theorem | fnasrn 5697 |
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 5698 |
Alternate definition for the maps-to notation df-mpt 4068 (which requires
that be a set).
(Contributed by Jim Kingdon, 9-Jan-2019.)
|
   
        |
|
Theorem | fnasrng 5699 |
A function expressed as the range of another function. (Contributed by
Jim Kingdon, 9-Jan-2019.)
|
   

 
    |
|
Theorem | ressnop0 5700 |
If is not in , then the restriction of a
singleton of
   to is
null. (Contributed by Scott Fenton,
15-Apr-2011.)
|
          |