Type | Label | Description |
Statement |
|
Definition | df-ref 5901* |
Define the set of all reflexive relationships over a base set.
(Contributed by SF, 19-Feb-2015.)
|
Ref     
    |
|
Definition | df-antisym 5902* |
Define the set of all antisymmetric relationships over a base set.
(Contributed by SF, 19-Feb-2015.)
|
Antisym     
           |
|
Definition | df-partial 5903 |
Define the set of all partial orderings over a base set. (Contributed
by SF, 19-Feb-2015.)
|
Po  Ref Trans Antisym
 |
|
Definition | df-connex 5904* |
Define the set of all connected relationships over a base set.
(Contributed by SF, 19-Feb-2015.)
|
Connex     
         |
|
Definition | df-strict 5905 |
Define the set of all strict orderings over a base set. (Contributed by
SF, 19-Feb-2015.)
|
Or Po Connex  |
|
Definition | df-found 5906* |
Define the set of all founded relationships over a base set.
(Contributed by SF, 19-Feb-2015.)
|
Fr        
          |
|
Definition | df-we 5907 |
Define the set of all well orderings over a base set. (Contributed by
SF, 19-Feb-2015.)
|
We Or Fr  |
|
Definition | df-ext 5908* |
Define the set of all extensional relationships over a base set.
(Contributed by SF, 19-Feb-2015.)
|
Ext     
  
         |
|
Definition | df-sym 5909* |
Define the set of all symmetric relationships over a base set.
(Contributed by SF, 19-Feb-2015.)
|
Sym     
         |
|
Definition | df-er 5910 |
Define the set of all equivalence relationships over a base set.
(Contributed by SF, 19-Feb-2015.)
|
Er Sym Trans  |
|
Theorem | transex 5911 |
The class of all transitive relationships is a set. (Contributed by SF,
19-Feb-2015.)
|
Trans  |
|
Theorem | refex 5912 |
The class of all reflexive relationships is a set. (Contributed by SF,
11-Mar-2015.)
|
Ref  |
|
Theorem | antisymex 5913 |
The class of all antisymmetric relationships is a set. (Contributed by
SF, 11-Mar-2015.)
|
Antisym  |
|
Theorem | connexex 5914 |
The class of all connected relationships is a set. (Contributed by SF,
11-Mar-2015.)
|
Connex  |
|
Theorem | foundex 5915 |
The class of all founded relationships is a set. (Contributed by SF,
19-Feb-2015.)
|
Fr  |
|
Theorem | extex 5916 |
The class of all extensional relationships is a set. (Contributed by
SF, 19-Feb-2015.)
|
Ext  |
|
Theorem | symex 5917 |
The class of all symmetric relationships is a set. (Contributed by SF,
20-Feb-2015.)
|
Sym  |
|
Theorem | partialex 5918 |
The class of all partial orderings is a set. (Contributed by SF,
11-Mar-2015.)
|
Po  |
|
Theorem | strictex 5919 |
The class of all strict orderings is a set. (Contributed by SF,
19-Feb-2015.)
|
Or  |
|
Theorem | weex 5920 |
The class of all well orderings is a set. (Contributed by SF,
19-Feb-2015.)
|
We  |
|
Theorem | erex 5921 |
The class of all equivalence relationships is a set. (Contributed by SF,
20-Feb-2015.)
|
Er  |
|
Theorem | trd 5922 |
Transitivity law in natural deduction form. (Contributed by SF,
20-Feb-2015.)
|
 Trans
                    |
|
Theorem | frd 5923* |
Founded relationship in natural deduction form. (Contributed by SF,
12-Mar-2015.)
|
 Fr                 |
|
Theorem | extd 5924* |
Extensional relationship in natural deduction form. (Contributed by SF,
20-Feb-2015.)
|
 Ext                   |
|
Theorem | symd 5925 |
Symmetric relationship in natural deduction form. (Contributed by SF,
20-Feb-2015.)
|
 Sym               |
|
Theorem | trrd 5926* |
Deduce transitivity from its properties. (Contributed by SF,
22-Feb-2015.)
|
       
           Trans
  |
|
Theorem | refrd 5927* |
Deduce reflexivity from its properties. (Contributed by SF,
12-Mar-2015.)
|
           Ref   |
|
Theorem | refd 5928 |
Natural deduction form of reflexivity. (Contributed by SF,
20-Mar-2015.)
|
 Ref         |
|
Theorem | antird 5929* |
Deduce antisymmetry from its properties. (Contributed by SF,
12-Mar-2015.)
|
              
  Antisym   |
|
Theorem | antid 5930 |
The antisymmetry property. (Contributed by SF, 18-Mar-2015.)
|
 Antisym
                |
|
Theorem | connexrd 5931* |
Deduce connectivity from its properties. (Contributed by SF,
12-Mar-2015.)
|
      
        Connex
  |
|
Theorem | connexd 5932 |
The connectivity property. (Contributed by SF, 18-Mar-2015.)
|
 Connex
              |
|
Theorem | ersymtr 5933 |
Equivalence relationship as symmetric, transitive relationship.
(Contributed by SF, 22-Feb-2015.)
|
 Er  Sym Trans    |
|
Theorem | porta 5934 |
Partial ordering as reflexive, transitive, antisymmetric relationship.
(Contributed by SF, 12-Mar-2015.)
|
 Po  Ref Trans Antisym    |
|
Theorem | sopc 5935 |
Linear ordering as partial, connected relationship. (Contributed by SF,
12-Mar-2015.)
|
 Or  Po Connex    |
|
Theorem | frds 5936* |
Substitution schema verson of frd 5923. (Contributed by SF,
19-Mar-2015.)
|

          Fr        
         |
|
Theorem | pod 5937* |
A reflexive, transitive, and anti-symmetric ordering is a partial
ordering. (Contributed by SF, 22-Feb-2015.)
|
             
                    
  Po   |
|
Theorem | sod 5938* |
A reflexive, transitive, antisymmetric, and connected relationship is a
strict ordering. (Contributed by SF, 12-Mar-2015.)
|
             
                    
            Or   |
|
Theorem | weds 5939* |
Any property that holds for some element of a well-ordered set has
an minimal
element satisfying that property. (Contributed by SF,
20-Mar-2015.)
|

          We        
       |
|
Theorem | po0 5940 |
Anything partially orders the empty set. (Contributed by SF,
12-Mar-2015.)
|
   Po   |
|
Theorem | connex0 5941 |
Anything is connected over the empty set. (Contributed by SF,
12-Mar-2015.)
|
   Connex
  |
|
Theorem | so0 5942 |
Anything totally orders the empty set. (Contributed by SF,
12-Mar-2015.)
|
   Or   |
|
Theorem | iserd 5943* |
A symmetric, transitive relationship is an equivalence relationship.
(Contributed by SF, 22-Feb-2015.)
|
                 
           Er   |
|
Theorem | ider 5944 |
The identity relationship is an equivalence relationship over the
universe. (Contributed by SF, 22-Feb-2015.)
|
Er  |
|
Theorem | ssetpov 5945 |
The subset relationship partially orders the universe. (Contributed by
SF, 12-Mar-2015.)
|
S Po  |
|
2.4.2 Equivalence relations and
classes
|
|
Syntax | cec 5946 |
Extend the definition of a class to include equivalence class.
|
  ![]](rbrack.gif)  |
|
Syntax | cqs 5947 |
Extend the definition of a class to include quotient set.
|
     |
|
Definition | df-ec 5948 |
Define the -coset of
. Exercise 35 of [Enderton] p. 61. This
is called the equivalence class of modulo when is
an
equivalence relation. 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 5949. (Contributed by set.mm contributors,
22-Feb-2015.)
|
  ![]](rbrack.gif)        |
|
Theorem | dfec2 5949* |
Alternate definition of -coset of .
Definition 34 of
[Suppes] p. 81. (Contributed by set.mm
contributors, 22-Feb-2015.)
|
  ![]](rbrack.gif)      |
|
Theorem | ecexg 5950 |
An equivalence class modulo a set is a set. (Contributed by set.mm
contributors, 24-Jul-1995.)
|
   ![]](rbrack.gif)   |
|
Theorem | ecexr 5951 |
A nonempty equivalence class implies the representative is a set.
(Contributed by set.mm contributors, 9-Jul-2014.)
|
   ![]](rbrack.gif)   |
|
Definition | df-qs 5952* |
Define quotient set.
is usually an equivalence relation.
Definition of [Enderton] p. 58.
(Contributed by set.mm contributors,
22-Feb-2015.)
|
   
 
  ![]](rbrack.gif)   |
|
Theorem | ersym 5953 |
An equivalence relation is symmetric. (Contributed by set.mm
contributors, 22-Feb-2015.)
|
 Er               |
|
Theorem | ersymb 5954 |
An equivalence relation is symmetric. (Contributed by set.mm
contributors, 30-Jul-1995.) (Revised by set.mm contributors,
9-Jul-2014.)
|
 Er               |
|
Theorem | ertr 5955 |
An equivalence relation is transitive. (Contributed by set.mm
contributors, 4-Jun-1995.) (Revised by set.mm contributors,
9-Jul-2014.)
|
 Er                     |
|
Theorem | ertrd 5956 |
A transitivity relation for equivalences. (Contributed by set.mm
contributors, 9-Jul-2014.)
|
 Er                     |
|
Theorem | ertr2d 5957 |
A transitivity relation for equivalences. (Contributed by set.mm
contributors, 9-Jul-2014.)
|
 Er                     |
|
Theorem | ertr3d 5958 |
A transitivity relation for equivalences. (Contributed by set.mm
contributors, 9-Jul-2014.)
|
 Er                     |
|
Theorem | ertr4d 5959 |
A transitivity relation for equivalences. (Contributed by set.mm
contributors, 9-Jul-2014.)
|
 Er                     |
|
Theorem | erref 5960 |
An equivalence relation is reflexive on its field. Compare Theorem 3M
of [Enderton] p. 56. (Contributed by
set.mm contributors,
6-May-2013.)
|
 Er           |
|
Theorem | eqerlem 5961* |
Lemma for eqer 5962. (Contributed by set.mm contributors,
17-Mar-2008.)
|
 
   
      ![]_](_urbrack.gif)
  ![]_](_urbrack.gif)   |
|
Theorem | eqer 5962* |
Equivalence relation involving equality of dependent classes   
and    . (Contributed by set.mm contributors, 17-Mar-2008.)
|
 
   
 Er  |
|
Theorem | eceq1 5963 |
Equality theorem for equivalence class. (Contributed by set.mm
contributors, 23-Jul-1995.)
|
   ![]](rbrack.gif)   ![]](rbrack.gif)   |
|
Theorem | eceq2 5964 |
Equality theorem for equivalence class. (Contributed by set.mm
contributors, 23-Jul-1995.)
|
   ![]](rbrack.gif)   ![]](rbrack.gif)   |
|
Theorem | elec 5965 |
Membership in an equivalence class. Theorem 72 of [Suppes] p. 82.
(Contributed by set.mm contributors, 9-Jul-2014.)
|
   ![]](rbrack.gif)     |
|
Theorem | erdmrn 5966 |
The range and domain of an equivalence relation are equal. (Contributed
by Rodolfo Medina, 11-Oct-2010.)
|
 Er   |
|
Theorem | ecss 5967 |
An equivalence class is a subset of the domain. (Contributed by set.mm
contributors, 6-Aug-1995.) (Revised by set.mm contributors,
9-Jul-2014.)
|
 Er       ![]](rbrack.gif)   |
|
Theorem | ecdmn0 5968 |
A representative of a nonempty equivalence class belongs to the domain
of the equivalence relation. (Contributed by set.mm contributors,
15-Feb-1996.) (Revised by set.mm contributors, 9-Jul-2014.)
|
   ![]](rbrack.gif)   |
|
Theorem | erth 5969 |
Basic property of equivalence relations. Theorem 73 of [Suppes] p. 82.
(Contributed by set.mm contributors, 23-Jul-1995.) (Revised by Mario
Carneiro, 9-Jul-2014.)
|
 Er              ![]](rbrack.gif)
  ![]](rbrack.gif)    |
|
Theorem | erth2 5970 |
Basic property of equivalence relations. Compare Theorem 73 of [Suppes]
p. 82. Assumes membership of the second argument in the domain.
(Contributed by set.mm contributors, 30-Jul-1995.) (Revised by set.mm
contributors, 9-Jul-2014.)
|
 Er              ![]](rbrack.gif)
  ![]](rbrack.gif)    |
|
Theorem | erthi 5971 |
Basic property of equivalence relations. Part of Lemma 3N of [Enderton]
p. 57. (Contributed by set.mm contributors, 30-Jul-1995.) (Revised by
set.mm contributors, 9-Jul-2014.)
|
 Er         ![]](rbrack.gif)
  ![]](rbrack.gif)   |
|
Theorem | ereldm 5972 |
Equality of equivalence classes implies equivalence of domain
membership. (Contributed by set.mm contributors, 28-Jan-1996.)
(Revised by set.mm contributors, 9-Jul-2014.)
|
 Er       ![]](rbrack.gif)   ![]](rbrack.gif)           |
|
Theorem | erdisj 5973 |
Equivalence classes do not overlap. In other words, two equivalence
classes are either equal or disjoint. Theorem 74 of [Suppes] p. 83.
(Contributed by set.mm contributors, 15-Jun-2004.) (Revised by Mario
Carneiro, 9-Jul-2014.)
|
 Er    ![]](rbrack.gif)   ![]](rbrack.gif)    ![]](rbrack.gif)   ![]](rbrack.gif)     |
|
Theorem | ecidsn 5974 |
An equivalence class modulo the identity relation is a singleton.
(Contributed by set.mm contributors, 24-Oct-2004.)
|
     |
|
Theorem | qseq1 5975 |
Equality theorem for quotient set. (Contributed by set.mm contributors,
23-Jul-1995.)
|
    
      |
|
Theorem | qseq2 5976 |
Equality theorem for quotient set. (Contributed by set.mm contributors,
23-Jul-1995.)
|
    
      |
|
Theorem | elqsg 5977* |
Closed form of elqs 5978. (Contributed by Rodolfo Medina,
12-Oct-2010.)
|
         ![]](rbrack.gif)    |
|
Theorem | elqs 5978* |
Membership in a quotient set. (Contributed by set.mm contributors,
23-Jul-1995.) (Revised by set.mm contributors, 12-Nov-2008.)
|
        ![]](rbrack.gif)   |
|
Theorem | elqsi 5979* |
Membership in a quotient set. (Contributed by set.mm contributors,
23-Jul-1995.)
|
     
  ![]](rbrack.gif)   |
|
Theorem | ecelqsg 5980 |
Membership of an equivalence class in a quotient set. (Contributed by
Jeff Madsen, 10-Jun-2010.)
|
     ![]](rbrack.gif)       |
|
Theorem | ecelqsi 5981 |
Membership of an equivalence class in a quotient set. (Contributed by
set.mm contributors, 25-Jul-1995.) (Revised by set.mm contributors,
9-Jul-2014.)
|
   ![]](rbrack.gif)       |
|
Theorem | ecopqsi 5982 |
"Closure" law for equivalence class of ordered pairs. (Contributed
by
set.mm contributors, 25-Mar-1996.)
|
              ![]](rbrack.gif)   |
|
Theorem | qsexg 5983 |
A quotient set exists. (Contributed by FL, 19-May-2007.)
|
      
  |
|
Theorem | qsex 5984 |
A quotient set exists. (Contributed by set.mm contributors,
14-Aug-1995.)
|
     |
|
Theorem | uniqs 5985 |
The union of a quotient set. (Contributed by set.mm contributors,
9-Dec-2008.)
|
     
      |
|
Theorem | uniqs2 5986 |
The union of a quotient set. (Contributed by set.mm contributors,
11-Jul-2014.)
|
 Er              |
|
Theorem | qsss 5987 |
A quotient set is a set of subsets of the base set. (Contributed by
Mario Carneiro, 9-Jul-2014.)
|
 Er              |
|
Theorem | snec 5988 |
The singleton of an equivalence class. (Contributed by set.mm
contributors, 29-Jan-1999.) (Revised by set.mm contributors,
9-Jul-2014.)
|
   ![]](rbrack.gif) 
       |
|
Theorem | ecqs 5989 |
Equivalence class in terms of quotient set. (Contributed by set.mm
contributors, 29-Jan-1999.) (Revised by set.mm contributors,
15-Jan-2009.)
|
  ![]](rbrack.gif)         |
|
Theorem | ecid 5990 |
A set is equal to its converse epsilon coset. (Note: converse epsilon
is not an equivalence relation.) (Contributed by set.mm contributors,
13-Aug-1995.) (Revised by set.mm contributors, 9-Jul-2014.)
|
  ![]](rbrack.gif)  |
|
Theorem | qsid 5991 |
A set is equal to its quotient set mod converse epsilon. (Note:
converse epsilon is not an equivalence relation.) (Contributed by
set.mm contributors, 13-Aug-1995.) (Revised by set.mm contributors,
9-Jul-2014.)
|
  
 |
|
Theorem | ectocld 5992* |
Implicit substitution of class for equivalence class. (Contributed by
set.mm contributors, 9-Jul-2014.)
|
       ![]](rbrack.gif)
     
   
  |
|
Theorem | ectocl 5993* |
Implicit substitution of class for equivalence class. (Contributed by
set.mm contributors, 23-Jul-1995.) (Revised by set.mm contributors,
9-Jul-2014.)
|
       ![]](rbrack.gif)
        |
|
Theorem | elqsn0 5994 |
A quotient set doesn't contain the empty set. (Contributed by set.mm
contributors, 24-Aug-1995.) (Revised by set.mm contributors,
21-Mar-2007.)
|
         |
|
Theorem | ecelqsdm 5995 |
Membership of an equivalence class in a quotient set. (Contributed by
set.mm contributors, 30-Jul-1995.) (Revised by set.mm contributors,
21-Mar-2007.)
|
    ![]](rbrack.gif)
       |
|
Theorem | qsdisj 5996 |
Members of a quotient set do not overlap. (Contributed by Rodolfo
Medina, 12-Oct-2010.) (Revised by Mario Carneiro, 11-Jul-2014.)
|
 Er               

    |
|
Theorem | ecoptocl 5997* |
Implicit substitution of class for equivalence class of ordered pair.
(Contributed by set.mm contributors, 23-Jul-1995.)
|
            ![]](rbrack.gif)           |
|
Theorem | 2ecoptocl 5998* |
Implicit substitution of classes for equivalence classes of ordered
pairs. (Contributed by set.mm contributors, 23-Jul-1995.)
|
            ![]](rbrack.gif)          ![]](rbrack.gif)                 |
|
Theorem | 3ecoptocl 5999* |
Implicit substitution of classes for equivalence classes of ordered
pairs. (Contributed by set.mm contributors, 9-Aug-1995.)
|
            ![]](rbrack.gif)          ![]](rbrack.gif)          ![]](rbrack.gif)                   |
|
2.4.3 The mapping operation
|
|
Syntax | cmap 6000 |
Extend the definition of a class to include the mapping operation. (Read
for , "the set of all functions that
map from to
.)
|
 |