Theorem List for Intuitionistic Logic Explorer - 6501-6600 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | ixpm 6501* |
If an infinite Cartesian product of a family    is inhabited,
every    is inhabited. (Contributed by Mario Carneiro,
22-Jun-2016.) (Revised by Jim Kingdon, 16-Feb-2023.)
|
    
  |
|
Theorem | ixp0 6502 |
The infinite Cartesian product of a family    with an empty
member is empty. (Contributed by NM, 1-Oct-2006.) (Revised by Jim
Kingdon, 16-Feb-2023.)
|
     |
|
Theorem | ixpssmap 6503* |
An infinite Cartesian product is a subset of set exponentiation. Remark
in [Enderton] p. 54. (Contributed by
NM, 28-Sep-2006.)
|
     |
|
Theorem | resixp 6504* |
Restriction of an element of an infinite Cartesian product.
(Contributed by FL, 7-Nov-2011.) (Proof shortened by Mario Carneiro,
31-May-2014.)
|
  
      |
|
Theorem | mptelixpg 6505* |
Condition for an explicit member of an indexed product. (Contributed by
Stefan O'Rear, 4-Jan-2015.)
|
    

   |
|
Theorem | elixpsn 6506* |
Membership in a class of singleton functions. (Contributed by Stefan
O'Rear, 24-Jan-2015.)
|
  
  

        |
|
Theorem | ixpsnf1o 6507* |
A bijection between a class and single-point functions to it.
(Contributed by Stefan O'Rear, 24-Jan-2015.)
|
   
    
          |
|
Theorem | mapsnf1o 6508* |
A bijection between a set and single-point functions to it.
(Contributed by Stefan O'Rear, 24-Jan-2015.)
|
   
                 |
|
2.6.27 Equinumerosity
|
|
Syntax | cen 6509 |
Extend class definition to include the equinumerosity relation
("approximately equals" symbol)
|
 |
|
Syntax | cdom 6510 |
Extend class definition to include the dominance relation (curly
less-than-or-equal)
|
 |
|
Syntax | cfn 6511 |
Extend class definition to include the class of all finite sets.
|
 |
|
Definition | df-en 6512* |
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 6518. (Contributed by NM, 28-Mar-1998.)
|
           |
|
Definition | df-dom 6513* |
Define the dominance relation. Compare Definition of [Enderton] p. 145.
Typical textbook definitions are derived as brdom 6521 and domen 6522.
(Contributed by NM, 28-Mar-1998.)
|
           |
|
Definition | df-fin 6514* |
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 12137. (Contributed by NM,
22-Aug-2008.)
|
    |
|
Theorem | relen 6515 |
Equinumerosity is a relation. (Contributed by NM, 28-Mar-1998.)
|
 |
|
Theorem | reldom 6516 |
Dominance is a relation. (Contributed by NM, 28-Mar-1998.)
|
 |
|
Theorem | encv 6517 |
If two classes are equinumerous, both classes are sets. (Contributed by
AV, 21-Mar-2019.)
|
     |
|
Theorem | bren 6518* |
Equinumerosity relation. (Contributed by NM, 15-Jun-1998.)
|
        |
|
Theorem | brdomg 6519* |
Dominance relation. (Contributed by NM, 15-Jun-1998.)
|
          |
|
Theorem | brdomi 6520* |
Dominance relation. (Contributed by Mario Carneiro, 26-Apr-2015.)
|
        |
|
Theorem | brdom 6521* |
Dominance relation. (Contributed by NM, 15-Jun-1998.)
|
        |
|
Theorem | domen 6522* |
Dominance in terms of equinumerosity. Example 1 of [Enderton] p. 146.
(Contributed by NM, 15-Jun-1998.)
|
       |
|
Theorem | domeng 6523* |
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 | ctex 6524 |
A countable set is a set. (Contributed by Thierry Arnoux,
29-Dec-2016.)
|
   |
|
Theorem | f1oen3g 6525 |
The domain and range of a one-to-one, onto function are equinumerous.
This variation of f1oeng 6528 does not require the Axiom of Replacement.
(Contributed by NM, 13-Jan-2007.) (Revised by Mario Carneiro,
10-Sep-2015.)
|
         |
|
Theorem | f1oen2g 6526 |
The domain and range of a one-to-one, onto function are equinumerous.
This variation of f1oeng 6528 does not require the Axiom of Replacement.
(Contributed by Mario Carneiro, 10-Sep-2015.)
|
         |
|
Theorem | f1dom2g 6527 |
The domain of a one-to-one function is dominated by its codomain. This
variation of f1domg 6529 does not require the Axiom of Replacement.
(Contributed by Mario Carneiro, 24-Jun-2015.)
|
         |
|
Theorem | f1oeng 6528 |
The domain and range of a one-to-one, onto function are equinumerous.
(Contributed by NM, 19-Jun-1998.)
|
         |
|
Theorem | f1domg 6529 |
The domain of a one-to-one function is dominated by its codomain.
(Contributed by NM, 4-Sep-2004.)
|
         |
|
Theorem | f1oen 6530 |
The domain and range of a one-to-one, onto function are equinumerous.
(Contributed by NM, 19-Jun-1998.)
|
       |
|
Theorem | f1dom 6531 |
The domain of a one-to-one function is dominated by its codomain.
(Contributed by NM, 19-Jun-1998.)
|
    
  |
|
Theorem | isfi 6532* |
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 6533 |
Equinumerosity implies dominance. (Contributed by NM, 31-Mar-1998.)
|
 |
|
Theorem | endom 6534 |
Equinumerosity implies dominance. Theorem 15 of [Suppes] p. 94.
(Contributed by NM, 28-May-1998.)
|
   |
|
Theorem | enrefg 6535 |
Equinumerosity is reflexive. Theorem 1 of [Suppes] p. 92. (Contributed
by NM, 18-Jun-1998.) (Revised by Mario Carneiro, 26-Apr-2015.)
|
   |
|
Theorem | enref 6536 |
Equinumerosity is reflexive. Theorem 1 of [Suppes] p. 92. (Contributed
by NM, 25-Sep-2004.)
|
 |
|
Theorem | eqeng 6537 |
Equality implies equinumerosity. (Contributed by NM, 26-Oct-2003.)
|
     |
|
Theorem | domrefg 6538 |
Dominance is reflexive. (Contributed by NM, 18-Jun-1998.)
|
   |
|
Theorem | en2d 6539* |
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 6540* |
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 6541* |
Equinumerosity inference from an implicit one-to-one onto function.
(Contributed by NM, 4-Jan-2004.)
|

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

 
    
   |
|
Theorem | dom2lem 6543* |
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 6544* |
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 6545* |
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 6546* |
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 6547* |
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 6548 |
Equality implies equinumerosity. (Contributed by NM, 30-Apr-1998.)
(Revised by Mario Carneiro, 15-Nov-2014.)
|
 |
|
Theorem | ssdomg 6549 |
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 6550 |
Equinumerosity is an equivalence relation. (Contributed by NM,
19-Mar-1998.) (Revised by Mario Carneiro, 15-Nov-2014.)
|
 |
|
Theorem | ensymb 6551 |
Symmetry of equinumerosity. Theorem 2 of [Suppes] p. 92. (Contributed by
Mario Carneiro, 26-Apr-2015.)
|
   |
|
Theorem | ensym 6552 |
Symmetry of equinumerosity. Theorem 2 of [Suppes] p. 92. (Contributed by
NM, 26-Oct-2003.) (Revised by Mario Carneiro, 26-Apr-2015.)
|
   |
|
Theorem | ensymi 6553 |
Symmetry of equinumerosity. Theorem 2 of [Suppes] p. 92. (Contributed
by NM, 25-Sep-2004.)
|
 |
|
Theorem | ensymd 6554 |
Symmetry of equinumerosity. Deduction form of ensym 6552. (Contributed
by David Moews, 1-May-2017.)
|
     |
|
Theorem | entr 6555 |
Transitivity of equinumerosity. Theorem 3 of [Suppes] p. 92.
(Contributed by NM, 9-Jun-1998.)
|
     |
|
Theorem | domtr 6556 |
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 6557 |
A chained equinumerosity inference. (Contributed by NM,
25-Sep-2004.)
|
 |
|
Theorem | entr2i 6558 |
A chained equinumerosity inference. (Contributed by NM,
25-Sep-2004.)
|
 |
|
Theorem | entr3i 6559 |
A chained equinumerosity inference. (Contributed by NM,
25-Sep-2004.)
|
 |
|
Theorem | entr4i 6560 |
A chained equinumerosity inference. (Contributed by NM,
25-Sep-2004.)
|
 |
|
Theorem | endomtr 6561 |
Transitivity of equinumerosity and dominance. (Contributed by NM,
7-Jun-1998.)
|
     |
|
Theorem | domentr 6562 |
Transitivity of dominance and equinumerosity. (Contributed by NM,
7-Jun-1998.)
|
     |
|
Theorem | f1imaeng 6563 |
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 6564 |
A one-to-one function's image under a subset of its domain is equinumerous
to the subset. (This version of f1imaen 6565 does not need ax-setind 4366.)
(Contributed by Mario Carneiro, 16-Nov-2014.) (Revised by Mario Carneiro,
25-Jun-2015.)
|
      
   
      |
|
Theorem | f1imaen 6565 |
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 6566 |
The empty set is equinumerous only to itself. Exercise 1 of
[TakeutiZaring] p. 88.
(Contributed by NM, 27-May-1998.)
|

  |
|
Theorem | ensn1 6567 |
A singleton is equinumerous to ordinal one. (Contributed by NM,
4-Nov-2002.)
|
   |
|
Theorem | ensn1g 6568 |
A singleton is equinumerous to ordinal one. (Contributed by NM,
23-Apr-2004.)
|
     |
|
Theorem | enpr1g 6569 |
   has only
one element. (Contributed by FL, 15-Feb-2010.)
|
      |
|
Theorem | en1 6570* |
A set is equinumerous to ordinal one iff it is a singleton.
(Contributed by NM, 25-Jul-2004.)
|
 
    |
|
Theorem | en1bg 6571 |
A set is equinumerous to ordinal one iff it is a singleton.
(Contributed by Jim Kingdon, 13-Apr-2020.)
|
        |
|
Theorem | reuen1 6572* |
Two ways to express "exactly one". (Contributed by Stefan O'Rear,
28-Oct-2014.)
|
 
    |
|
Theorem | euen1 6573 |
Two ways to express "exactly one". (Contributed by Stefan O'Rear,
28-Oct-2014.)
|
   
   |
|
Theorem | euen1b 6574* |
Two ways to express " has a unique element". (Contributed by
Mario Carneiro, 9-Apr-2015.)
|
 
  |
|
Theorem | en1uniel 6575 |
A singleton contains its sole element. (Contributed by Stefan O'Rear,
16-Aug-2015.)
|
    |
|
Theorem | 2dom 6576* |
A set that dominates ordinal 2 has at least 2 different members.
(Contributed by NM, 25-Jul-2004.)
|
  
  |
|
Theorem | fundmen 6577 |
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 6578 |
A function is equinumerous to its domain. Exercise 4 of [Suppes] p. 98.
(Contributed by NM, 17-Sep-2013.)
|
 
   |
|
Theorem | cnven 6579 |
A relational set is equinumerous to its converse. (Contributed by Mario
Carneiro, 28-Dec-2014.)
|
      |
|
Theorem | cnvct 6580 |
If a set is countable, so is its converse. (Contributed by Thierry
Arnoux, 29-Dec-2016.)
|
    |
|
Theorem | fndmeng 6581 |
A function is equinumerate to its domain. (Contributed by Paul Chapman,
22-Jun-2011.)
|
     |
|
Theorem | mapsnen 6582 |
Set exponentiation to a singleton exponent is equinumerous to its base.
Exercise 4.43 of [Mendelson] p. 255.
(Contributed by NM, 17-Dec-2003.)
(Revised by Mario Carneiro, 15-Nov-2014.)
|
     |
|
Theorem | map1 6583 |
Set exponentiation: ordinal 1 to any set is equinumerous to ordinal 1.
Exercise 4.42(b) of [Mendelson] p.
255. (Contributed by NM,
17-Dec-2003.)
|
     |
|
Theorem | en2sn 6584 |
Two singletons are equinumerous. (Contributed by NM, 9-Nov-2003.)
|
         |
|
Theorem | snfig 6585 |
A singleton is finite. For the proper class case, see snprc 3511.
(Contributed by Jim Kingdon, 13-Apr-2020.)
|
     |
|
Theorem | fiprc 6586 |
The class of finite sets is a proper class. (Contributed by Jeff
Hankins, 3-Oct-2008.)
|
 |
|
Theorem | unen 6587 |
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 | ssct 6588 |
Any subset of a countable set is countable. (Contributed by Thierry
Arnoux, 31-Jan-2017.)
|
     |
|
Theorem | 1domsn 6589 |
A singleton (whether of a set or a proper class) is dominated by one.
(Contributed by Jim Kingdon, 1-Mar-2022.)
|
   |
|
Theorem | enm 6590* |
A set equinumerous to an inhabited set is inhabited. (Contributed by
Jim Kingdon, 19-May-2020.)
|
    
  |
|
Theorem | xpsnen 6591 |
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 6592 |
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 6593 |
One times a cardinal number. (Contributed by NM, 27-Sep-2004.) (Revised
by Mario Carneiro, 29-Apr-2015.)
|
     |
|
Theorem | endisj 6594* |
Any two sets are equinumerous to disjoint sets. Exercise 4.39 of
[Mendelson] p. 255. (Contributed by
NM, 16-Apr-2004.)
|
        
  |
|
Theorem | xpcomf1o 6595* |
The canonical bijection from   to   .
(Contributed by Mario Carneiro, 23-Apr-2014.)
|
  
              |
|
Theorem | xpcomco 6596* |
Composition with the bijection of xpcomf1o 6595 swaps the arguments to a
mapping. (Contributed by Mario Carneiro, 30-May-2015.)
|
  
      
  
    |
|
Theorem | xpcomen 6597 |
Commutative law for equinumerosity of Cartesian product. Proposition
4.22(d) of [Mendelson] p. 254.
(Contributed by NM, 5-Jan-2004.)
(Revised by Mario Carneiro, 15-Nov-2014.)
|
     |
|
Theorem | xpcomeng 6598 |
Commutative law for equinumerosity of Cartesian product. Proposition
4.22(d) of [Mendelson] p. 254.
(Contributed by NM, 27-Mar-2006.)
|
    
    |
|
Theorem | xpsnen2g 6599 |
A set is equinumerous to its Cartesian product with a singleton on the
left. (Contributed by Stefan O'Rear, 21-Nov-2014.)
|
         |
|
Theorem | xpassen 6600 |
Associative law for equinumerosity of Cartesian product. Proposition
4.22(e) of [Mendelson] p. 254.
(Contributed by NM, 22-Jan-2004.)
(Revised by Mario Carneiro, 15-Nov-2014.)
|
    
    |