Theorem List for Intuitionistic Logic Explorer - 6001-6100 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | ovmpos 6001* |
Value of a function given by the maps-to notation, expressed using
explicit substitution. (Contributed by Mario Carneiro, 30-Apr-2015.)
|
       ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif) 
      ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)   |
|
Theorem | ov2gf 6002* |
The value of an operation class abstraction. A version of ovmpog 6012
using bound-variable hypotheses. (Contributed by NM, 17-Aug-2006.)
(Revised by Mario Carneiro, 19-Dec-2013.)
|
          
    
       
  |
|
Theorem | ovmpodxf 6003* |
Value of an operation given by a maps-to rule, deduction form.
(Contributed by Mario Carneiro, 29-Dec-2014.)
|
  
   
  
  
                           |
|
Theorem | ovmpodx 6004* |
Value of an operation given by a maps-to rule, deduction form.
(Contributed by Mario Carneiro, 29-Dec-2014.)
|
  
   
  
  
               |
|
Theorem | ovmpod 6005* |
Value of an operation given by a maps-to rule, deduction form.
(Contributed by Mario Carneiro, 7-Dec-2014.)
|
  
   
  
              |
|
Theorem | ovmpox 6006* |
The value of an operation class abstraction. Variant of ovmpoga 6007 which
does not require and to be
distinct. (Contributed by Jeff
Madsen, 10-Jun-2010.) (Revised by Mario Carneiro, 20-Dec-2013.)
|
    
  
       
  |
|
Theorem | ovmpoga 6007* |
Value of an operation given by a maps-to rule. (Contributed by Mario
Carneiro, 19-Dec-2013.)
|
     
       
  |
|
Theorem | ovmpoa 6008* |
Value of an operation given by a maps-to rule. (Contributed by NM,
19-Dec-2013.)
|
     

      
  |
|
Theorem | ovmpodf 6009* |
Alternate deduction version of ovmpo 6013, suitable for iteration.
(Contributed by Mario Carneiro, 7-Jan-2017.)
|
        
 
   
 
                       |
|
Theorem | ovmpodv 6010* |
Alternate deduction version of ovmpo 6013, suitable for iteration.
(Contributed by Mario Carneiro, 7-Jan-2017.)
|
        
 
   
 
        
      |
|
Theorem | ovmpodv2 6011* |
Alternate deduction version of ovmpo 6013, suitable for iteration.
(Contributed by Mario Carneiro, 7-Jan-2017.)
|
        
 
   
 
  
          |
|
Theorem | ovmpog 6012* |
Value of an operation given by a maps-to rule. Special case.
(Contributed by NM, 14-Sep-1999.) (Revised by David Abernethy,
19-Jun-2012.)
|
  

     
      |
|
Theorem | ovmpo 6013* |
Value of an operation given by a maps-to rule. Special case.
(Contributed by NM, 16-May-1995.) (Revised by David Abernethy,
19-Jun-2012.)
|
  

         
  |
|
Theorem | ovi3 6014* |
The value of an operation class abstraction. Special case.
(Contributed by NM, 28-May-1995.) (Revised by Mario Carneiro,
29-Dec-2014.)
|
    
 

    
 
 
       
   
               
         
   
            |
|
Theorem | ov6g 6015* |
The value of an operation class abstraction. Special case.
(Contributed by NM, 13-Nov-2006.)
|
           
  
        
 
         |
|
Theorem | ovg 6016* |
The value of an operation class abstraction. (Contributed by Jeff
Madsen, 10-Jun-2010.)
|
              
 
         
 
       
        |
|
Theorem | ovres 6017 |
The value of a restricted operation. (Contributed by FL, 10-Nov-2006.)
|
     
           |
|
Theorem | ovresd 6018 |
Lemma for converting metric theorems to metric space theorems.
(Contributed by Mario Carneiro, 2-Oct-2015.)
|
                   |
|
Theorem | oprssov 6019 |
The value of a member of the domain of a subclass of an operation.
(Contributed by NM, 23-Aug-2007.)
|
  

    
          |
|
Theorem | fovcdm 6020 |
An operation's value belongs to its codomain. (Contributed by NM,
27-Aug-2006.)
|
            
  |
|
Theorem | fovcdmda 6021 |
An operation's value belongs to its codomain. (Contributed by Mario
Carneiro, 29-Dec-2016.)
|
          
 
      |
|
Theorem | fovcdmd 6022 |
An operation's value belongs to its codomain. (Contributed by Mario
Carneiro, 29-Dec-2016.)
|
        
          |
|
Theorem | fnrnov 6023* |
The range of an operation expressed as a collection of the operation's
values. (Contributed by NM, 29-Oct-2006.)
|
     
       |
|
Theorem | foov 6024* |
An onto mapping of an operation expressed in terms of operation values.
(Contributed by NM, 29-Oct-2006.)
|
                        |
|
Theorem | fnovrn 6025 |
An operation's value belongs to its range. (Contributed by NM,
10-Feb-2007.)
|
  
     
  |
|
Theorem | ovelrn 6026* |
A member of an operation's range is a value of the operation.
(Contributed by NM, 7-Feb-2007.) (Revised by Mario Carneiro,
30-Jan-2014.)
|
   


       |
|
Theorem | funimassov 6027* |
Membership relation for the values of a function whose image is a
subclass. (Contributed by Mario Carneiro, 23-Dec-2013.)
|
   
       
         |
|
Theorem | ovelimab 6028* |
Operation value in an image. (Contributed by Mario Carneiro,
23-Dec-2013.) (Revised by Mario Carneiro, 29-Jan-2014.)
|
   
         
       |
|
Theorem | ovconst2 6029 |
The value of a constant operation. (Contributed by NM, 5-Nov-2006.)
|
               |
|
Theorem | caovclg 6030* |
Convert an operation closure law to class notation. (Contributed by
Mario Carneiro, 26-May-2014.)
|
  
 
       
 
      |
|
Theorem | caovcld 6031* |
Convert an operation closure law to class notation. (Contributed by
Mario Carneiro, 30-Dec-2014.)
|
  
 
                |
|
Theorem | caovcl 6032* |
Convert an operation closure law to class notation. (Contributed by NM,
4-Aug-1995.) (Revised by Mario Carneiro, 26-May-2014.)
|
              
  |
|
Theorem | caovcomg 6033* |
Convert an operation commutative law to class notation. (Contributed
by Mario Carneiro, 1-Jun-2013.)
|
  
 
           
 
          |
|
Theorem | caovcomd 6034* |
Convert an operation commutative law to class notation. (Contributed
by Mario Carneiro, 30-Dec-2014.)
|
  
 
                        |
|
Theorem | caovcom 6035* |
Convert an operation commutative law to class notation. (Contributed
by NM, 26-Aug-1995.) (Revised by Mario Carneiro, 1-Jun-2013.)
|
                 |
|
Theorem | caovassg 6036* |
Convert an operation associative law to class notation. (Contributed
by Mario Carneiro, 1-Jun-2013.) (Revised by Mario Carneiro,
26-May-2014.)
|
  
 
                   
 
                  |
|
Theorem | caovassd 6037* |
Convert an operation associative law to class notation. (Contributed
by Mario Carneiro, 30-Dec-2014.)
|
  
 
                                          |
|
Theorem | caovass 6038* |
Convert an operation associative law to class notation. (Contributed
by NM, 26-Aug-1995.) (Revised by Mario Carneiro, 26-May-2014.)
|
                       
         |
|
Theorem | caovcang 6039* |
Convert an operation cancellation law to class notation. (Contributed
by NM, 20-Aug-1995.) (Revised by Mario Carneiro, 30-Dec-2014.)
|
  
 
        
    
 
            |
|
Theorem | caovcand 6040* |
Convert an operation cancellation law to class notation. (Contributed
by Mario Carneiro, 30-Dec-2014.)
|
  
 
        
             
   
   |
|
Theorem | caovcanrd 6041* |
Commute the arguments of an operation cancellation law. (Contributed
by Mario Carneiro, 30-Dec-2014.)
|
  
 
        
           
                 
   
   |
|
Theorem | caovcan 6042* |
Convert an operation cancellation law to class notation. (Contributed
by NM, 20-Aug-1995.)
|
 
         
         
       |
|
Theorem | caovordig 6043* |
Convert an operation ordering law to class notation. (Contributed by
Mario Carneiro, 31-Dec-2014.)
|
  
 
  
              
 
  
             |
|
Theorem | caovordid 6044* |
Convert an operation ordering law to class notation. (Contributed by
Mario Carneiro, 31-Dec-2014.)
|
  
 
  
                                   |
|
Theorem | caovordg 6045* |
Convert an operation ordering law to class notation. (Contributed by
NM, 19-Feb-1996.) (Revised by Mario Carneiro, 30-Dec-2014.)
|
  
 
  
              
 
  
             |
|
Theorem | caovordd 6046* |
Convert an operation ordering law to class notation. (Contributed by
Mario Carneiro, 30-Dec-2014.)
|
  
 
  
                                   |
|
Theorem | caovord2d 6047* |
Operation ordering law with commuted arguments. (Contributed by Mario
Carneiro, 30-Dec-2014.)
|
  
 
  
                    
 
                          |
|
Theorem | caovord3d 6048* |
Ordering law. (Contributed by Mario Carneiro, 30-Dec-2014.)
|
  
 
  
                    
 
                
             |
|
Theorem | caovord 6049* |
Convert an operation ordering law to class notation. (Contributed by
NM, 19-Feb-1996.)
|

  
                             |
|
Theorem | caovord2 6050* |
Operation ordering law with commuted arguments. (Contributed by NM,
27-Feb-1996.)
|

  
                                     |
|
Theorem | caovord3 6051* |
Ordering law. (Contributed by NM, 29-Feb-1996.)
|

  
                           
             |
|
Theorem | caovdig 6052* |
Convert an operation distributive law to class notation. (Contributed
by NM, 25-Aug-1995.) (Revised by Mario Carneiro, 26-Jul-2014.)
|
  
 
                       
 
                      |
|
Theorem | caovdid 6053* |
Convert an operation distributive law to class notation. (Contributed
by Mario Carneiro, 30-Dec-2014.)
|
  
 
                                                  |
|
Theorem | caovdir2d 6054* |
Convert an operation distributive law to class notation. (Contributed
by Mario Carneiro, 30-Dec-2014.)
|
  
 
                             
 
       
 
                                |
|
Theorem | caovdirg 6055* |
Convert an operation reverse distributive law to class notation.
(Contributed by Mario Carneiro, 19-Oct-2014.)
|
  
 
                       
 
                      |
|
Theorem | caovdird 6056* |
Convert an operation distributive law to class notation. (Contributed
by Mario Carneiro, 30-Dec-2014.)
|
  
 
                                                  |
|
Theorem | caovdi 6057* |
Convert an operation distributive law to class notation. (Contributed
by NM, 25-Aug-1995.) (Revised by Mario Carneiro, 28-Jun-2013.)
|
                                         |
|
Theorem | caov32d 6058* |
Rearrange arguments in a commutative, associative operation.
(Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro,
30-Dec-2014.)
|
        
 
           
 
                                    |
|
Theorem | caov12d 6059* |
Rearrange arguments in a commutative, associative operation.
(Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro,
30-Dec-2014.)
|
        
 
           
 
                                    |
|
Theorem | caov31d 6060* |
Rearrange arguments in a commutative, associative operation.
(Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro,
30-Dec-2014.)
|
        
 
           
 
                                    |
|
Theorem | caov13d 6061* |
Rearrange arguments in a commutative, associative operation.
(Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro,
30-Dec-2014.)
|
        
 
           
 
                                    |
|
Theorem | caov4d 6062* |
Rearrange arguments in a commutative, associative operation.
(Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro,
30-Dec-2014.)
|
        
 
           
 
                    
                                   |
|
Theorem | caov411d 6063* |
Rearrange arguments in a commutative, associative operation.
(Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro,
30-Dec-2014.)
|
        
 
           
 
                    
                                   |
|
Theorem | caov42d 6064* |
Rearrange arguments in a commutative, associative operation.
(Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro,
30-Dec-2014.)
|
        
 
           
 
                    
                                   |
|
Theorem | caov32 6065* |
Rearrange arguments in a commutative, associative operation.
(Contributed by NM, 26-Aug-1995.)
|
                               
         |
|
Theorem | caov12 6066* |
Rearrange arguments in a commutative, associative operation.
(Contributed by NM, 26-Aug-1995.)
|
                                         |
|
Theorem | caov31 6067* |
Rearrange arguments in a commutative, associative operation.
(Contributed by NM, 26-Aug-1995.)
|
                               
         |
|
Theorem | caov13 6068* |
Rearrange arguments in a commutative, associative operation.
(Contributed by NM, 26-Aug-1995.)
|
                                         |
|
Theorem | caovdilemd 6069* |
Lemma used by real number construction. (Contributed by Jim Kingdon,
16-Sep-2019.)
|
  
 
           
 
                       
 
                   
 
                                                      |
|
Theorem | caovlem2d 6070* |
Rearrangement of expression involving multiplication ( ) and
addition ( ).
(Contributed by Jim Kingdon, 3-Jan-2020.)
|
  
 
           
 
                       
 
                   
 
                   
 
           
 
                   
 
                                                                                |
|
Theorem | caovimo 6071* |
Uniqueness of inverse element in commutative, associative operation with
identity. The identity element is . (Contributed by Jim Kingdon,
18-Sep-2019.)
|
 
                              
                |
|
2.6.12 Maps-to notation
|
|
Theorem | elmpocl 6072* |
If a two-parameter class is inhabited, constrain the implicit pair.
(Contributed by Stefan O'Rear, 7-Mar-2015.)
|
            |
|
Theorem | elmpocl1 6073* |
If a two-parameter class is inhabited, the first argument is in its
nominal domain. (Contributed by FL, 15-Oct-2012.) (Revised by Stefan
O'Rear, 7-Mar-2015.)
|
          |
|
Theorem | elmpocl2 6074* |
If a two-parameter class is inhabited, the second argument is in its
nominal domain. (Contributed by FL, 15-Oct-2012.) (Revised by Stefan
O'Rear, 7-Mar-2015.)
|
          |
|
Theorem | elovmpo 6075* |
Utility lemma for two-parameter classes. (Contributed by Stefan O'Rear,
21-Jan-2015.)
|
                |
|
Theorem | f1ocnvd 6076* |
Describe an implicit one-to-one onto function. (Contributed by Mario
Carneiro, 30-Apr-2015.)
|
          
 
 
               |
|
Theorem | f1od 6077* |
Describe an implicit one-to-one onto function. (Contributed by Mario
Carneiro, 12-May-2014.)
|
          
 
 
          |
|
Theorem | f1ocnv2d 6078* |
Describe an implicit one-to-one onto function. (Contributed by Mario
Carneiro, 30-Apr-2015.)
|
            
 

              |
|
Theorem | f1o2d 6079* |
Describe an implicit one-to-one onto function. (Contributed by Mario
Carneiro, 12-May-2014.)
|
            
 

         |
|
Theorem | f1opw2 6080* |
A one-to-one mapping induces a one-to-one mapping on power sets. This
version of f1opw 6081 avoids the Axiom of Replacement.
(Contributed by
Mario Carneiro, 26-Jun-2015.)
|
                                   |
|
Theorem | f1opw 6081* |
A one-to-one mapping induces a one-to-one mapping on power sets.
(Contributed by Stefan O'Rear, 18-Nov-2014.) (Revised by Mario
Carneiro, 26-Jun-2015.)
|
                    |
|
Theorem | suppssfv 6082* |
Formula building theorem for support restriction, on a function which
preserves zero. (Contributed by Stefan O'Rear, 9-Mar-2015.)
|
                       
  
           
  |
|
Theorem | suppssov1 6083* |
Formula building theorem for support restrictions: operator with left
annihilator. (Contributed by Stefan O'Rear, 9-Mar-2015.)
|
                                            
  |
|
2.6.13 Function operation
|
|
Syntax | cof 6084 |
Extend class notation to include mapping of an operation to a function
operation.
|
   |
|
Syntax | cofr 6085 |
Extend class notation to include mapping of a binary relation to a
function relation.
|
   |
|
Definition | df-of 6086* |
Define the function operation map. The definition is designed so that
if is a binary
operation, then   is the analogous operation
on functions which corresponds to applying pointwise to the values
of the functions. (Contributed by Mario Carneiro, 20-Jul-2014.)
|
  


                 |
|
Definition | df-ofr 6087* |
Define the function relation map. The definition is designed so that if
is a binary
relation, then   is the analogous relation on
functions which is true when each element of the left function relates
to the corresponding element of the right function. (Contributed by
Mario Carneiro, 28-Jul-2014.)
|
                      |
|
Theorem | ofeq 6088 |
Equality theorem for function operation. (Contributed by Mario
Carneiro, 20-Jul-2014.)
|
       |
|
Theorem | ofreq 6089 |
Equality theorem for function relation. (Contributed by Mario Carneiro,
28-Jul-2014.)
|
       |
|
Theorem | ofexg 6090 |
A function operation restricted to a set is a set. (Contributed by NM,
28-Jul-2014.)
|
      |
|
Theorem | nfof 6091 |
Hypothesis builder for function operation. (Contributed by Mario
Carneiro, 20-Jul-2014.)
|
      |
|
Theorem | nfofr 6092 |
Hypothesis builder for function relation. (Contributed by Mario
Carneiro, 28-Jul-2014.)
|
      |
|
Theorem | offval 6093* |
Value of an operation applied to two functions. (Contributed by Mario
Carneiro, 20-Jul-2014.)
|
           
            
               |
|
Theorem | ofrfval 6094* |
Value of a relation applied to two functions. (Contributed by Mario
Carneiro, 28-Jul-2014.)
|
           
            
            |
|
Theorem | ofvalg 6095 |
Evaluate a function operation at a point. (Contributed by Mario
Carneiro, 20-Jul-2014.) (Revised by Jim Kingdon, 22-Nov-2023.)
|
           

           
  

                
      |
|
Theorem | ofrval 6096 |
Exhibit a function relation at a point. (Contributed by Mario
Carneiro, 28-Jul-2014.)
|
           

           
  
        |
|
Theorem | ofmresval 6097 |
Value of a restriction of the function operation map. (Contributed by
NM, 20-Oct-2014.)
|
                     |
|
Theorem | off 6098* |
The function operation produces a function. (Contributed by Mario
Carneiro, 20-Jul-2014.)
|
  
 
           
          
            |
|
Theorem | offeq 6099* |
Convert an identity of the operation to the analogous identity on
the function operation. (Contributed by Jim Kingdon,
26-Nov-2023.)
|
  
 
           
          
                    
  
               
  |
|
Theorem | ofres 6100 |
Restrict the operands of a function operation to the same domain as that
of the operation itself. (Contributed by Mario Carneiro,
15-Sep-2014.)
|
                      
    |