Theorem List for Intuitionistic Logic Explorer - 6301-6400 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | nndcel 6301 |
Set membership between two natural numbers is decidable. (Contributed by
Jim Kingdon, 6-Sep-2019.)
|
   DECID
  |
|
Theorem | nnsseleq 6302 |
For natural numbers, inclusion is equivalent to membership or equality.
(Contributed by Jim Kingdon, 16-Sep-2021.)
|
         |
|
Theorem | dcdifsnid 6303* |
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 3605 from subset to equality but the proof relies
on equality being
decidable. (Contributed by Jim Kingdon, 17-Jun-2022.)
|
    DECID
           |
|
Theorem | fnsnsplitdc 6304* |
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 6305* |
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 6306 |
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 3605
from subset to equality but the proof relies on equality being
decidable. (Contributed by Jim Kingdon, 31-Aug-2021.)
|
          
  |
|
Theorem | nnaordi 6307 |
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 6308 |
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 6309 |
Ordering property of addition of natural numbers. (Contributed by NM,
9-Nov-2002.)
|
           |
|
Theorem | nnaword 6310 |
Weak ordering property of addition. (Contributed by NM, 17-Sep-1995.)
(Revised by Mario Carneiro, 15-Nov-2014.)
|
           |
|
Theorem | nnacan 6311 |
Cancellation law for addition of natural numbers. (Contributed by NM,
27-Oct-1995.) (Revised by Mario Carneiro, 15-Nov-2014.)
|
     
 
   |
|
Theorem | nnaword1 6312 |
Weak ordering property of addition. (Contributed by NM, 9-Nov-2002.)
(Revised by Mario Carneiro, 15-Nov-2014.)
|
       |
|
Theorem | nnaword2 6313 |
Weak ordering property of addition. (Contributed by NM, 9-Nov-2002.)
|
       |
|
Theorem | nnawordi 6314 |
Adding to both sides of an inequality in (Contributed by Scott
Fenton, 16-Apr-2012.) (Revised by Mario Carneiro, 12-May-2012.)
|
           |
|
Theorem | nnmordi 6315 |
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 6316 |
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 6317 |
Weak ordering property of ordinal multiplication. (Contributed by Mario
Carneiro, 17-Nov-2014.)
|
             |
|
Theorem | nnmcan 6318 |
Cancellation law for multiplication of natural numbers. (Contributed by
NM, 26-Oct-1995.) (Revised by Mario Carneiro, 15-Nov-2014.)
|
             |
|
Theorem | 1onn 6319 |
One is a natural number. (Contributed by NM, 29-Oct-1995.)
|
 |
|
Theorem | 2onn 6320 |
The ordinal 2 is a natural number. (Contributed by NM, 28-Sep-2004.)
|
 |
|
Theorem | 3onn 6321 |
The ordinal 3 is a natural number. (Contributed by Mario Carneiro,
5-Jan-2016.)
|
 |
|
Theorem | 4onn 6322 |
The ordinal 4 is a natural number. (Contributed by Mario Carneiro,
5-Jan-2016.)
|
 |
|
Theorem | nnm1 6323 |
Multiply an element of by .
(Contributed by Mario
Carneiro, 17-Nov-2014.)
|
  
  |
|
Theorem | nnm2 6324 |
Multiply an element of by
(Contributed by Scott Fenton,
18-Apr-2012.) (Revised by Mario Carneiro, 17-Nov-2014.)
|
  
    |
|
Theorem | nn2m 6325 |
Multiply an element of by
(Contributed by Scott Fenton,
16-Apr-2012.) (Revised by Mario Carneiro, 17-Nov-2014.)
|
  
    |
|
Theorem | nnaordex 6326* |
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 6327* |
Equivalence for weak ordering of natural numbers. (Contributed by NM,
8-Nov-2002.) (Revised by Mario Carneiro, 15-Nov-2014.)
|
     

   |
|
Theorem | nnm00 6328 |
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.24 Equivalence relations and
classes
|
|
Syntax | wer 6329 |
Extend the definition of a wff to include the equivalence predicate.
|
 |
|
Syntax | cec 6330 |
Extend the definition of a class to include equivalence class.
|
  ![] ]](rbrack.gif)  |
|
Syntax | cqs 6331 |
Extend the definition of a class to include quotient set.
|
     |
|
Definition | df-er 6332 |
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 6333 we derive a
more typical definition. We show that an equivalence relation is
reflexive, symmetric, and transitive in erref 6352, ersymb 6346, and ertr 6347.
(Contributed by NM, 4-Jun-1995.) (Revised by Mario Carneiro,
2-Nov-2015.)
|
   
      |
|
Theorem | dfer2 6333* |
Alternate definition of equivalence predicate. (Contributed by NM,
3-Jan-1997.) (Revised by Mario Carneiro, 12-Aug-2015.)
|
           
  
              |
|
Definition | df-ec 6334 |
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 6333). 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 6335. (Contributed by
NM, 23-Jul-1995.)
|
  ![] ]](rbrack.gif)        |
|
Theorem | dfec2 6335* |
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 6336 |
An equivalence class modulo a set is a set. (Contributed by NM,
24-Jul-1995.)
|
   ![] ]](rbrack.gif)   |
|
Theorem | ecexr 6337 |
An inhabited equivalence class implies the representative is a set.
(Contributed by Mario Carneiro, 9-Jul-2014.)
|
   ![] ]](rbrack.gif)   |
|
Definition | df-qs 6338* |
Define quotient set.
is usually an equivalence relation.
Definition of [Enderton] p. 58.
(Contributed by NM, 23-Jul-1995.)
|
   
 
  ![] ]](rbrack.gif)   |
|
Theorem | ereq1 6339 |
Equality theorem for equivalence predicate. (Contributed by NM,
4-Jun-1995.) (Revised by Mario Carneiro, 12-Aug-2015.)
|
     |
|
Theorem | ereq2 6340 |
Equality theorem for equivalence predicate. (Contributed by Mario
Carneiro, 12-Aug-2015.)
|
     |
|
Theorem | errel 6341 |
An equivalence relation is a relation. (Contributed by Mario Carneiro,
12-Aug-2015.)
|
   |
|
Theorem | erdm 6342 |
The domain of an equivalence relation. (Contributed by Mario Carneiro,
12-Aug-2015.)
|
   |
|
Theorem | ercl 6343 |
Elementhood in the field of an equivalence relation. (Contributed by
Mario Carneiro, 12-Aug-2015.)
|
         |
|
Theorem | ersym 6344 |
An equivalence relation is symmetric. (Contributed by NM, 4-Jun-1995.)
(Revised by Mario Carneiro, 12-Aug-2015.)
|
           |
|
Theorem | ercl2 6345 |
Elementhood in the field of an equivalence relation. (Contributed by
Mario Carneiro, 12-Aug-2015.)
|
         |
|
Theorem | ersymb 6346 |
An equivalence relation is symmetric. (Contributed by NM, 30-Jul-1995.)
(Revised by Mario Carneiro, 12-Aug-2015.)
|
           |
|
Theorem | ertr 6347 |
An equivalence relation is transitive. (Contributed by NM, 4-Jun-1995.)
(Revised by Mario Carneiro, 12-Aug-2015.)
|
               |
|
Theorem | ertrd 6348 |
A transitivity relation for equivalences. (Contributed by Mario
Carneiro, 9-Jul-2014.)
|
               |
|
Theorem | ertr2d 6349 |
A transitivity relation for equivalences. (Contributed by Mario
Carneiro, 9-Jul-2014.)
|
               |
|
Theorem | ertr3d 6350 |
A transitivity relation for equivalences. (Contributed by Mario
Carneiro, 9-Jul-2014.)
|
               |
|
Theorem | ertr4d 6351 |
A transitivity relation for equivalences. (Contributed by Mario
Carneiro, 9-Jul-2014.)
|
               |
|
Theorem | erref 6352 |
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 6353 |
The converse of an equivalence relation is itself. (Contributed by
Mario Carneiro, 12-Aug-2015.)
|
 
  |
|
Theorem | errn 6354 |
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 6355 |
An equivalence relation is a subset of the cartesian product of the field.
(Contributed by Mario Carneiro, 12-Aug-2015.)
|

    |
|
Theorem | erex 6356 |
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 6357 |
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 6358* |
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 6359 |
Evaluate the incomparability relation. (Contributed by Mario Carneiro,
9-Jul-2014.)
|
               |
|
Theorem | swoer 6360* |
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 6361* |
The incomparability equivalence relation is compatible with the
original order. (Contributed by Mario Carneiro, 31-Dec-2014.)
|
      
 

   
   

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

   
   

            
   |
|
Theorem | eqerlem 6363* |
Lemma for eqer 6364. (Contributed by NM, 17-Mar-2008.) (Proof
shortened
by Mario Carneiro, 6-Dec-2016.)
|
 
        
 ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)   |
|
Theorem | eqer 6364* |
Equivalence relation involving equality of dependent classes   
and    . (Contributed by NM, 17-Mar-2008.) (Revised by Mario
Carneiro, 12-Aug-2015.)
|
 
      |
|
Theorem | ider 6365 |
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 6366 |
The empty set is an equivalence relation on the empty set. (Contributed
by Mario Carneiro, 5-Sep-2015.)
|
 |
|
Theorem | eceq1 6367 |
Equality theorem for equivalence class. (Contributed by NM,
23-Jul-1995.)
|
   ![] ]](rbrack.gif)   ![] ]](rbrack.gif)   |
|
Theorem | eceq1d 6368 |
Equality theorem for equivalence class (deduction form). (Contributed
by Jim Kingdon, 31-Dec-2019.)
|
     ![] ]](rbrack.gif)
  ![] ]](rbrack.gif)   |
|
Theorem | eceq2 6369 |
Equality theorem for equivalence class. (Contributed by NM,
23-Jul-1995.)
|
   ![] ]](rbrack.gif)   ![] ]](rbrack.gif)   |
|
Theorem | elecg 6370 |
Membership in an equivalence class. Theorem 72 of [Suppes] p. 82.
(Contributed by Mario Carneiro, 9-Jul-2014.)
|
      ![] ]](rbrack.gif)      |
|
Theorem | elec 6371 |
Membership in an equivalence class. Theorem 72 of [Suppes] p. 82.
(Contributed by NM, 23-Jul-1995.)
|
   ![] ]](rbrack.gif)     |
|
Theorem | relelec 6372 |
Membership in an equivalence class when is a relation. (Contributed
by Mario Carneiro, 11-Sep-2015.)
|
    ![] ]](rbrack.gif)
     |
|
Theorem | ecss 6373 |
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 6374* |
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 6375 |
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 6376 |
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 6377 |
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 6378 |
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 6379 |
An equivalence class modulo the identity relation is a singleton.
(Contributed by NM, 24-Oct-2004.)
|
     |
|
Theorem | qseq1 6380 |
Equality theorem for quotient set. (Contributed by NM, 23-Jul-1995.)
|
    
      |
|
Theorem | qseq2 6381 |
Equality theorem for quotient set. (Contributed by NM, 23-Jul-1995.)
|
    
      |
|
Theorem | elqsg 6382* |
Closed form of elqs 6383. (Contributed by Rodolfo Medina,
12-Oct-2010.)
|
      
  ![] ]](rbrack.gif)    |
|
Theorem | elqs 6383* |
Membership in a quotient set. (Contributed by NM, 23-Jul-1995.)
|
     
  ![] ]](rbrack.gif)   |
|
Theorem | elqsi 6384* |
Membership in a quotient set. (Contributed by NM, 23-Jul-1995.)
|
     
  ![] ]](rbrack.gif)   |
|
Theorem | ecelqsg 6385 |
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 6386 |
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 6387 |
"Closure" law for equivalence class of ordered pairs. (Contributed
by
NM, 25-Mar-1996.)
|
              ![] ]](rbrack.gif)   |
|
Theorem | qsexg 6388 |
A quotient set exists. (Contributed by FL, 19-May-2007.) (Revised by
Mario Carneiro, 9-Jul-2014.)
|
    
  |
|
Theorem | qsex 6389 |
A quotient set exists. (Contributed by NM, 14-Aug-1995.)
|
   
 |
|
Theorem | uniqs 6390 |
The union of a quotient set. (Contributed by NM, 9-Dec-2008.)
|
     
      |
|
Theorem | qsss 6391 |
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 6392 |
The union of a quotient set. (Contributed by Mario Carneiro,
11-Jul-2014.)
|
         
  |
|
Theorem | snec 6393 |
The singleton of an equivalence class. (Contributed by NM,
29-Jan-1999.) (Revised by Mario Carneiro, 9-Jul-2014.)
|
   ![] ]](rbrack.gif)         |
|
Theorem | ecqs 6394 |
Equivalence class in terms of quotient set. (Contributed by NM,
29-Jan-1999.)
|
  ![] ]](rbrack.gif)
        |
|
Theorem | ecid 6395 |
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 6396 |
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 6397 |
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 6398* |
Implicit substitution of class for equivalence class. (Contributed by
Mario Carneiro, 9-Jul-2014.)
|
       ![] ]](rbrack.gif)             |
|
Theorem | ectocl 6399* |
Implicit substitution of class for equivalence class. (Contributed by
NM, 23-Jul-1995.) (Revised by Mario Carneiro, 9-Jul-2014.)
|
       ![] ]](rbrack.gif)    
    |
|
Theorem | elqsn0m 6400* |
An element of a quotient set is inhabited. (Contributed by Jim Kingdon,
21-Aug-2019.)
|
 
    

  |