Theorem List for Intuitionistic Logic Explorer - 6201-6300 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | ecopoveq 6201* |
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 6202* |
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 6203* |
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 6204* |
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 6205* |
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 6206* |
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 6207* |
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 6208* |
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 6209* |
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 6210* |
Corollary of Theorem 3Q of [Enderton] p. 60.
(Contributed by NM,
12-Nov-1995.) (Revised by David Abernethy, 4-Jun-2013.)
|
       
 
 
 
       
  
  
               
     
                                
    
             |
|
Theorem | th3q 6211* |
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 6212* |
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 6213* |
Lemma used to transfer a commutative law via an equivalence relation.
Most uses will want ecovicom 6214 instead. (Contributed by NM,
29-Aug-1995.) (Revised by David Abernethy, 4-Jun-2013.)
|
   
    
 
     
              
 
     
              
    |
|
Theorem | ecovicom 6214* |
Lemma used to transfer a commutative law via an equivalence relation.
(Contributed by Jim Kingdon, 15-Sep-2019.)
|
   
    
 
     
              
 
     
              
 
   
 
 
     
    |
|
Theorem | ecovass 6215* |
Lemma used to transfer an associative law via an equivalence relation.
In most cases ecoviass 6216 will be more useful. (Contributed by NM,
31-Aug-1995.) (Revised by David Abernethy, 4-Jun-2013.)
|
   
    
 
     
              
 
     
                           
         
 
     
              
 
       
 
    
   
  
    |
|
Theorem | ecoviass 6216* |
Lemma used to transfer an associative law via an equivalence relation.
(Contributed by Jim Kingdon, 16-Sep-2019.)
|
   
    
 
     
              
 
     
                           
         
 
     
              
 
       
 
       
 
 
   
 
   
  
   
  
    |
|
Theorem | ecovdi 6217* |
Lemma used to transfer a distributive law via an equivalence relation.
Most likely ecovidi 6218 will be more helpful. (Contributed by NM,
2-Sep-1995.) (Revised by David Abernethy, 4-Jun-2013.)
|
   
    
 
     
              
 
                    
 
                    
 
                      
     
              
 
       
 
       
 
    
             |
|
Theorem | ecovidi 6218* |
Lemma used to transfer a distributive law via an equivalence relation.
(Contributed by Jim Kingdon, 17-Sep-2019.)
|
   
    
 
     
              
 
                    
 
                    
 
                      
     
              
 
       
 
       
 
       
 
 
   
 
   
  
             |
|
2.6.25 Equinumerosity
|
|
Syntax | cen 6219 |
Extend class definition to include the equinumerosity relation
("approximately equals" symbol)
|
 |
|
Syntax | cdom 6220 |
Extend class definition to include the dominance relation (curly
less-than-or-equal)
|
 |
|
Syntax | cfn 6221 |
Extend class definition to include the class of all finite sets.
|
 |
|
Definition | df-en 6222* |
Define the equinumerosity relation. Definition of [Enderton] p. 129.
We define
to be a binary relation rather than a connective, so
its arguments must be sets to be meaningful. This is acceptable because
we do not consider equinumerosity for proper classes. We derive the
usual definition as bren 6228. (Contributed by NM, 28-Mar-1998.)
|
           |
|
Definition | df-dom 6223* |
Define the dominance relation. Compare Definition of [Enderton] p. 145.
Typical textbook definitions are derived as brdom 6231 and domen 6232.
(Contributed by NM, 28-Mar-1998.)
|
           |
|
Definition | df-fin 6224* |
Define the (proper) class of all finite sets. Similar to Definition
10.29 of [TakeutiZaring] p. 91,
whose "Fin(a)" corresponds to
our " ". This definition is
meaningful whether or not we
accept the Axiom of Infinity ax-inf2 10101. (Contributed by NM,
22-Aug-2008.)
|
    |
|
Theorem | relen 6225 |
Equinumerosity is a relation. (Contributed by NM, 28-Mar-1998.)
|
 |
|
Theorem | reldom 6226 |
Dominance is a relation. (Contributed by NM, 28-Mar-1998.)
|
 |
|
Theorem | encv 6227 |
If two classes are equinumerous, both classes are sets. (Contributed by
AV, 21-Mar-2019.)
|
     |
|
Theorem | bren 6228* |
Equinumerosity relation. (Contributed by NM, 15-Jun-1998.)
|
        |
|
Theorem | brdomg 6229* |
Dominance relation. (Contributed by NM, 15-Jun-1998.)
|
          |
|
Theorem | brdomi 6230* |
Dominance relation. (Contributed by Mario Carneiro, 26-Apr-2015.)
|
        |
|
Theorem | brdom 6231* |
Dominance relation. (Contributed by NM, 15-Jun-1998.)
|
        |
|
Theorem | domen 6232* |
Dominance in terms of equinumerosity. Example 1 of [Enderton] p. 146.
(Contributed by NM, 15-Jun-1998.)
|
       |
|
Theorem | domeng 6233* |
Dominance in terms of equinumerosity, with the sethood requirement
expressed as an antecedent. Example 1 of [Enderton] p. 146.
(Contributed by NM, 24-Apr-2004.)
|
         |
|
Theorem | f1oen3g 6234 |
The domain and range of a one-to-one, onto function are equinumerous.
This variation of f1oeng 6237 does not require the Axiom of Replacement.
(Contributed by NM, 13-Jan-2007.) (Revised by Mario Carneiro,
10-Sep-2015.)
|
         |
|
Theorem | f1oen2g 6235 |
The domain and range of a one-to-one, onto function are equinumerous.
This variation of f1oeng 6237 does not require the Axiom of Replacement.
(Contributed by Mario Carneiro, 10-Sep-2015.)
|
         |
|
Theorem | f1dom2g 6236 |
The domain of a one-to-one function is dominated by its codomain. This
variation of f1domg 6238 does not require the Axiom of Replacement.
(Contributed by Mario Carneiro, 24-Jun-2015.)
|
         |
|
Theorem | f1oeng 6237 |
The domain and range of a one-to-one, onto function are equinumerous.
(Contributed by NM, 19-Jun-1998.)
|
         |
|
Theorem | f1domg 6238 |
The domain of a one-to-one function is dominated by its codomain.
(Contributed by NM, 4-Sep-2004.)
|
         |
|
Theorem | f1oen 6239 |
The domain and range of a one-to-one, onto function are equinumerous.
(Contributed by NM, 19-Jun-1998.)
|
       |
|
Theorem | f1dom 6240 |
The domain of a one-to-one function is dominated by its codomain.
(Contributed by NM, 19-Jun-1998.)
|
    
  |
|
Theorem | isfi 6241* |
Express " is
finite." Definition 10.29 of [TakeutiZaring] p. 91
(whose " " is a predicate instead of a class). (Contributed by
NM, 22-Aug-2008.)
|
 
  |
|
Theorem | enssdom 6242 |
Equinumerosity implies dominance. (Contributed by NM, 31-Mar-1998.)
|
 |
|
Theorem | endom 6243 |
Equinumerosity implies dominance. Theorem 15 of [Suppes] p. 94.
(Contributed by NM, 28-May-1998.)
|
   |
|
Theorem | enrefg 6244 |
Equinumerosity is reflexive. Theorem 1 of [Suppes] p. 92. (Contributed
by NM, 18-Jun-1998.) (Revised by Mario Carneiro, 26-Apr-2015.)
|
   |
|
Theorem | enref 6245 |
Equinumerosity is reflexive. Theorem 1 of [Suppes] p. 92. (Contributed
by NM, 25-Sep-2004.)
|
 |
|
Theorem | eqeng 6246 |
Equality implies equinumerosity. (Contributed by NM, 26-Oct-2003.)
|
     |
|
Theorem | domrefg 6247 |
Dominance is reflexive. (Contributed by NM, 18-Jun-1998.)
|
   |
|
Theorem | en2d 6248* |
Equinumerosity inference from an implicit one-to-one onto function.
(Contributed by NM, 27-Jul-2004.) (Revised by Mario Carneiro,
12-May-2014.)
|
     
      
 
 
      |
|
Theorem | en3d 6249* |
Equinumerosity inference from an implicit one-to-one onto function.
(Contributed by NM, 27-Jul-2004.) (Revised by Mario Carneiro,
12-May-2014.)
|
     
   
      
      |
|
Theorem | en2i 6250* |
Equinumerosity inference from an implicit one-to-one onto function.
(Contributed by NM, 4-Jan-2004.)
|

 
        |
|
Theorem | en3i 6251* |
Equinumerosity inference from an implicit one-to-one onto function.
(Contributed by NM, 19-Jul-2004.)
|

 
    
   |
|
Theorem | dom2lem 6252* |
A mapping (first hypothesis) that is one-to-one (second hypothesis)
implies its domain is dominated by its codomain. (Contributed by NM,
24-Jul-2004.)
|
 
  
 
      
       |
|
Theorem | dom2d 6253* |
A mapping (first hypothesis) that is one-to-one (second hypothesis)
implies its domain is dominated by its codomain. (Contributed by NM,
24-Jul-2004.) (Revised by Mario Carneiro, 20-May-2013.)
|
 
  
 
      
   |
|
Theorem | dom3d 6254* |
A mapping (first hypothesis) that is one-to-one (second hypothesis)
implies its domain is dominated by its codomain. (Contributed by Mario
Carneiro, 20-May-2013.)
|
 
  
 
            |
|
Theorem | dom2 6255* |
A mapping (first hypothesis) that is one-to-one (second hypothesis)
implies its domain is dominated by its codomain. and can be
read    and    , as can be inferred from their
distinct variable conditions. (Contributed by NM, 26-Oct-2003.)
|
     
     |
|
Theorem | dom3 6256* |
A mapping (first hypothesis) that is one-to-one (second hypothesis)
implies its domain is dominated by its codomain. and can be
read    and    , as can be inferred from their
distinct variable conditions. (Contributed by Mario Carneiro,
20-May-2013.)
|
     
       |
|
Theorem | idssen 6257 |
Equality implies equinumerosity. (Contributed by NM, 30-Apr-1998.)
(Revised by Mario Carneiro, 15-Nov-2014.)
|
 |
|
Theorem | ssdomg 6258 |
A set dominates its subsets. Theorem 16 of [Suppes] p. 94.
(Contributed by NM, 19-Jun-1998.) (Revised by Mario Carneiro,
24-Jun-2015.)
|
     |
|
Theorem | ener 6259 |
Equinumerosity is an equivalence relation. (Contributed by NM,
19-Mar-1998.) (Revised by Mario Carneiro, 15-Nov-2014.)
|
 |
|
Theorem | ensymb 6260 |
Symmetry of equinumerosity. Theorem 2 of [Suppes] p. 92. (Contributed by
Mario Carneiro, 26-Apr-2015.)
|
   |
|
Theorem | ensym 6261 |
Symmetry of equinumerosity. Theorem 2 of [Suppes] p. 92. (Contributed by
NM, 26-Oct-2003.) (Revised by Mario Carneiro, 26-Apr-2015.)
|
   |
|
Theorem | ensymi 6262 |
Symmetry of equinumerosity. Theorem 2 of [Suppes] p. 92. (Contributed
by NM, 25-Sep-2004.)
|
 |
|
Theorem | ensymd 6263 |
Symmetry of equinumerosity. Deduction form of ensym 6261. (Contributed
by David Moews, 1-May-2017.)
|
     |
|
Theorem | entr 6264 |
Transitivity of equinumerosity. Theorem 3 of [Suppes] p. 92.
(Contributed by NM, 9-Jun-1998.)
|
     |
|
Theorem | domtr 6265 |
Transitivity of dominance relation. Theorem 17 of [Suppes] p. 94.
(Contributed by NM, 4-Jun-1998.) (Revised by Mario Carneiro,
15-Nov-2014.)
|
     |
|
Theorem | entri 6266 |
A chained equinumerosity inference. (Contributed by NM,
25-Sep-2004.)
|
 |
|
Theorem | entr2i 6267 |
A chained equinumerosity inference. (Contributed by NM,
25-Sep-2004.)
|
 |
|
Theorem | entr3i 6268 |
A chained equinumerosity inference. (Contributed by NM,
25-Sep-2004.)
|
 |
|
Theorem | entr4i 6269 |
A chained equinumerosity inference. (Contributed by NM,
25-Sep-2004.)
|
 |
|
Theorem | endomtr 6270 |
Transitivity of equinumerosity and dominance. (Contributed by NM,
7-Jun-1998.)
|
     |
|
Theorem | domentr 6271 |
Transitivity of dominance and equinumerosity. (Contributed by NM,
7-Jun-1998.)
|
     |
|
Theorem | f1imaeng 6272 |
A one-to-one function's image under a subset of its domain is equinumerous
to the subset. (Contributed by Mario Carneiro, 15-May-2015.)
|
     
    
  |
|
Theorem | f1imaen2g 6273 |
A one-to-one function's image under a subset of its domain is equinumerous
to the subset. (This version of f1imaen 6274 does not need ax-setind 4262.)
(Contributed by Mario Carneiro, 16-Nov-2014.) (Revised by Mario Carneiro,
25-Jun-2015.)
|
      
   
      |
|
Theorem | f1imaen 6274 |
A one-to-one function's image under a subset of its domain is
equinumerous to the subset. (Contributed by NM, 30-Sep-2004.)
|
             |
|
Theorem | en0 6275 |
The empty set is equinumerous only to itself. Exercise 1 of
[TakeutiZaring] p. 88.
(Contributed by NM, 27-May-1998.)
|

  |
|
Theorem | ensn1 6276 |
A singleton is equinumerous to ordinal one. (Contributed by NM,
4-Nov-2002.)
|
   |
|
Theorem | ensn1g 6277 |
A singleton is equinumerous to ordinal one. (Contributed by NM,
23-Apr-2004.)
|
     |
|
Theorem | enpr1g 6278 |
   has only
one element. (Contributed by FL, 15-Feb-2010.)
|
      |
|
Theorem | en1 6279* |
A set is equinumerous to ordinal one iff it is a singleton.
(Contributed by NM, 25-Jul-2004.)
|
 
    |
|
Theorem | en1bg 6280 |
A set is equinumerous to ordinal one iff it is a singleton.
(Contributed by Jim Kingdon, 13-Apr-2020.)
|
        |
|
Theorem | reuen1 6281* |
Two ways to express "exactly one". (Contributed by Stefan O'Rear,
28-Oct-2014.)
|
 
    |
|
Theorem | euen1 6282 |
Two ways to express "exactly one". (Contributed by Stefan O'Rear,
28-Oct-2014.)
|
   
   |
|
Theorem | euen1b 6283* |
Two ways to express " has a unique element". (Contributed by
Mario Carneiro, 9-Apr-2015.)
|
 
  |
|
Theorem | en1uniel 6284 |
A singleton contains its sole element. (Contributed by Stefan O'Rear,
16-Aug-2015.)
|
    |
|
Theorem | 2dom 6285* |
A set that dominates ordinal 2 has at least 2 different members.
(Contributed by NM, 25-Jul-2004.)
|
  
  |
|
Theorem | fundmen 6286 |
A function is equinumerous to its domain. Exercise 4 of [Suppes] p. 98.
(Contributed by NM, 28-Jul-2004.) (Revised by Mario Carneiro,
15-Nov-2014.)
|
   |
|
Theorem | fundmeng 6287 |
A function is equinumerous to its domain. Exercise 4 of [Suppes] p. 98.
(Contributed by NM, 17-Sep-2013.)
|
 
   |
|
Theorem | cnven 6288 |
A relational set is equinumerous to its converse. (Contributed by Mario
Carneiro, 28-Dec-2014.)
|
      |
|
Theorem | fndmeng 6289 |
A function is equinumerate to its domain. (Contributed by Paul Chapman,
22-Jun-2011.)
|
     |
|
Theorem | en2sn 6290 |
Two singletons are equinumerous. (Contributed by NM, 9-Nov-2003.)
|
         |
|
Theorem | snfig 6291 |
A singleton is finite. (Contributed by Jim Kingdon, 13-Apr-2020.)
|
     |
|
Theorem | fiprc 6292 |
The class of finite sets is a proper class. (Contributed by Jeff
Hankins, 3-Oct-2008.)
|
 |
|
Theorem | unen 6293 |
Equinumerosity of union of disjoint sets. Theorem 4 of [Suppes] p. 92.
(Contributed by NM, 11-Jun-1998.) (Revised by Mario Carneiro,
26-Apr-2015.)
|
      
      
   |
|
Theorem | enm 6294* |
A set equinumerous to an inhabited set is inhabited. (Contributed by
Jim Kingdon, 19-May-2020.)
|
    
  |
|
Theorem | xpsnen 6295 |
A set is equinumerous to its Cartesian product with a singleton.
Proposition 4.22(c) of [Mendelson] p.
254. (Contributed by NM,
4-Jan-2004.) (Revised by Mario Carneiro, 15-Nov-2014.)
|
     |
|
Theorem | xpsneng 6296 |
A set is equinumerous to its Cartesian product with a singleton.
Proposition 4.22(c) of [Mendelson] p.
254. (Contributed by NM,
22-Oct-2004.)
|
         |
|
Theorem | xp1en 6297 |
One times a cardinal number. (Contributed by NM, 27-Sep-2004.) (Revised
by Mario Carneiro, 29-Apr-2015.)
|
     |
|
Theorem | endisj 6298* |
Any two sets are equinumerous to disjoint sets. Exercise 4.39 of
[Mendelson] p. 255. (Contributed by
NM, 16-Apr-2004.)
|
        
  |
|
Theorem | xpcomf1o 6299* |
The canonical bijection from   to   .
(Contributed by Mario Carneiro, 23-Apr-2014.)
|
  
              |
|
Theorem | xpcomco 6300* |
Composition with the bijection of xpcomf1o 6299 swaps the arguments to a
mapping. (Contributed by Mario Carneiro, 30-May-2015.)
|
  
      
  
    |