Type | Label | Description |
Statement |
|
Theorem | nnmass 6501 |
Multiplication of natural numbers is associative. Theorem 4K(4) of
[Enderton] p. 81. (Contributed by NM,
20-Sep-1995.) (Revised by Mario
Carneiro, 15-Nov-2014.)
|
     
  
    |
|
Theorem | nnmsucr 6502 |
Multiplication with successor. Exercise 16 of [Enderton] p. 82.
(Contributed by NM, 21-Sep-1995.) (Proof shortened by Andrew Salmon,
22-Oct-2011.)
|
           |
|
Theorem | nnmcom 6503 |
Multiplication of natural numbers is commutative. Theorem 4K(5) of
[Enderton] p. 81. (Contributed by NM,
21-Sep-1995.) (Proof shortened
by Andrew Salmon, 22-Oct-2011.)
|
    
    |
|
Theorem | nndir 6504 |
Distributive law for natural numbers (right-distributivity). (Contributed
by Jim Kingdon, 3-Dec-2019.)
|
     
    
    |
|
Theorem | nnsucelsuc 6505 |
Membership is inherited by successors. The reverse direction holds for
all ordinals, as seen at onsucelsucr 4519, but the forward direction, for
all ordinals, implies excluded middle as seen as onsucelsucexmid 4541.
(Contributed by Jim Kingdon, 25-Aug-2019.)
|
     |
|
Theorem | nnsucsssuc 6506 |
Membership is inherited by successors. The reverse direction holds for
all ordinals, as seen at onsucsssucr 4520, but the forward direction, for
all ordinals, implies excluded middle as seen as onsucsssucexmid 4538.
(Contributed by Jim Kingdon, 25-Aug-2019.)
|
   
   |
|
Theorem | nntri3or 6507 |
Trichotomy for natural numbers. (Contributed by Jim Kingdon,
25-Aug-2019.)
|
       |
|
Theorem | nntri2 6508 |
A trichotomy law for natural numbers. (Contributed by Jim Kingdon,
28-Aug-2019.)
|
         |
|
Theorem | nnsucuniel 6509 |
Given an element of
the union of a natural number ,
is an element of itself. The reverse
direction holds
for all ordinals (sucunielr 4521). The forward direction for all
ordinals implies excluded middle (ordsucunielexmid 4542). (Contributed
by Jim Kingdon, 13-Mar-2022.)
|
  
   |
|
Theorem | nntri1 6510 |
A trichotomy law for natural numbers. (Contributed by Jim Kingdon,
28-Aug-2019.)
|
       |
|
Theorem | nntri3 6511 |
A trichotomy law for natural numbers. (Contributed by Jim Kingdon,
15-May-2020.)
|
         |
|
Theorem | nntri2or2 6512 |
A trichotomy law for natural numbers. (Contributed by Jim Kingdon,
15-Sep-2021.)
|
       |
|
Theorem | nndceq 6513 |
Equality of natural numbers is decidable. Theorem 7.2.6 of [HoTT], p.
(varies). For the specific case where is zero, see nndceq0 4629.
(Contributed by Jim Kingdon, 31-Aug-2019.)
|
   DECID
  |
|
Theorem | nndcel 6514 |
Set membership between two natural numbers is decidable. (Contributed by
Jim Kingdon, 6-Sep-2019.)
|
   DECID
  |
|
Theorem | nnsseleq 6515 |
For natural numbers, inclusion is equivalent to membership or equality.
(Contributed by Jim Kingdon, 16-Sep-2021.)
|
         |
|
Theorem | nnsssuc 6516 |
A natural number is a subset of another natural number if and only if it
belongs to its successor. (Contributed by Jim Kingdon, 22-Jul-2023.)
|
       |
|
Theorem | nntr2 6517 |
Transitive law for natural numbers. (Contributed by Jim Kingdon,
22-Jul-2023.)
|
         |
|
Theorem | dcdifsnid 6518* |
If we remove a single element from a set with decidable equality then
put it back in, we end up with the original set. This strengthens
difsnss 3750 from subset to equality but the proof relies
on equality being
decidable. (Contributed by Jim Kingdon, 17-Jun-2022.)
|
    DECID
           |
|
Theorem | fnsnsplitdc 6519* |
Split a function into a single point and all the rest. (Contributed by
Stefan O'Rear, 27-Feb-2015.) (Revised by Jim Kingdon, 29-Jan-2023.)
|
    DECID                     |
|
Theorem | funresdfunsndc 6520* |
Restricting a function to a domain without one element of the domain of
the function, and adding a pair of this element and the function value
of the element results in the function itself, where equality is
decidable. (Contributed by AV, 2-Dec-2018.) (Revised by Jim Kingdon,
30-Jan-2023.)
|
     DECID
                    |
|
Theorem | nndifsnid 6521 |
If we remove a single element from a natural number then put it back in,
we end up with the original natural number. This strengthens difsnss 3750
from subset to equality but the proof relies on equality being
decidable. (Contributed by Jim Kingdon, 31-Aug-2021.)
|
          
  |
|
Theorem | nnaordi 6522 |
Ordering property of addition. Proposition 8.4 of [TakeutiZaring]
p. 58, limited to natural numbers. (Contributed by NM, 3-Feb-1996.)
(Revised by Mario Carneiro, 15-Nov-2014.)
|
     
     |
|
Theorem | nnaord 6523 |
Ordering property of addition. Proposition 8.4 of [TakeutiZaring] p. 58,
limited to natural numbers, and its converse. (Contributed by NM,
7-Mar-1996.) (Revised by Mario Carneiro, 15-Nov-2014.)
|
           |
|
Theorem | nnaordr 6524 |
Ordering property of addition of natural numbers. (Contributed by NM,
9-Nov-2002.)
|
           |
|
Theorem | nnaword 6525 |
Weak ordering property of addition. (Contributed by NM, 17-Sep-1995.)
(Revised by Mario Carneiro, 15-Nov-2014.)
|
           |
|
Theorem | nnacan 6526 |
Cancellation law for addition of natural numbers. (Contributed by NM,
27-Oct-1995.) (Revised by Mario Carneiro, 15-Nov-2014.)
|
     
 
   |
|
Theorem | nnaword1 6527 |
Weak ordering property of addition. (Contributed by NM, 9-Nov-2002.)
(Revised by Mario Carneiro, 15-Nov-2014.)
|
       |
|
Theorem | nnaword2 6528 |
Weak ordering property of addition. (Contributed by NM, 9-Nov-2002.)
|
       |
|
Theorem | nnawordi 6529 |
Adding to both sides of an inequality in . (Contributed by Scott
Fenton, 16-Apr-2012.) (Revised by Mario Carneiro, 12-May-2012.)
|
           |
|
Theorem | nnmordi 6530 |
Ordering property of multiplication. Half of Proposition 8.19 of
[TakeutiZaring] p. 63, limited to
natural numbers. (Contributed by NM,
18-Sep-1995.) (Revised by Mario Carneiro, 15-Nov-2014.)
|
       
     |
|
Theorem | nnmord 6531 |
Ordering property of multiplication. Proposition 8.19 of [TakeutiZaring]
p. 63, limited to natural numbers. (Contributed by NM, 22-Jan-1996.)
(Revised by Mario Carneiro, 15-Nov-2014.)
|
       
     |
|
Theorem | nnmword 6532 |
Weak ordering property of ordinal multiplication. (Contributed by Mario
Carneiro, 17-Nov-2014.)
|
             |
|
Theorem | nnmcan 6533 |
Cancellation law for multiplication of natural numbers. (Contributed by
NM, 26-Oct-1995.) (Revised by Mario Carneiro, 15-Nov-2014.)
|
             |
|
Theorem | 1onn 6534 |
One is a natural number. (Contributed by NM, 29-Oct-1995.)
|
 |
|
Theorem | 2onn 6535 |
The ordinal 2 is a natural number. (Contributed by NM, 28-Sep-2004.)
|
 |
|
Theorem | 3onn 6536 |
The ordinal 3 is a natural number. (Contributed by Mario Carneiro,
5-Jan-2016.)
|
 |
|
Theorem | 4onn 6537 |
The ordinal 4 is a natural number. (Contributed by Mario Carneiro,
5-Jan-2016.)
|
 |
|
Theorem | 2ssom 6538 |
The ordinal 2 is included in the set of natural number ordinals.
(Contributed by BJ, 5-Aug-2024.)
|
 |
|
Theorem | nnm1 6539 |
Multiply an element of by .
(Contributed by Mario
Carneiro, 17-Nov-2014.)
|
  
  |
|
Theorem | nnm2 6540 |
Multiply an element of by .
(Contributed by Scott Fenton,
18-Apr-2012.) (Revised by Mario Carneiro, 17-Nov-2014.)
|
  
    |
|
Theorem | nn2m 6541 |
Multiply an element of by .
(Contributed by Scott Fenton,
16-Apr-2012.) (Revised by Mario Carneiro, 17-Nov-2014.)
|
  
    |
|
Theorem | nnaordex 6542* |
Equivalence for ordering. Compare Exercise 23 of [Enderton] p. 88.
(Contributed by NM, 5-Dec-1995.) (Revised by Mario Carneiro,
15-Nov-2014.)
|
      

    |
|
Theorem | nnawordex 6543* |
Equivalence for weak ordering of natural numbers. (Contributed by NM,
8-Nov-2002.) (Revised by Mario Carneiro, 15-Nov-2014.)
|
     

   |
|
Theorem | nnm00 6544 |
The product of two natural numbers is zero iff at least one of them is
zero. (Contributed by Jim Kingdon, 11-Nov-2004.)
|
           |
|
2.6.25 Equivalence relations and
classes
|
|
Syntax | wer 6545 |
Extend the definition of a wff to include the equivalence predicate.
|
 |
|
Syntax | cec 6546 |
Extend the definition of a class to include equivalence class.
|
  ![] ]](rbrack.gif)  |
|
Syntax | cqs 6547 |
Extend the definition of a class to include quotient set.
|
     |
|
Definition | df-er 6548 |
Define the equivalence relation predicate. Our notation is not standard.
A formal notation doesn't seem to exist in the literature; instead only
informal English tends to be used. The present definition, although
somewhat cryptic, nicely avoids dummy variables. In dfer2 6549 we derive a
more typical definition. We show that an equivalence relation is
reflexive, symmetric, and transitive in erref 6568, ersymb 6562, and ertr 6563.
(Contributed by NM, 4-Jun-1995.) (Revised by Mario Carneiro,
2-Nov-2015.)
|
   
      |
|
Theorem | dfer2 6549* |
Alternate definition of equivalence predicate. (Contributed by NM,
3-Jan-1997.) (Revised by Mario Carneiro, 12-Aug-2015.)
|
           
  
              |
|
Definition | df-ec 6550 |
Define the -coset of
. Exercise 35 of [Enderton] p. 61. This
is called the equivalence class of modulo when is an
equivalence relation (i.e. when ; see dfer2 6549). In this case,
is a
representative (member) of the equivalence class   ![] ]](rbrack.gif) ,
which contains all sets that are equivalent to . Definition of
[Enderton] p. 57 uses the notation   (subscript) , although
we simply follow the brackets by since we don't have subscripted
expressions. For an alternate definition, see dfec2 6551. (Contributed by
NM, 23-Jul-1995.)
|
  ![] ]](rbrack.gif)        |
|
Theorem | dfec2 6551* |
Alternate definition of -coset of .
Definition 34 of
[Suppes] p. 81. (Contributed by NM,
3-Jan-1997.) (Proof shortened by
Mario Carneiro, 9-Jul-2014.)
|
   ![] ]](rbrack.gif)       |
|
Theorem | ecexg 6552 |
An equivalence class modulo a set is a set. (Contributed by NM,
24-Jul-1995.)
|
   ![] ]](rbrack.gif)   |
|
Theorem | ecexr 6553 |
An inhabited equivalence class implies the representative is a set.
(Contributed by Mario Carneiro, 9-Jul-2014.)
|
   ![] ]](rbrack.gif)   |
|
Definition | df-qs 6554* |
Define quotient set.
is usually an equivalence relation.
Definition of [Enderton] p. 58.
(Contributed by NM, 23-Jul-1995.)
|
   
 
  ![] ]](rbrack.gif)   |
|
Theorem | ereq1 6555 |
Equality theorem for equivalence predicate. (Contributed by NM,
4-Jun-1995.) (Revised by Mario Carneiro, 12-Aug-2015.)
|
     |
|
Theorem | ereq2 6556 |
Equality theorem for equivalence predicate. (Contributed by Mario
Carneiro, 12-Aug-2015.)
|
     |
|
Theorem | errel 6557 |
An equivalence relation is a relation. (Contributed by Mario Carneiro,
12-Aug-2015.)
|
   |
|
Theorem | erdm 6558 |
The domain of an equivalence relation. (Contributed by Mario Carneiro,
12-Aug-2015.)
|
   |
|
Theorem | ercl 6559 |
Elementhood in the field of an equivalence relation. (Contributed by
Mario Carneiro, 12-Aug-2015.)
|
         |
|
Theorem | ersym 6560 |
An equivalence relation is symmetric. (Contributed by NM, 4-Jun-1995.)
(Revised by Mario Carneiro, 12-Aug-2015.)
|
           |
|
Theorem | ercl2 6561 |
Elementhood in the field of an equivalence relation. (Contributed by
Mario Carneiro, 12-Aug-2015.)
|
         |
|
Theorem | ersymb 6562 |
An equivalence relation is symmetric. (Contributed by NM, 30-Jul-1995.)
(Revised by Mario Carneiro, 12-Aug-2015.)
|
           |
|
Theorem | ertr 6563 |
An equivalence relation is transitive. (Contributed by NM, 4-Jun-1995.)
(Revised by Mario Carneiro, 12-Aug-2015.)
|
               |
|
Theorem | ertrd 6564 |
A transitivity relation for equivalences. (Contributed by Mario
Carneiro, 9-Jul-2014.)
|
               |
|
Theorem | ertr2d 6565 |
A transitivity relation for equivalences. (Contributed by Mario
Carneiro, 9-Jul-2014.)
|
               |
|
Theorem | ertr3d 6566 |
A transitivity relation for equivalences. (Contributed by Mario
Carneiro, 9-Jul-2014.)
|
               |
|
Theorem | ertr4d 6567 |
A transitivity relation for equivalences. (Contributed by Mario
Carneiro, 9-Jul-2014.)
|
               |
|
Theorem | erref 6568 |
An equivalence relation is reflexive on its field. Compare Theorem 3M
of [Enderton] p. 56. (Contributed by
Mario Carneiro, 6-May-2013.)
(Revised by Mario Carneiro, 12-Aug-2015.)
|
         |
|
Theorem | ercnv 6569 |
The converse of an equivalence relation is itself. (Contributed by
Mario Carneiro, 12-Aug-2015.)
|
 
  |
|
Theorem | errn 6570 |
The range and domain of an equivalence relation are equal. (Contributed
by Rodolfo Medina, 11-Oct-2010.) (Revised by Mario Carneiro,
12-Aug-2015.)
|
   |
|
Theorem | erssxp 6571 |
An equivalence relation is a subset of the cartesian product of the field.
(Contributed by Mario Carneiro, 12-Aug-2015.)
|

    |
|
Theorem | erex 6572 |
An equivalence relation is a set if its domain is a set. (Contributed by
Rodolfo Medina, 15-Oct-2010.) (Proof shortened by Mario Carneiro,
12-Aug-2015.)
|
     |
|
Theorem | erexb 6573 |
An equivalence relation is a set if and only if its domain is a set.
(Contributed by Rodolfo Medina, 15-Oct-2010.) (Revised by Mario Carneiro,
12-Aug-2015.)
|
     |
|
Theorem | iserd 6574* |
A reflexive, symmetric, transitive relation is an equivalence relation
on its domain. (Contributed by Mario Carneiro, 9-Jul-2014.) (Revised
by Mario Carneiro, 12-Aug-2015.)
|
           
          
        |
|
Theorem | brdifun 6575 |
Evaluate the incomparability relation. (Contributed by Mario Carneiro,
9-Jul-2014.)
|
               |
|
Theorem | swoer 6576* |
Incomparability under a strict weak partial order is an equivalence
relation. (Contributed by Mario Carneiro, 9-Jul-2014.) (Revised by
Mario Carneiro, 12-Aug-2015.)
|
      
 

   
   

      |
|
Theorem | swoord1 6577* |
The incomparability equivalence relation is compatible with the
original order. (Contributed by Mario Carneiro, 31-Dec-2014.)
|
      
 

   
   

            
   |
|
Theorem | swoord2 6578* |
The incomparability equivalence relation is compatible with the
original order. (Contributed by Mario Carneiro, 31-Dec-2014.)
|
      
 

   
   

            
   |
|
Theorem | eqerlem 6579* |
Lemma for eqer 6580. (Contributed by NM, 17-Mar-2008.) (Proof
shortened
by Mario Carneiro, 6-Dec-2016.)
|
 
        
 ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)   |
|
Theorem | eqer 6580* |
Equivalence relation involving equality of dependent classes   
and    . (Contributed by NM, 17-Mar-2008.) (Revised by Mario
Carneiro, 12-Aug-2015.)
|
 
      |
|
Theorem | ider 6581 |
The identity relation is an equivalence relation. (Contributed by NM,
10-May-1998.) (Proof shortened by Andrew Salmon, 22-Oct-2011.) (Proof
shortened by Mario Carneiro, 9-Jul-2014.)
|
 |
|
Theorem | 0er 6582 |
The empty set is an equivalence relation on the empty set. (Contributed
by Mario Carneiro, 5-Sep-2015.)
|
 |
|
Theorem | eceq1 6583 |
Equality theorem for equivalence class. (Contributed by NM,
23-Jul-1995.)
|
   ![] ]](rbrack.gif)   ![] ]](rbrack.gif)   |
|
Theorem | eceq1d 6584 |
Equality theorem for equivalence class (deduction form). (Contributed
by Jim Kingdon, 31-Dec-2019.)
|
     ![] ]](rbrack.gif)
  ![] ]](rbrack.gif)   |
|
Theorem | eceq2 6585 |
Equality theorem for equivalence class. (Contributed by NM,
23-Jul-1995.)
|
   ![] ]](rbrack.gif)   ![] ]](rbrack.gif)   |
|
Theorem | elecg 6586 |
Membership in an equivalence class. Theorem 72 of [Suppes] p. 82.
(Contributed by Mario Carneiro, 9-Jul-2014.)
|
      ![] ]](rbrack.gif)      |
|
Theorem | elec 6587 |
Membership in an equivalence class. Theorem 72 of [Suppes] p. 82.
(Contributed by NM, 23-Jul-1995.)
|
   ![] ]](rbrack.gif)     |
|
Theorem | relelec 6588 |
Membership in an equivalence class when is a relation. (Contributed
by Mario Carneiro, 11-Sep-2015.)
|
    ![] ]](rbrack.gif)
     |
|
Theorem | ecss 6589 |
An equivalence class is a subset of the domain. (Contributed by NM,
6-Aug-1995.) (Revised by Mario Carneiro, 12-Aug-2015.)
|
     ![] ]](rbrack.gif)
  |
|
Theorem | ecdmn0m 6590* |
A representative of an inhabited equivalence class belongs to the domain
of the equivalence relation. (Contributed by Jim Kingdon,
21-Aug-2019.)
|
 
  ![] ]](rbrack.gif)   |
|
Theorem | ereldm 6591 |
Equality of equivalence classes implies equivalence of domain
membership. (Contributed by NM, 28-Jan-1996.) (Revised by Mario
Carneiro, 12-Aug-2015.)
|
     ![] ]](rbrack.gif)   ![] ]](rbrack.gif)  

   |
|
Theorem | erth 6592 |
Basic property of equivalence relations. Theorem 73 of [Suppes] p. 82.
(Contributed by NM, 23-Jul-1995.) (Revised by Mario Carneiro,
6-Jul-2015.)
|
          ![] ]](rbrack.gif)   ![] ]](rbrack.gif)    |
|
Theorem | erth2 6593 |
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 6594 |
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 6595 |
An equivalence class modulo the identity relation is a singleton.
(Contributed by NM, 24-Oct-2004.)
|
     |
|
Theorem | qseq1 6596 |
Equality theorem for quotient set. (Contributed by NM, 23-Jul-1995.)
|
    
      |
|
Theorem | qseq2 6597 |
Equality theorem for quotient set. (Contributed by NM, 23-Jul-1995.)
|
    
      |
|
Theorem | elqsg 6598* |
Closed form of elqs 6599. (Contributed by Rodolfo Medina,
12-Oct-2010.)
|
      
  ![] ]](rbrack.gif)    |
|
Theorem | elqs 6599* |
Membership in a quotient set. (Contributed by NM, 23-Jul-1995.)
|
     
  ![] ]](rbrack.gif)   |
|
Theorem | elqsi 6600* |
Membership in a quotient set. (Contributed by NM, 23-Jul-1995.)
|
     
  ![] ]](rbrack.gif)   |