Theorem List for Intuitionistic Logic Explorer - 5401-5500 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | ssimaexg 5401* |
The existence of a subimage. (Contributed by FL, 15-Apr-2007.)
|
 
               |
|
Theorem | funfvdm 5402 |
A simplified expression for the value of a function when we know it's a
function. (Contributed by Jim Kingdon, 1-Jan-2019.)
|
      
         |
|
Theorem | funfvdm2 5403* |
The value of a function. Definition of function value in [Enderton]
p. 43. (Contributed by Jim Kingdon, 1-Jan-2019.)
|
      
       |
|
Theorem | funfvdm2f 5404 |
The value of a function. Version of funfvdm2 5403 using a bound-variable
hypotheses instead of distinct variable conditions. (Contributed by Jim
Kingdon, 1-Jan-2019.)
|
     
            |
|
Theorem | fvun1 5405 |
The value of a union when the argument is in the first domain.
(Contributed by Scott Fenton, 29-Jun-2013.)
|
            
      |
|
Theorem | fvun2 5406 |
The value of a union when the argument is in the second domain.
(Contributed by Scott Fenton, 29-Jun-2013.)
|
            
      |
|
Theorem | dmfco 5407 |
Domains of a function composition. (Contributed by NM, 27-Jan-1997.)
|
         
   |
|
Theorem | fvco2 5408 |
Value of a function composition. Similar to second part of Theorem 3H
of [Enderton] p. 47. (Contributed by
NM, 9-Oct-2004.) (Proof shortened
by Andrew Salmon, 22-Oct-2011.) (Revised by Stefan O'Rear,
16-Oct-2014.)
|
        
          |
|
Theorem | fvco 5409 |
Value of a function composition. Similar to Exercise 5 of [TakeutiZaring]
p. 28. (Contributed by NM, 22-Apr-2006.) (Proof shortened by Mario
Carneiro, 26-Dec-2014.)
|
        
          |
|
Theorem | fvco3 5410 |
Value of a function composition. (Contributed by NM, 3-Jan-2004.)
(Revised by Mario Carneiro, 26-Dec-2014.)
|
      
                |
|
Theorem | fvco4 5411 |
Value of a composition. (Contributed by BJ, 7-Jul-2022.)
|
       

 
     
          |
|
Theorem | fvopab3g 5412* |
Value of a function given by ordered-pair class abstraction.
(Contributed by NM, 6-Mar-1996.) (Revised by Mario Carneiro,
28-Apr-2015.)
|
        
                     |
|
Theorem | fvopab3ig 5413* |
Value of a function given by ordered-pair class abstraction.
(Contributed by NM, 23-Oct-1999.)
|
        
                     |
|
Theorem | fvmptss2 5414* |
A mapping always evaluates to a subset of the substituted expression in
the mapping, even if this is a proper class, or we are out of the
domain. (Contributed by Mario Carneiro, 13-Feb-2015.) (Revised by
Mario Carneiro, 3-Jul-2019.)
|
 
     
 |
|
Theorem | fvmptg 5415* |
Value of a function given in maps-to notation. (Contributed by NM,
2-Oct-2007.) (Revised by Mario Carneiro, 31-Aug-2015.)
|
 
           |
|
Theorem | fvmpt 5416* |
Value of a function given in maps-to notation. (Contributed by NM,
17-Aug-2011.)
|
 
      
  |
|
Theorem | fvmpts 5417* |
Value of a function given in maps-to notation, using explicit class
substitution. (Contributed by Scott Fenton, 17-Jul-2013.) (Revised by
Mario Carneiro, 31-Aug-2015.)
|
      ![]_ ]_](_urbrack.gif)     
  ![]_ ]_](_urbrack.gif)   |
|
Theorem | fvmpt3 5418* |
Value of a function given in maps-to notation, with a slightly
different sethood condition. (Contributed by Stefan O'Rear,
30-Jan-2015.)
|
 
  
     
  |
|
Theorem | fvmpt3i 5419* |
Value of a function given in maps-to notation, with a slightly different
sethood condition. (Contributed by Mario Carneiro, 11-Sep-2015.)
|
 
      
  |
|
Theorem | fvmptd 5420* |
Deduction version of fvmpt 5416. (Contributed by Scott Fenton,
18-Feb-2013.) (Revised by Mario Carneiro, 31-Aug-2015.)
|
     
             |
|
Theorem | mptrcl 5421* |
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 5422* |
Value of a function given by the maps-to notation. (Contributed by FL,
21-Jun-2010.)
|
    
      |
|
Theorem | fvmptssdm 5423* |
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 5424* |
Sufficient condition for a maps-to notation to be set-like.
(Contributed by Mario Carneiro, 3-Jul-2019.)
|
    
    
  |
|
Theorem | fvmpt2d 5425* |
Deduction version of fvmpt2 5422. (Contributed by Thierry Arnoux,
8-Dec-2016.)
|
     
           |
|
Theorem | fvmptdf 5426* |
Alternate deduction version of fvmpt 5416, suitable for iteration.
(Contributed by Mario Carneiro, 7-Jan-2017.)
|
             
       
     |
|
Theorem | fvmptdv 5427* |
Alternate deduction version of fvmpt 5416, suitable for iteration.
(Contributed by Mario Carneiro, 7-Jan-2017.)
|
             
   
     |
|
Theorem | fvmptdv2 5428* |
Alternate deduction version of fvmpt 5416, suitable for iteration.
(Contributed by Mario Carneiro, 7-Jan-2017.)
|
           
         |
|
Theorem | mpteqb 5429* |
Bidirectional equality theorem for a mapping abstraction. Equivalent to
eqfnfv 5436. (Contributed by Mario Carneiro,
14-Nov-2014.)
|
      

   |
|
Theorem | fvmptt 5430* |
Closed theorem form of fvmpt 5416. (Contributed by Scott Fenton,
21-Feb-2013.) (Revised by Mario Carneiro, 11-Sep-2015.)
|
    
            |
|
Theorem | fvmptf 5431* |
Value of a function given by an ordered-pair class abstraction. This
version of fvmptg 5415 uses bound-variable hypotheses instead of
distinct
variable conditions. (Contributed by NM, 8-Nov-2005.) (Revised by
Mario Carneiro, 15-Oct-2016.)
|
    
         
  |
|
Theorem | fvmptd3 5432* |
Deduction version of fvmpt 5416. (Contributed by Glauco Siliprandi,
23-Oct-2021.)
|
  
 
          |
|
Theorem | elfvmptrab1 5433* |
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 5434* |
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 5435* |
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 5436* |
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 5437* |
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 5438* |
Derive equality of functions from equality of their values.
(Contributed by Jeff Madsen, 2-Sep-2009.)
|
      
   
         |
|
Theorem | eqfnfvd 5439* |
Deduction for equality of functions. (Contributed by Mario Carneiro,
24-Jul-2014.)
|
     
             |
|
Theorem | eqfnfv2f 5440* |
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 5436 uses bound-variable hypotheses instead of
distinct variable conditions. (Contributed by NM, 29-Jan-2004.)
|
       
            |
|
Theorem | eqfunfv 5441* |
Equality of functions is determined by their values. (Contributed by
Scott Fenton, 19-Jun-2011.)
|
   
      
        |
|
Theorem | fvreseq 5442* |
Equality of restricted functions is determined by their values.
(Contributed by NM, 3-Aug-1994.)
|
          
           |
|
Theorem | fndmdif 5443* |
Two ways to express the locus of differences between two functions.
(Contributed by Stefan O'Rear, 17-Jan-2015.)
|
  
  
           |
|
Theorem | fndmdifcom 5444 |
The difference set between two functions is commutative. (Contributed
by Stefan O'Rear, 17-Jan-2015.)
|
  
  
   |
|
Theorem | fndmin 5445* |
Two ways to express the locus of equality between two functions.
(Contributed by Stefan O'Rear, 17-Jan-2015.)
|
  
  
           |
|
Theorem | fneqeql 5446 |
Two functions are equal iff their equalizer is the whole domain.
(Contributed by Stefan O'Rear, 7-Mar-2015.)
|
         |
|
Theorem | fneqeql2 5447 |
Two functions are equal iff their equalizer contains the whole domain.
(Contributed by Stefan O'Rear, 9-Mar-2015.)
|
   
     |
|
Theorem | fnreseql 5448 |
Two functions are equal on a subset iff their equalizer contains that
subset. (Contributed by Stefan O'Rear, 7-Mar-2015.)
|
 
     
     |
|
Theorem | chfnrn 5449* |
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 5450 |
Ordered pair with function value. Part of Theorem 4.3(i) of [Monk1]
p. 41. (Contributed by NM, 14-Oct-1996.)
|
            |
|
Theorem | funfvbrb 5451 |
Two ways to say that
is in the domain of .
(Contributed by
Mario Carneiro, 1-May-2014.)
|
           |
|
Theorem | fvimacnvi 5452 |
A member of a preimage is a function value argument. (Contributed by NM,
4-May-2007.)
|
       
      |
|
Theorem | fvimacnv 5453 |
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 5126 could probably be
strengthened to a biconditional." (Contributed by Raph Levien,
20-Nov-2006.)
|
       
        |
|
Theorem | funimass3 5454 |
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 5453 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 5455* |
A subclass of a preimage in terms of function values. (Contributed by
NM, 15-May-2007.)
|
 
       
       |
|
Theorem | funconstss 5456* |
Two ways of specifying that a function is constant on a subdomain.
(Contributed by NM, 8-Mar-2007.)
|
 
      
          |
|
Theorem | elpreima 5457 |
Membership in the preimage of a set under a function. (Contributed by
Jeff Madsen, 2-Sep-2009.)
|
           
    |
|
Theorem | fniniseg 5458 |
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 5459* |
Inverse images under functions expressed as abstractions. (Contributed
by Stefan O'Rear, 1-Feb-2015.)
|
     

       |
|
Theorem | fniniseg2 5460* |
Inverse point images under functions expressed as abstractions.
(Contributed by Stefan O'Rear, 1-Feb-2015.)
|
            
   |
|
Theorem | fnniniseg2 5461* |
Support sets of functions expressed as abstractions. (Contributed by
Stefan O'Rear, 1-Feb-2015.)
|
                  |
|
Theorem | rexsupp 5462* |
Existential quantification restricted to a support. (Contributed by
Stefan O'Rear, 23-Mar-2015.)
|
             
         |
|
Theorem | unpreima 5463 |
Preimage of a union. (Contributed by Jeff Madsen, 2-Sep-2009.)
|
                      |
|
Theorem | inpreima 5464 |
Preimage of an intersection. (Contributed by Jeff Madsen, 2-Sep-2009.)
(Proof shortened by Mario Carneiro, 14-Jun-2016.)
|
                      |
|
Theorem | difpreima 5465 |
Preimage of a difference. (Contributed by Mario Carneiro,
14-Jun-2016.)
|
                      |
|
Theorem | respreima 5466 |
The preimage of a restricted function. (Contributed by Jeff Madsen,
2-Sep-2009.)
|
                 |
|
Theorem | fimacnv 5467 |
The preimage of the codomain of a mapping is the mapping's domain.
(Contributed by FL, 25-Jan-2007.)
|
            |
|
Theorem | fnopfv 5468 |
Ordered pair with function value. Part of Theorem 4.3(i) of [Monk1]
p. 41. (Contributed by NM, 30-Sep-2004.)
|
            |
|
Theorem | fvelrn 5469 |
A function's value belongs to its range. (Contributed by NM,
14-Oct-1996.)
|
      
  |
|
Theorem | fnfvelrn 5470 |
A function's value belongs to its range. (Contributed by NM,
15-Oct-1996.)
|
      
  |
|
Theorem | ffvelrn 5471 |
A function's value belongs to its codomain. (Contributed by NM,
12-Aug-1999.)
|
      
      |
|
Theorem | ffvelrni 5472 |
A function's value belongs to its codomain. (Contributed by NM,
6-Apr-2005.)
|
        
  |
|
Theorem | ffvelrnda 5473 |
A function's value belongs to its codomain. (Contributed by Mario
Carneiro, 29-Dec-2016.)
|
            
  |
|
Theorem | ffvelrnd 5474 |
A function's value belongs to its codomain. (Contributed by Mario
Carneiro, 29-Dec-2016.)
|
               |
|
Theorem | rexrn 5475* |
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 5476* |
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 5477* |
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 5478* |
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 5479* |
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 5480* |
A restricted quantifier over an image set. (Contributed by Mario
Carneiro, 20-Aug-2015.)
|
  
            |
|
Theorem | rexrnmpt 5481* |
A restricted quantifier over an image set. (Contributed by Mario
Carneiro, 20-Aug-2015.)
|
  
            |
|
Theorem | dff2 5482 |
Alternate definition of a mapping. (Contributed by NM, 14-Nov-2007.)
|
     
     |
|
Theorem | dff3im 5483* |
Property of a mapping. (Contributed by Jim Kingdon, 4-Jan-2019.)
|
      
  
     |
|
Theorem | dff4im 5484* |
Property of a mapping. (Contributed by Jim Kingdon, 4-Jan-2019.)
|
      
  
     |
|
Theorem | dffo3 5485* |
An onto mapping expressed in terms of function values. (Contributed by
NM, 29-Oct-2006.)
|
                   |
|
Theorem | dffo4 5486* |
Alternate definition of an onto mapping. (Contributed by NM,
20-Mar-2007.)
|
                 |
|
Theorem | dffo5 5487* |
Alternate definition of an onto mapping. (Contributed by NM,
20-Mar-2007.)
|
                 |
|
Theorem | fmpt 5488* |
Functionality of the mapping operation. (Contributed by Mario Carneiro,
26-Jul-2013.) (Revised by Mario Carneiro, 31-Aug-2015.)
|
   
      |
|
Theorem | f1ompt 5489* |
Express bijection for a mapping operation. (Contributed by Mario
Carneiro, 30-May-2015.) (Revised by Mario Carneiro, 4-Dec-2016.)
|
          
   |
|
Theorem | fmpti 5490* |
Functionality of the mapping operation. (Contributed by NM,
19-Mar-2005.) (Revised by Mario Carneiro, 1-Sep-2015.)
|
  
      |
|
Theorem | fmptd 5491* |
Domain and codomain of the mapping operation; deduction form.
(Contributed by Mario Carneiro, 13-Jan-2013.)
|
             |
|
Theorem | fmpttd 5492* |
Version of fmptd 5491 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 5493* |
Domain and codomain of the mapping operation; deduction form.
(Contributed by Thierry Arnoux, 4-Jun-2017.)
|
     
         |
|
Theorem | fmptdf 5494* |
A version of fmptd 5491 using bound-variable hypothesis instead of a
distinct variable condition for . (Contributed by Glauco
Siliprandi, 29-Jun-2017.)
|
     
         |
|
Theorem | ffnfv 5495* |
A function maps to a class to which all values belong. (Contributed by
NM, 3-Dec-2003.)
|
              |
|
Theorem | ffnfvf 5496 |
A function maps to a class to which all values belong. This version of
ffnfv 5495 uses bound-variable hypotheses instead of
distinct variable
conditions. (Contributed by NM, 28-Sep-2006.)
|
                    |
|
Theorem | fnfvrnss 5497* |
An upper bound for range determined by function values. (Contributed by
NM, 8-Oct-2004.)
|
      

  |
|
Theorem | rnmptss 5498* |
The range of an operation given by the maps-to notation as a subset.
(Contributed by Thierry Arnoux, 24-Sep-2017.)
|
   
  |
|
Theorem | fmpt2d 5499* |
Domain and codomain of the mapping operation; deduction form.
(Contributed by NM, 27-Dec-2014.)
|
                       |
|
Theorem | ffvresb 5500* |
A necessary and sufficient condition for a restricted function.
(Contributed by Mario Carneiro, 14-Nov-2013.)
|
         
   
    |