Type | Label | Description |
Statement |
|
Theorem | nnmcl 6501 |
Closure of multiplication of natural numbers. Proposition 8.17 of
[TakeutiZaring] p. 63.
(Contributed by NM, 20-Sep-1995.) (Proof
shortened by Andrew Salmon, 22-Oct-2011.)
|
    
  |
|
Theorem | nnacli 6502 |
is closed under
addition. Inference form of nnacl 6500.
(Contributed by Scott Fenton, 20-Apr-2012.)
|
 
 |
|
Theorem | nnmcli 6503 |
is closed under
multiplication. Inference form of nnmcl 6501.
(Contributed by Scott Fenton, 20-Apr-2012.)
|
 
 |
|
Theorem | nnacom 6504 |
Addition of natural numbers is commutative. Theorem 4K(2) of [Enderton]
p. 81. (Contributed by NM, 6-May-1995.) (Revised by Mario Carneiro,
15-Nov-2014.)
|
    
    |
|
Theorem | nnaass 6505 |
Addition of natural numbers is associative. Theorem 4K(1) of [Enderton]
p. 81. (Contributed by NM, 20-Sep-1995.) (Revised by Mario Carneiro,
15-Nov-2014.)
|
     
  
    |
|
Theorem | nndi 6506 |
Distributive law for natural numbers (left-distributivity). Theorem
4K(3) of [Enderton] p. 81.
(Contributed by NM, 20-Sep-1995.) (Revised
by Mario Carneiro, 15-Nov-2014.)
|
          
    |
|
Theorem | nnmass 6507 |
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 6508 |
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 6509 |
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 6510 |
Distributive law for natural numbers (right-distributivity). (Contributed
by Jim Kingdon, 3-Dec-2019.)
|
     
    
    |
|
Theorem | nnsucelsuc 6511 |
Membership is inherited by successors. The reverse direction holds for
all ordinals, as seen at onsucelsucr 4522, but the forward direction, for
all ordinals, implies excluded middle as seen as onsucelsucexmid 4544.
(Contributed by Jim Kingdon, 25-Aug-2019.)
|
     |
|
Theorem | nnsucsssuc 6512 |
Membership is inherited by successors. The reverse direction holds for
all ordinals, as seen at onsucsssucr 4523, but the forward direction, for
all ordinals, implies excluded middle as seen as onsucsssucexmid 4541.
(Contributed by Jim Kingdon, 25-Aug-2019.)
|
   
   |
|
Theorem | nntri3or 6513 |
Trichotomy for natural numbers. (Contributed by Jim Kingdon,
25-Aug-2019.)
|
       |
|
Theorem | nntri2 6514 |
A trichotomy law for natural numbers. (Contributed by Jim Kingdon,
28-Aug-2019.)
|
         |
|
Theorem | nnsucuniel 6515 |
Given an element of
the union of a natural number ,
is an element of itself. The reverse
direction holds
for all ordinals (sucunielr 4524). The forward direction for all
ordinals implies excluded middle (ordsucunielexmid 4545). (Contributed
by Jim Kingdon, 13-Mar-2022.)
|
  
   |
|
Theorem | nntri1 6516 |
A trichotomy law for natural numbers. (Contributed by Jim Kingdon,
28-Aug-2019.)
|
       |
|
Theorem | nntri3 6517 |
A trichotomy law for natural numbers. (Contributed by Jim Kingdon,
15-May-2020.)
|
         |
|
Theorem | nntri2or2 6518 |
A trichotomy law for natural numbers. (Contributed by Jim Kingdon,
15-Sep-2021.)
|
       |
|
Theorem | nndceq 6519 |
Equality of natural numbers is decidable. Theorem 7.2.6 of [HoTT], p.
(varies). For the specific case where is zero, see nndceq0 4632.
(Contributed by Jim Kingdon, 31-Aug-2019.)
|
   DECID
  |
|
Theorem | nndcel 6520 |
Set membership between two natural numbers is decidable. (Contributed by
Jim Kingdon, 6-Sep-2019.)
|
   DECID
  |
|
Theorem | nnsseleq 6521 |
For natural numbers, inclusion is equivalent to membership or equality.
(Contributed by Jim Kingdon, 16-Sep-2021.)
|
         |
|
Theorem | nnsssuc 6522 |
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 6523 |
Transitive law for natural numbers. (Contributed by Jim Kingdon,
22-Jul-2023.)
|
         |
|
Theorem | dcdifsnid 6524* |
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 3753 from subset to equality but the proof relies
on equality being
decidable. (Contributed by Jim Kingdon, 17-Jun-2022.)
|
    DECID
           |
|
Theorem | fnsnsplitdc 6525* |
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 6526* |
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 6527 |
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 3753
from subset to equality but the proof relies on equality being
decidable. (Contributed by Jim Kingdon, 31-Aug-2021.)
|
          
  |
|
Theorem | nnaordi 6528 |
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 6529 |
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 6530 |
Ordering property of addition of natural numbers. (Contributed by NM,
9-Nov-2002.)
|
           |
|
Theorem | nnaword 6531 |
Weak ordering property of addition. (Contributed by NM, 17-Sep-1995.)
(Revised by Mario Carneiro, 15-Nov-2014.)
|
           |
|
Theorem | nnacan 6532 |
Cancellation law for addition of natural numbers. (Contributed by NM,
27-Oct-1995.) (Revised by Mario Carneiro, 15-Nov-2014.)
|
     
 
   |
|
Theorem | nnaword1 6533 |
Weak ordering property of addition. (Contributed by NM, 9-Nov-2002.)
(Revised by Mario Carneiro, 15-Nov-2014.)
|
       |
|
Theorem | nnaword2 6534 |
Weak ordering property of addition. (Contributed by NM, 9-Nov-2002.)
|
       |
|
Theorem | nnawordi 6535 |
Adding to both sides of an inequality in . (Contributed by Scott
Fenton, 16-Apr-2012.) (Revised by Mario Carneiro, 12-May-2012.)
|
           |
|
Theorem | nnmordi 6536 |
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 6537 |
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 6538 |
Weak ordering property of ordinal multiplication. (Contributed by Mario
Carneiro, 17-Nov-2014.)
|
             |
|
Theorem | nnmcan 6539 |
Cancellation law for multiplication of natural numbers. (Contributed by
NM, 26-Oct-1995.) (Revised by Mario Carneiro, 15-Nov-2014.)
|
             |
|
Theorem | 1onn 6540 |
One is a natural number. (Contributed by NM, 29-Oct-1995.)
|
 |
|
Theorem | 2onn 6541 |
The ordinal 2 is a natural number. (Contributed by NM, 28-Sep-2004.)
|
 |
|
Theorem | 3onn 6542 |
The ordinal 3 is a natural number. (Contributed by Mario Carneiro,
5-Jan-2016.)
|
 |
|
Theorem | 4onn 6543 |
The ordinal 4 is a natural number. (Contributed by Mario Carneiro,
5-Jan-2016.)
|
 |
|
Theorem | 2ssom 6544 |
The ordinal 2 is included in the set of natural number ordinals.
(Contributed by BJ, 5-Aug-2024.)
|
 |
|
Theorem | nnm1 6545 |
Multiply an element of by .
(Contributed by Mario
Carneiro, 17-Nov-2014.)
|
  
  |
|
Theorem | nnm2 6546 |
Multiply an element of by .
(Contributed by Scott Fenton,
18-Apr-2012.) (Revised by Mario Carneiro, 17-Nov-2014.)
|
  
    |
|
Theorem | nn2m 6547 |
Multiply an element of by .
(Contributed by Scott Fenton,
16-Apr-2012.) (Revised by Mario Carneiro, 17-Nov-2014.)
|
  
    |
|
Theorem | nnaordex 6548* |
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 6549* |
Equivalence for weak ordering of natural numbers. (Contributed by NM,
8-Nov-2002.) (Revised by Mario Carneiro, 15-Nov-2014.)
|
     

   |
|
Theorem | nnm00 6550 |
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 6551 |
Extend the definition of a wff to include the equivalence predicate.
|
 |
|
Syntax | cec 6552 |
Extend the definition of a class to include equivalence class.
|
  ![] ]](rbrack.gif)  |
|
Syntax | cqs 6553 |
Extend the definition of a class to include quotient set.
|
     |
|
Definition | df-er 6554 |
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 6555 we derive a
more typical definition. We show that an equivalence relation is
reflexive, symmetric, and transitive in erref 6574, ersymb 6568, and ertr 6569.
(Contributed by NM, 4-Jun-1995.) (Revised by Mario Carneiro,
2-Nov-2015.)
|
   
      |
|
Theorem | dfer2 6555* |
Alternate definition of equivalence predicate. (Contributed by NM,
3-Jan-1997.) (Revised by Mario Carneiro, 12-Aug-2015.)
|
           
  
              |
|
Definition | df-ec 6556 |
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 6555). 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 6557. (Contributed by
NM, 23-Jul-1995.)
|
  ![] ]](rbrack.gif)        |
|
Theorem | dfec2 6557* |
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 6558 |
An equivalence class modulo a set is a set. (Contributed by NM,
24-Jul-1995.)
|
   ![] ]](rbrack.gif)   |
|
Theorem | ecexr 6559 |
An inhabited equivalence class implies the representative is a set.
(Contributed by Mario Carneiro, 9-Jul-2014.)
|
   ![] ]](rbrack.gif)   |
|
Definition | df-qs 6560* |
Define quotient set.
is usually an equivalence relation.
Definition of [Enderton] p. 58.
(Contributed by NM, 23-Jul-1995.)
|
   
 
  ![] ]](rbrack.gif)   |
|
Theorem | ereq1 6561 |
Equality theorem for equivalence predicate. (Contributed by NM,
4-Jun-1995.) (Revised by Mario Carneiro, 12-Aug-2015.)
|
     |
|
Theorem | ereq2 6562 |
Equality theorem for equivalence predicate. (Contributed by Mario
Carneiro, 12-Aug-2015.)
|
     |
|
Theorem | errel 6563 |
An equivalence relation is a relation. (Contributed by Mario Carneiro,
12-Aug-2015.)
|
   |
|
Theorem | erdm 6564 |
The domain of an equivalence relation. (Contributed by Mario Carneiro,
12-Aug-2015.)
|
   |
|
Theorem | ercl 6565 |
Elementhood in the field of an equivalence relation. (Contributed by
Mario Carneiro, 12-Aug-2015.)
|
         |
|
Theorem | ersym 6566 |
An equivalence relation is symmetric. (Contributed by NM, 4-Jun-1995.)
(Revised by Mario Carneiro, 12-Aug-2015.)
|
           |
|
Theorem | ercl2 6567 |
Elementhood in the field of an equivalence relation. (Contributed by
Mario Carneiro, 12-Aug-2015.)
|
         |
|
Theorem | ersymb 6568 |
An equivalence relation is symmetric. (Contributed by NM, 30-Jul-1995.)
(Revised by Mario Carneiro, 12-Aug-2015.)
|
           |
|
Theorem | ertr 6569 |
An equivalence relation is transitive. (Contributed by NM, 4-Jun-1995.)
(Revised by Mario Carneiro, 12-Aug-2015.)
|
               |
|
Theorem | ertrd 6570 |
A transitivity relation for equivalences. (Contributed by Mario
Carneiro, 9-Jul-2014.)
|
               |
|
Theorem | ertr2d 6571 |
A transitivity relation for equivalences. (Contributed by Mario
Carneiro, 9-Jul-2014.)
|
               |
|
Theorem | ertr3d 6572 |
A transitivity relation for equivalences. (Contributed by Mario
Carneiro, 9-Jul-2014.)
|
               |
|
Theorem | ertr4d 6573 |
A transitivity relation for equivalences. (Contributed by Mario
Carneiro, 9-Jul-2014.)
|
               |
|
Theorem | erref 6574 |
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 6575 |
The converse of an equivalence relation is itself. (Contributed by
Mario Carneiro, 12-Aug-2015.)
|
 
  |
|
Theorem | errn 6576 |
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 6577 |
An equivalence relation is a subset of the cartesian product of the field.
(Contributed by Mario Carneiro, 12-Aug-2015.)
|

    |
|
Theorem | erex 6578 |
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 6579 |
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 6580* |
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 6581 |
Evaluate the incomparability relation. (Contributed by Mario Carneiro,
9-Jul-2014.)
|
               |
|
Theorem | swoer 6582* |
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 6583* |
The incomparability equivalence relation is compatible with the
original order. (Contributed by Mario Carneiro, 31-Dec-2014.)
|
      
 

   
   

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

   
   

            
   |
|
Theorem | eqerlem 6585* |
Lemma for eqer 6586. (Contributed by NM, 17-Mar-2008.) (Proof
shortened
by Mario Carneiro, 6-Dec-2016.)
|
 
        
 ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)   |
|
Theorem | eqer 6586* |
Equivalence relation involving equality of dependent classes   
and    . (Contributed by NM, 17-Mar-2008.) (Revised by Mario
Carneiro, 12-Aug-2015.)
|
 
      |
|
Theorem | ider 6587 |
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 6588 |
The empty set is an equivalence relation on the empty set. (Contributed
by Mario Carneiro, 5-Sep-2015.)
|
 |
|
Theorem | eceq1 6589 |
Equality theorem for equivalence class. (Contributed by NM,
23-Jul-1995.)
|
   ![] ]](rbrack.gif)   ![] ]](rbrack.gif)   |
|
Theorem | eceq1d 6590 |
Equality theorem for equivalence class (deduction form). (Contributed
by Jim Kingdon, 31-Dec-2019.)
|
     ![] ]](rbrack.gif)
  ![] ]](rbrack.gif)   |
|
Theorem | eceq2 6591 |
Equality theorem for equivalence class. (Contributed by NM,
23-Jul-1995.)
|
   ![] ]](rbrack.gif)   ![] ]](rbrack.gif)   |
|
Theorem | elecg 6592 |
Membership in an equivalence class. Theorem 72 of [Suppes] p. 82.
(Contributed by Mario Carneiro, 9-Jul-2014.)
|
      ![] ]](rbrack.gif)      |
|
Theorem | elec 6593 |
Membership in an equivalence class. Theorem 72 of [Suppes] p. 82.
(Contributed by NM, 23-Jul-1995.)
|
   ![] ]](rbrack.gif)     |
|
Theorem | relelec 6594 |
Membership in an equivalence class when is a relation. (Contributed
by Mario Carneiro, 11-Sep-2015.)
|
    ![] ]](rbrack.gif)
     |
|
Theorem | ecss 6595 |
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 6596* |
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 6597 |
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 6598 |
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 6599 |
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 6600 |
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)   |