Theorem List for Intuitionistic Logic Explorer - 6601-6700 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | erth2 6601 |
Basic property of equivalence relations. Compare Theorem 73 of [Suppes]
p. 82. Assumes membership of the second argument in the domain.
(Contributed by NM, 30-Jul-1995.) (Revised by Mario Carneiro,
6-Jul-2015.)
|
          ![] ]](rbrack.gif)   ![] ]](rbrack.gif)    |
|
Theorem | erthi 6602 |
Basic property of equivalence relations. Part of Lemma 3N of [Enderton]
p. 57. (Contributed by NM, 30-Jul-1995.) (Revised by Mario Carneiro,
9-Jul-2014.)
|
         ![] ]](rbrack.gif)   ![] ]](rbrack.gif)   |
|
Theorem | ecidsn 6603 |
An equivalence class modulo the identity relation is a singleton.
(Contributed by NM, 24-Oct-2004.)
|
     |
|
Theorem | qseq1 6604 |
Equality theorem for quotient set. (Contributed by NM, 23-Jul-1995.)
|
    
      |
|
Theorem | qseq2 6605 |
Equality theorem for quotient set. (Contributed by NM, 23-Jul-1995.)
|
    
      |
|
Theorem | elqsg 6606* |
Closed form of elqs 6607. (Contributed by Rodolfo Medina,
12-Oct-2010.)
|
      
  ![] ]](rbrack.gif)    |
|
Theorem | elqs 6607* |
Membership in a quotient set. (Contributed by NM, 23-Jul-1995.)
|
     
  ![] ]](rbrack.gif)   |
|
Theorem | elqsi 6608* |
Membership in a quotient set. (Contributed by NM, 23-Jul-1995.)
|
     
  ![] ]](rbrack.gif)   |
|
Theorem | ecelqsg 6609 |
Membership of an equivalence class in a quotient set. (Contributed by
Jeff Madsen, 10-Jun-2010.) (Revised by Mario Carneiro, 9-Jul-2014.)
|
     ![] ]](rbrack.gif)
      |
|
Theorem | ecelqsi 6610 |
Membership of an equivalence class in a quotient set. (Contributed by
NM, 25-Jul-1995.) (Revised by Mario Carneiro, 9-Jul-2014.)
|
   ![] ]](rbrack.gif)
      |
|
Theorem | ecopqsi 6611 |
"Closure" law for equivalence class of ordered pairs. (Contributed
by
NM, 25-Mar-1996.)
|
              ![] ]](rbrack.gif)   |
|
Theorem | qsexg 6612 |
A quotient set exists. (Contributed by FL, 19-May-2007.) (Revised by
Mario Carneiro, 9-Jul-2014.)
|
    
  |
|
Theorem | qsex 6613 |
A quotient set exists. (Contributed by NM, 14-Aug-1995.)
|
   
 |
|
Theorem | uniqs 6614 |
The union of a quotient set. (Contributed by NM, 9-Dec-2008.)
|
     
      |
|
Theorem | qsss 6615 |
A quotient set is a set of subsets of the base set. (Contributed by
Mario Carneiro, 9-Jul-2014.) (Revised by Mario Carneiro,
12-Aug-2015.)
|
          |
|
Theorem | uniqs2 6616 |
The union of a quotient set. (Contributed by Mario Carneiro,
11-Jul-2014.)
|
         
  |
|
Theorem | snec 6617 |
The singleton of an equivalence class. (Contributed by NM,
29-Jan-1999.) (Revised by Mario Carneiro, 9-Jul-2014.)
|
   ![] ]](rbrack.gif)         |
|
Theorem | ecqs 6618 |
Equivalence class in terms of quotient set. (Contributed by NM,
29-Jan-1999.)
|
  ![] ]](rbrack.gif)
        |
|
Theorem | ecid 6619 |
A set is equal to its converse epsilon coset. (Note: converse epsilon
is not an equivalence relation.) (Contributed by NM, 13-Aug-1995.)
(Revised by Mario Carneiro, 9-Jul-2014.)
|
  ![] ]](rbrack.gif)  |
|
Theorem | ecidg 6620 |
A set is equal to its converse epsilon coset. (Note: converse epsilon
is not an equivalence relation.) (Contributed by Jim Kingdon,
8-Jan-2020.)
|
   ![] ]](rbrack.gif)
  |
|
Theorem | qsid 6621 |
A set is equal to its quotient set mod converse epsilon. (Note:
converse epsilon is not an equivalence relation.) (Contributed by NM,
13-Aug-1995.) (Revised by Mario Carneiro, 9-Jul-2014.)
|
  
 |
|
Theorem | ectocld 6622* |
Implicit substitution of class for equivalence class. (Contributed by
Mario Carneiro, 9-Jul-2014.)
|
       ![] ]](rbrack.gif)             |
|
Theorem | ectocl 6623* |
Implicit substitution of class for equivalence class. (Contributed by
NM, 23-Jul-1995.) (Revised by Mario Carneiro, 9-Jul-2014.)
|
       ![] ]](rbrack.gif)    
    |
|
Theorem | elqsn0m 6624* |
An element of a quotient set is inhabited. (Contributed by Jim Kingdon,
21-Aug-2019.)
|
 
    

  |
|
Theorem | elqsn0 6625 |
A quotient set doesn't contain the empty set. (Contributed by NM,
24-Aug-1995.)
|
 
    
  |
|
Theorem | ecelqsdm 6626 |
Membership of an equivalence class in a quotient set. (Contributed by
NM, 30-Jul-1995.)
|
 
  ![] ]](rbrack.gif)
       |
|
Theorem | xpider 6627 |
A square Cartesian product is an equivalence relation (in general it's not
a poset). (Contributed by FL, 31-Jul-2009.) (Revised by Mario Carneiro,
12-Aug-2015.)
|
   |
|
Theorem | iinerm 6628* |
The intersection of a nonempty family of equivalence relations is an
equivalence relation. (Contributed by Mario Carneiro, 27-Sep-2015.)
|
  
     |
|
Theorem | riinerm 6629* |
The relative intersection of a family of equivalence relations is an
equivalence relation. (Contributed by Mario Carneiro, 27-Sep-2015.)
|
  
      
  |
|
Theorem | erinxp 6630 |
A restricted equivalence relation is an equivalence relation.
(Contributed by Mario Carneiro, 10-Jul-2015.) (Revised by Mario
Carneiro, 12-Aug-2015.)
|
           |
|
Theorem | ecinxp 6631 |
Restrict the relation in an equivalence class to a base set. (Contributed
by Mario Carneiro, 10-Jul-2015.)
|
         ![] ]](rbrack.gif)
  ![] ]](rbrack.gif)  
    |
|
Theorem | qsinxp 6632 |
Restrict the equivalence relation in a quotient set to the base set.
(Contributed by Mario Carneiro, 23-Feb-2015.)
|
    
       
      |
|
Theorem | qsel 6633 |
If an element of a quotient set contains a given element, it is equal to
the equivalence class of the element. (Contributed by Mario Carneiro,
12-Aug-2015.)
|
     
   ![] ]](rbrack.gif)   |
|
Theorem | qliftlem 6634* |
, a function lift, is
a subset of . (Contributed by
Mario Carneiro, 23-Dec-2016.)
|

   ![] ]](rbrack.gif)                 ![] ]](rbrack.gif)
      |
|
Theorem | qliftrel 6635* |
, a function lift, is
a subset of . (Contributed by
Mario Carneiro, 23-Dec-2016.)
|

   ![] ]](rbrack.gif)                 
   |
|
Theorem | qliftel 6636* |
Elementhood in the relation . (Contributed by Mario Carneiro,
23-Dec-2016.)
|

   ![] ]](rbrack.gif)                ![] ]](rbrack.gif)      
    |
|
Theorem | qliftel1 6637* |
Elementhood in the relation . (Contributed by Mario Carneiro,
23-Dec-2016.)
|

   ![] ]](rbrack.gif)                 ![] ]](rbrack.gif)     |
|
Theorem | qliftfun 6638* |
The function is the
unique function defined by
    , provided that the well-definedness condition
holds. (Contributed by Mario Carneiro, 23-Dec-2016.)
|

   ![] ]](rbrack.gif)              
       
    |
|
Theorem | qliftfund 6639* |
The function is the
unique function defined by
    , provided that the well-definedness condition
holds. (Contributed by Mario Carneiro, 23-Dec-2016.)
|

   ![] ]](rbrack.gif)                  
 
  |
|
Theorem | qliftfuns 6640* |
The function is the
unique function defined by
    , provided that the well-definedness condition
holds.
(Contributed by Mario Carneiro, 23-Dec-2016.)
|

   ![] ]](rbrack.gif)                       ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)     |
|
Theorem | qliftf 6641* |
The domain and codomain of the function . (Contributed by Mario
Carneiro, 23-Dec-2016.)
|

   ![] ]](rbrack.gif)                         |
|
Theorem | qliftval 6642* |
The value of the function . (Contributed by Mario Carneiro,
23-Dec-2016.)
|

   ![] ]](rbrack.gif)              
         ![] ]](rbrack.gif) 
  |
|
Theorem | ecoptocl 6643* |
Implicit substitution of class for equivalence class of ordered pair.
(Contributed by NM, 23-Jul-1995.)
|
            ![] ]](rbrack.gif)     
     |
|
Theorem | 2ecoptocl 6644* |
Implicit substitution of classes for equivalence classes of ordered
pairs. (Contributed by NM, 23-Jul-1995.)
|
            ![] ]](rbrack.gif)          ![] ]](rbrack.gif)        
 
      |
|
Theorem | 3ecoptocl 6645* |
Implicit substitution of classes for equivalence classes of ordered
pairs. (Contributed by NM, 9-Aug-1995.)
|
            ![] ]](rbrack.gif)          ![] ]](rbrack.gif)          ![] ]](rbrack.gif)        
 
 
  
   |
|
Theorem | brecop 6646* |
Binary relation on a quotient set. Lemma for real number construction.
(Contributed by NM, 29-Jan-1996.)
|
           
               
             
 
 
                                   
 
              |
|
Theorem | eroveu 6647* |
Lemma for eroprf 6649. (Contributed by Jeff Madsen, 10-Jun-2010.)
(Revised by Mario Carneiro, 9-Jul-2014.)
|
                                
            
         
 
  

    ![] ]](rbrack.gif)
  ![] ]](rbrack.gif)      ![] ]](rbrack.gif)    |
|
Theorem | erovlem 6648* |
Lemma for eroprf 6649. (Contributed by Jeff Madsen, 10-Jun-2010.)
(Revised by Mario Carneiro, 30-Dec-2014.)
|
                                
            
               
    ![] ]](rbrack.gif)
  ![] ]](rbrack.gif)      ![] ]](rbrack.gif)     
         ![] ]](rbrack.gif)   ![] ]](rbrack.gif)      ![] ]](rbrack.gif)      |
|
Theorem | eroprf 6649* |
Functionality of an operation defined on equivalence classes.
(Contributed by Jeff Madsen, 10-Jun-2010.) (Revised by Mario Carneiro,
30-Dec-2014.)
|
                                
            
               
    ![] ]](rbrack.gif)
  ![] ]](rbrack.gif)      ![] ]](rbrack.gif)                   |
|
Theorem | eroprf2 6650* |
Functionality of an operation defined on equivalence classes.
(Contributed by Jeff Madsen, 10-Jun-2010.)
|
 
      
       
                       
    
  
    
       |
|
Theorem | ecopoveq 6651* |
This is the first of several theorems about equivalence relations of
the kind used in construction of fractions and signed reals, involving
operations on equivalent classes of ordered pairs. This theorem
expresses the relation (specified by the hypothesis) in terms
of its operation . (Contributed by NM, 16-Aug-1995.)
|
       
               
     
         
 
        
     |
|
Theorem | ecopovsym 6652* |
Assuming the operation is commutative, show that the relation
,
specified by the first hypothesis, is symmetric.
(Contributed by NM, 27-Aug-1995.) (Revised by Mario Carneiro,
26-Apr-2015.)
|
       
               
     
      

    |
|
Theorem | ecopovtrn 6653* |
Assuming that operation is commutative (second hypothesis),
closed (third hypothesis), associative (fourth hypothesis), and has
the cancellation property (fifth hypothesis), show that the relation
,
specified by the first hypothesis, is transitive.
(Contributed by NM, 11-Feb-1996.) (Revised by Mario Carneiro,
26-Apr-2015.)
|
       
               
     
      

  
  
   
  
         
       |
|
Theorem | ecopover 6654* |
Assuming that operation is commutative (second hypothesis),
closed (third hypothesis), associative (fourth hypothesis), and has
the cancellation property (fifth hypothesis), show that the relation
,
specified by the first hypothesis, is an equivalence
relation. (Contributed by NM, 16-Feb-1996.) (Revised by Mario
Carneiro, 12-Aug-2015.)
|
       
               
     
      

  
  
   
  
         
 
   |
|
Theorem | ecopovsymg 6655* |
Assuming the operation is commutative, show that the relation
,
specified by the first hypothesis, is symmetric.
(Contributed by Jim Kingdon, 1-Sep-2019.)
|
       
               
     
                |
|
Theorem | ecopovtrng 6656* |
Assuming that operation is commutative (second hypothesis),
closed (third hypothesis), associative (fourth hypothesis), and has
the cancellation property (fifth hypothesis), show that the relation
,
specified by the first hypothesis, is transitive.
(Contributed by Jim Kingdon, 1-Sep-2019.)
|
       
               
     
                        
  
          
       |
|
Theorem | ecopoverg 6657* |
Assuming that operation is commutative (second hypothesis),
closed (third hypothesis), associative (fourth hypothesis), and has
the cancellation property (fifth hypothesis), show that the relation
,
specified by the first hypothesis, is an equivalence
relation. (Contributed by Jim Kingdon, 1-Sep-2019.)
|
       
               
     
                        
  
          
 
   |
|
Theorem | th3qlem1 6658* |
Lemma for Exercise 44 version of Theorem 3Q of [Enderton] p. 60. The
third hypothesis is the compatibility assumption. (Contributed by NM,
3-Aug-1995.) (Revised by Mario Carneiro, 9-Jul-2014.)
|
  
 
 
   
          
            
      |
|
Theorem | th3qlem2 6659* |
Lemma for Exercise 44 version of Theorem 3Q of [Enderton] p. 60,
extended to operations on ordered pairs. The fourth hypothesis is the
compatibility assumption. (Contributed by NM, 4-Aug-1995.) (Revised by
Mario Carneiro, 12-Aug-2015.)
|
       
 
 
 
       
  
  
               
                                 
    
            |
|
Theorem | th3qcor 6660* |
Corollary of Theorem 3Q of [Enderton] p. 60.
(Contributed by NM,
12-Nov-1995.) (Revised by David Abernethy, 4-Jun-2013.)
|
       
 
 
 
       
  
  
               
     
                                
    
             |
|
Theorem | th3q 6661* |
Theorem 3Q of [Enderton] p. 60, extended to
operations on ordered
pairs. (Contributed by NM, 4-Aug-1995.) (Revised by Mario Carneiro,
19-Dec-2013.)
|
       
 
 
 
       
  
  
               
     
                                
    
                
 
           
           |
|
Theorem | oviec 6662* |
Express an operation on equivalence classes of ordered pairs in terms of
equivalence class of operations on ordered pairs. See iset.mm for
additional comments describing the hypotheses. (Unnecessary distinct
variable restrictions were removed by David Abernethy, 4-Jun-2013.)
(Contributed by NM, 6-Aug-1995.) (Revised by Mario Carneiro,
4-Jun-2013.)
|
    
 

    
 
 

    
 
 

           
               
           
 
     
                 
               
           
 
   
       
 
 
    
  
 
                    
                     
 
 
 
     
    
   
              |
|
Theorem | ecovcom 6663* |
Lemma used to transfer a commutative law via an equivalence relation.
Most uses will want ecovicom 6664 instead. (Contributed by NM,
29-Aug-1995.) (Revised by David Abernethy, 4-Jun-2013.)
|
   
    
 
     
              
 
     
              
    |
|
Theorem | ecovicom 6664* |
Lemma used to transfer a commutative law via an equivalence relation.
(Contributed by Jim Kingdon, 15-Sep-2019.)
|
   
    
 
     
              
 
     
              
 
   
 
 
     
    |
|
Theorem | ecovass 6665* |
Lemma used to transfer an associative law via an equivalence relation.
In most cases ecoviass 6666 will be more useful. (Contributed by NM,
31-Aug-1995.) (Revised by David Abernethy, 4-Jun-2013.)
|
   
    
 
     
              
 
     
                           
         
 
     
              
 
       
 
    
   
  
    |
|
Theorem | ecoviass 6666* |
Lemma used to transfer an associative law via an equivalence relation.
(Contributed by Jim Kingdon, 16-Sep-2019.)
|
   
    
 
     
              
 
     
                           
         
 
     
              
 
       
 
       
 
 
   
 
   
  
   
  
    |
|
Theorem | ecovdi 6667* |
Lemma used to transfer a distributive law via an equivalence relation.
Most likely ecovidi 6668 will be more helpful. (Contributed by NM,
2-Sep-1995.) (Revised by David Abernethy, 4-Jun-2013.)
|
   
    
 
     
              
 
                    
 
                    
 
                      
     
              
 
       
 
       
 
    
             |
|
Theorem | ecovidi 6668* |
Lemma used to transfer a distributive law via an equivalence relation.
(Contributed by Jim Kingdon, 17-Sep-2019.)
|
   
    
 
     
              
 
                    
 
                    
 
                      
     
              
 
       
 
       
 
       
 
 
   
 
   
  
             |
|
2.6.26 The mapping operation
|
|
Syntax | cmap 6669 |
Extend the definition of a class to include the mapping operation. (Read
for , "the set of all functions that map
from to
.)
|
 |
|
Syntax | cpm 6670 |
Extend the definition of a class to include the partial mapping operation.
(Read for , "the set of all partial functions
that map from
to .)
|
 |
|
Definition | df-map 6671* |
Define the mapping operation or set exponentiation. The set of all
functions that map from to is
written   (see
mapval 6681). Many authors write followed by as a superscript
for this operation and rely on context to avoid confusion other
exponentiation operations (e.g., Definition 10.42 of [TakeutiZaring]
p. 95). Other authors show as a prefixed superscript, which is
read " pre
" (e.g.,
definition of [Enderton] p. 52).
Definition 8.21 of [Eisenberg] p. 125
uses the notation Map( ,
) for our   . The up-arrow is used by
Donald Knuth
for iterated exponentiation (Science 194, 1235-1242, 1976). We
adopt
the first case of his notation (simple exponentiation) and subscript it
with m to distinguish it from other kinds of exponentiation.
(Contributed by NM, 8-Dec-2003.)
|
          |
|
Definition | df-pm 6672* |
Define the partial mapping operation. A partial function from to
is a function
from a subset of to
. The set of all
partial functions from to is
written   (see
pmvalg 6680). A notation for this operation apparently
does not appear in
the literature. We use to distinguish it from the less general
set exponentiation operation (df-map 6671) . See mapsspm 6703 for
its relationship to set exponentiation. (Contributed by NM,
15-Nov-2007.)
|
    

   |
|
Theorem | mapprc 6673* |
When is a proper
class, the class of all functions mapping
to is empty.
Exercise 4.41 of [Mendelson] p. 255.
(Contributed
by NM, 8-Dec-2003.)
|
         |
|
Theorem | pmex 6674* |
The class of all partial functions from one set to another is a set.
(Contributed by NM, 15-Nov-2007.)
|
           |
|
Theorem | mapex 6675* |
The class of all functions mapping one set to another is a set. Remark
after Definition 10.24 of [Kunen] p. 31.
(Contributed by Raph Levien,
4-Dec-2003.)
|
           |
|
Theorem | fnmap 6676 |
Set exponentiation has a universal domain. (Contributed by NM,
8-Dec-2003.) (Revised by Mario Carneiro, 8-Sep-2013.)
|
   |
|
Theorem | fnpm 6677 |
Partial function exponentiation has a universal domain. (Contributed by
Mario Carneiro, 14-Nov-2013.)
|
   |
|
Theorem | reldmmap 6678 |
Set exponentiation is a well-behaved binary operator. (Contributed by
Stefan O'Rear, 27-Feb-2015.)
|
 |
|
Theorem | mapvalg 6679* |
The value of set exponentiation.   is the set of all
functions that map from to .
Definition 10.24 of [Kunen]
p. 24. (Contributed by NM, 8-Dec-2003.) (Revised by Mario Carneiro,
8-Sep-2013.)
|
    
        |
|
Theorem | pmvalg 6680* |
The value of the partial mapping operation. 
 is the set
of all partial functions that map from to . (Contributed by
NM, 15-Nov-2007.) (Revised by Mario Carneiro, 8-Sep-2013.)
|
        
   |
|
Theorem | mapval 6681* |
The value of set exponentiation (inference version).   is
the set of all functions that map from to . Definition
10.24 of [Kunen] p. 24. (Contributed by
NM, 8-Dec-2003.)
|
 
       |
|
Theorem | elmapg 6682 |
Membership relation for set exponentiation. (Contributed by NM,
17-Oct-2006.) (Revised by Mario Carneiro, 15-Nov-2014.)
|
    
        |
|
Theorem | elmapd 6683 |
Deduction form of elmapg 6682. (Contributed by BJ, 11-Apr-2020.)
|
               |
|
Theorem | mapdm0 6684 |
The empty set is the only map with empty domain. (Contributed by Glauco
Siliprandi, 11-Oct-2020.) (Proof shortened by Thierry Arnoux,
3-Dec-2021.)
|
       |
|
Theorem | elpmg 6685 |
The predicate "is a partial function". (Contributed by Mario
Carneiro,
14-Nov-2013.)
|
    
 
      |
|
Theorem | elpm2g 6686 |
The predicate "is a partial function". (Contributed by NM,
31-Dec-2013.)
|
    
          |
|
Theorem | elpm2r 6687 |
Sufficient condition for being a partial function. (Contributed by NM,
31-Dec-2013.)
|
               |
|
Theorem | elpmi 6688 |
A partial function is a function. (Contributed by Mario Carneiro,
15-Sep-2015.)
|
       
   |
|
Theorem | pmfun 6689 |
A partial function is a function. (Contributed by Mario Carneiro,
30-Jan-2014.) (Revised by Mario Carneiro, 26-Apr-2015.)
|
     |
|
Theorem | elmapex 6690 |
Eliminate antecedent for mapping theorems: domain can be taken to be a
set. (Contributed by Stefan O'Rear, 8-Oct-2014.)
|
   
   |
|
Theorem | elmapi 6691 |
A mapping is a function, forward direction only with superfluous
antecedent removed. (Contributed by Stefan O'Rear, 10-Oct-2014.)
|
         |
|
Theorem | elmapfn 6692 |
A mapping is a function with the appropriate domain. (Contributed by AV,
6-Apr-2019.)
|
     |
|
Theorem | elmapfun 6693 |
A mapping is always a function. (Contributed by Stefan O'Rear,
9-Oct-2014.) (Revised by Stefan O'Rear, 5-May-2015.)
|
     |
|
Theorem | elmapssres 6694 |
A restricted mapping is a mapping. (Contributed by Stefan O'Rear,
9-Oct-2014.) (Revised by Mario Carneiro, 5-May-2015.)
|
  
        |
|
Theorem | fpmg 6695 |
A total function is a partial function. (Contributed by Mario Carneiro,
31-Dec-2013.)
|
           |
|
Theorem | pmss12g 6696 |
Subset relation for the set of partial functions. (Contributed by Mario
Carneiro, 31-Dec-2013.)
|
    
 
      |
|
Theorem | pmresg 6697 |
Elementhood of a restricted function in the set of partial functions.
(Contributed by Mario Carneiro, 31-Dec-2013.)
|
           |
|
Theorem | elmap 6698 |
Membership relation for set exponentiation. (Contributed by NM,
8-Dec-2003.)
|
         |
|
Theorem | mapval2 6699* |
Alternate expression for the value of set exponentiation. (Contributed
by NM, 3-Nov-2007.)
|
 
  
     |
|
Theorem | elpm 6700 |
The predicate "is a partial function". (Contributed by NM,
15-Nov-2007.) (Revised by Mario Carneiro, 14-Nov-2013.)
|
   
     |