Theorem List for Intuitionistic Logic Explorer - 4101-4200 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | opcom 4101 |
An ordered pair commutes iff its members are equal. (Contributed by NM,
28-May-2009.)
|
      
  |
|
Theorem | moop2 4102* |
"At most one" property of an ordered pair. (Contributed by NM,
11-Apr-2004.) (Revised by Mario Carneiro, 26-Apr-2015.)
|
     |
|
Theorem | opeqsn 4103 |
Equivalence for an ordered pair equal to a singleton. (Contributed by
NM, 3-Jun-2008.)
|
            |
|
Theorem | opeqpr 4104 |
Equivalence for an ordered pair equal to an unordered pair.
(Contributed by NM, 3-Jun-2008.)
|
      
          
       |
|
Theorem | euotd 4105* |
Prove existential uniqueness for an ordered triple. (Contributed by
Mario Carneiro, 20-May-2015.)
|
        
                
   |
|
Theorem | uniop 4106 |
The union of an ordered pair. Theorem 65 of [Suppes] p. 39.
(Contributed by NM, 17-Aug-2004.) (Revised by Mario Carneiro,
26-Apr-2015.)
|
        |
|
Theorem | uniopel 4107 |
Ordered pair membership is inherited by class union. (Contributed by
NM, 13-May-2008.) (Revised by Mario Carneiro, 26-Apr-2015.)
|
           |
|
2.3.5 Ordered-pair class abstractions
(cont.)
|
|
Theorem | opabid 4108 |
The law of concretion. Special case of Theorem 9.5 of [Quine] p. 61.
(Contributed by NM, 14-Apr-1995.) (Proof shortened by Andrew Salmon,
25-Jul-2011.)
|
           |
|
Theorem | elopab 4109* |
Membership in a class abstraction of pairs. (Contributed by NM,
24-Mar-1998.)
|
     
           |
|
Theorem | opelopabsbALT 4110* |
The law of concretion in terms of substitutions. Less general than
opelopabsb 4111, but having a much shorter proof.
(Contributed by NM,
30-Sep-2002.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
(New usage is discouraged.) (Proof modification is discouraged.)
|
           ![] ]](rbrack.gif)   ![] ]](rbrack.gif)   |
|
Theorem | opelopabsb 4111* |
The law of concretion in terms of substitutions. (Contributed by NM,
30-Sep-2002.) (Revised by Mario Carneiro, 18-Nov-2016.)
|
           ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)   |
|
Theorem | brabsb 4112* |
The law of concretion in terms of substitutions. (Contributed by NM,
17-Mar-2008.)
|
          ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)   |
|
Theorem | opelopabt 4113* |
Closed theorem form of opelopab 4122. (Contributed by NM,
19-Feb-2013.)
|
      
  
    
  
               |
|
Theorem | opelopabga 4114* |
The law of concretion. Theorem 9.5 of [Quine] p.
61. (Contributed by
Mario Carneiro, 19-Dec-2013.)
|
                     |
|
Theorem | brabga 4115* |
The law of concretion for a binary relation. (Contributed by Mario
Carneiro, 19-Dec-2013.)
|
                    |
|
Theorem | opelopab2a 4116* |
Ordered pair membership in an ordered pair class abstraction.
(Contributed by Mario Carneiro, 19-Dec-2013.)
|
                         |
|
Theorem | opelopaba 4117* |
The law of concretion. Theorem 9.5 of [Quine] p.
61. (Contributed by
Mario Carneiro, 19-Dec-2013.)
|
                 |
|
Theorem | braba 4118* |
The law of concretion for a binary relation. (Contributed by NM,
19-Dec-2013.)
|
                |
|
Theorem | opelopabg 4119* |
The law of concretion. Theorem 9.5 of [Quine] p.
61. (Contributed by
NM, 28-May-1995.) (Revised by Mario Carneiro, 19-Dec-2013.)
|
                       |
|
Theorem | brabg 4120* |
The law of concretion for a binary relation. (Contributed by NM,
16-Aug-1999.) (Revised by Mario Carneiro, 19-Dec-2013.)
|
                      |
|
Theorem | opelopab2 4121* |
Ordered pair membership in an ordered pair class abstraction.
(Contributed by NM, 14-Oct-2007.) (Revised by Mario Carneiro,
19-Dec-2013.)
|
                           |
|
Theorem | opelopab 4122* |
The law of concretion. Theorem 9.5 of [Quine] p.
61. (Contributed by
NM, 16-May-1995.)
|

   
              |
|
Theorem | brab 4123* |
The law of concretion for a binary relation. (Contributed by NM,
16-Aug-1999.)
|

   
             |
|
Theorem | opelopabaf 4124* |
The law of concretion. Theorem 9.5 of [Quine] p.
61. This version of
opelopab 4122 uses bound-variable hypotheses in place of
distinct variable
conditions." (Contributed by Mario Carneiro, 19-Dec-2013.) (Proof
shortened by Mario Carneiro, 18-Nov-2016.)
|
                     |
|
Theorem | opelopabf 4125* |
The law of concretion. Theorem 9.5 of [Quine] p.
61. This version of
opelopab 4122 uses bound-variable hypotheses in place of
distinct variable
conditions." (Contributed by NM, 19-Dec-2008.)
|
    
   
              |
|
Theorem | ssopab2 4126 |
Equivalence of ordered pair abstraction subclass and implication.
(Contributed by NM, 27-Dec-1996.) (Revised by Mario Carneiro,
19-May-2013.)
|
      
            |
|
Theorem | ssopab2b 4127 |
Equivalence of ordered pair abstraction subclass and implication.
(Contributed by NM, 27-Dec-1996.) (Proof shortened by Mario Carneiro,
18-Nov-2016.)
|
               
   |
|
Theorem | ssopab2i 4128 |
Inference of ordered pair abstraction subclass from implication.
(Contributed by NM, 5-Apr-1995.)
|
             |
|
Theorem | ssopab2dv 4129* |
Inference of ordered pair abstraction subclass from implication.
(Contributed by NM, 19-Jan-2014.) (Revised by Mario Carneiro,
24-Jun-2014.)
|
                 |
|
Theorem | eqopab2b 4130 |
Equivalence of ordered pair abstraction equality and biconditional.
(Contributed by Mario Carneiro, 4-Jan-2017.)
|
               
   |
|
Theorem | opabm 4131* |
Inhabited ordered pair class abstraction. (Contributed by Jim Kingdon,
29-Sep-2018.)
|
             |
|
Theorem | iunopab 4132* |
Move indexed union inside an ordered-pair abstraction. (Contributed by
Stefan O'Rear, 20-Feb-2015.)
|

            |
|
2.3.6 Power class of union and
intersection
|
|
Theorem | pwin 4133 |
The power class of the intersection of two classes is the intersection
of their power classes. Exercise 4.12(j) of [Mendelson] p. 235.
(Contributed by NM, 23-Nov-2003.)
|
        |
|
Theorem | pwunss 4134 |
The power class of the union of two classes includes the union of their
power classes. Exercise 4.12(k) of [Mendelson] p. 235. (Contributed by
NM, 23-Nov-2003.)
|
        |
|
Theorem | pwssunim 4135 |
The power class of the union of two classes is a subset of the union of
their power classes, if one class is a subclass of the other. One
direction of Exercise 4.12(l) of [Mendelson] p. 235. (Contributed by
Jim Kingdon, 30-Sep-2018.)
|
     
      |
|
Theorem | pwundifss 4136 |
Break up the power class of a union into a union of smaller classes.
(Contributed by Jim Kingdon, 30-Sep-2018.)
|
        
    |
|
Theorem | pwunim 4137 |
The power class of the union of two classes equals the union of their
power classes, iff one class is a subclass of the other. Part of Exercise
7(b) of [Enderton] p. 28. (Contributed
by Jim Kingdon, 30-Sep-2018.)
|
     
 
    |
|
2.3.7 Epsilon and identity
relations
|
|
Syntax | cep 4138 |
Extend class notation to include the epsilon relation.
|
 |
|
Syntax | cid 4139 |
Extend the definition of a class to include identity relation.
|
 |
|
Definition | df-eprel 4140* |
Define the epsilon relation. Similar to Definition 6.22 of
[TakeutiZaring] p. 30. The
epsilon relation and set membership are the
same, that is,   when is a set by
epelg 4141. Thus, 5 { 1 , 5 }. (Contributed by NM,
13-Aug-1995.)
|
      |
|
Theorem | epelg 4141 |
The epsilon relation and membership are the same. General version of
epel 4143. (Contributed by Scott Fenton, 27-Mar-2011.)
(Revised by Mario
Carneiro, 28-Apr-2015.)
|
     |
|
Theorem | epelc 4142 |
The epsilon relationship and the membership relation are the same.
(Contributed by Scott Fenton, 11-Apr-2012.)
|
   |
|
Theorem | epel 4143 |
The epsilon relation and the membership relation are the same.
(Contributed by NM, 13-Aug-1995.)
|
   |
|
Definition | df-id 4144* |
Define the identity relation. Definition 9.15 of [Quine] p. 64. For
example, 5 5
and 4 5. (Contributed by NM,
13-Aug-1995.)
|
      |
|
2.3.8 Partial and complete ordering
|
|
Syntax | wpo 4145 |
Extend wff notation to include the strict partial ordering predicate.
Read: ' is a
partial order on .'
|
 |
|
Syntax | wor 4146 |
Extend wff notation to include the strict linear ordering predicate.
Read: ' orders
.'
|
 |
|
Definition | df-po 4147* |
Define the strict partial order predicate. Definition of [Enderton]
p. 168. The expression means is a partial order on
. (Contributed
by NM, 16-Mar-1997.)
|
  
   
             |
|
Definition | df-iso 4148* |
Define the strict linear order predicate. The expression
is
true if relationship orders .
The property
        is called
weak linearity by Proposition
11.2.3 of [HoTT], p. (varies). If we
assumed excluded middle, it would
be equivalent to trichotomy,     . (Contributed
by NM, 21-Jan-1996.) (Revised by Jim Kingdon, 4-Oct-2018.)
|
   
   
  
       |
|
Theorem | poss 4149 |
Subset theorem for the partial ordering predicate. (Contributed by NM,
27-Mar-1997.) (Proof shortened by Mario Carneiro, 18-Nov-2016.)
|
     |
|
Theorem | poeq1 4150 |
Equality theorem for partial ordering predicate. (Contributed by NM,
27-Mar-1997.)
|
     |
|
Theorem | poeq2 4151 |
Equality theorem for partial ordering predicate. (Contributed by NM,
27-Mar-1997.)
|
     |
|
Theorem | nfpo 4152 |
Bound-variable hypothesis builder for partial orders. (Contributed by
Stefan O'Rear, 20-Jan-2015.)
|
      |
|
Theorem | nfso 4153 |
Bound-variable hypothesis builder for total orders. (Contributed by
Stefan O'Rear, 20-Jan-2015.)
|
      |
|
Theorem | pocl 4154 |
Properties of partial order relation in class notation. (Contributed by
NM, 27-Mar-1997.)
|
                     |
|
Theorem | ispod 4155* |
Sufficient conditions for a partial order. (Contributed by NM,
9-Jul-2014.)
|
        
 
           
  |
|
Theorem | swopolem 4156* |
Perform the substitutions into the strict weak ordering law.
(Contributed by Mario Carneiro, 31-Dec-2014.)
|
  
 
  
          
 
  
         |
|
Theorem | swopo 4157* |
A strict weak order is a partial order. (Contributed by Mario Carneiro,
9-Jul-2014.)
|
  
 
  
      
 
  
           |
|
Theorem | poirr 4158 |
A partial order relation is irreflexive. (Contributed by NM,
27-Mar-1997.)
|
  
    |
|
Theorem | potr 4159 |
A partial order relation is a transitive relation. (Contributed by NM,
27-Mar-1997.)
|
    
            |
|
Theorem | po2nr 4160 |
A partial order relation has no 2-cycle loops. (Contributed by NM,
27-Mar-1997.)
|
    
        |
|
Theorem | po3nr 4161 |
A partial order relation has no 3-cycle loops. (Contributed by NM,
27-Mar-1997.)
|
    
    
     |
|
Theorem | po0 4162 |
Any relation is a partial ordering of the empty set. (Contributed by
NM, 28-Mar-1997.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
|
 |
|
Theorem | pofun 4163* |
A function preserves a partial order relation. (Contributed by Jeff
Madsen, 18-Jun-2011.)
|
       
       |
|
Theorem | sopo 4164 |
A strict linear order is a strict partial order. (Contributed by NM,
28-Mar-1997.)
|
   |
|
Theorem | soss 4165 |
Subset theorem for the strict ordering predicate. (Contributed by NM,
16-Mar-1997.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
|
     |
|
Theorem | soeq1 4166 |
Equality theorem for the strict ordering predicate. (Contributed by NM,
16-Mar-1997.)
|
     |
|
Theorem | soeq2 4167 |
Equality theorem for the strict ordering predicate. (Contributed by NM,
16-Mar-1997.)
|
     |
|
Theorem | sonr 4168 |
A strict order relation is irreflexive. (Contributed by NM,
24-Nov-1995.)
|
  
    |
|
Theorem | sotr 4169 |
A strict order relation is a transitive relation. (Contributed by NM,
21-Jan-1996.)
|
    
            |
|
Theorem | issod 4170* |
An irreflexive, transitive, trichotomous relation is a linear ordering
(in the sense of df-iso 4148). (Contributed by NM, 21-Jan-1996.)
(Revised by Mario Carneiro, 9-Jul-2014.)
|
    
 
  
       |
|
Theorem | sowlin 4171 |
A strict order relation satisfies weak linearity. (Contributed by Jim
Kingdon, 6-Oct-2018.)
|
    
  
         |
|
Theorem | so2nr 4172 |
A strict order relation has no 2-cycle loops. (Contributed by NM,
21-Jan-1996.)
|
    
        |
|
Theorem | so3nr 4173 |
A strict order relation has no 3-cycle loops. (Contributed by NM,
21-Jan-1996.)
|
    
    
     |
|
Theorem | sotricim 4174 |
One direction of sotritric 4175 holds for all weakly linear orders.
(Contributed by Jim Kingdon, 28-Sep-2019.)
|
    
   
      |
|
Theorem | sotritric 4175 |
A trichotomy relationship, given a trichotomous order. (Contributed by
Jim Kingdon, 28-Sep-2019.)
|
                       |
|
Theorem | sotritrieq 4176 |
A trichotomy relationship, given a trichotomous order. (Contributed by
Jim Kingdon, 13-Dec-2019.)
|
                       |
|
Theorem | so0 4177 |
Any relation is a strict ordering of the empty set. (Contributed by NM,
16-Mar-1997.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
|
 |
|
2.3.9 Founded and set-like
relations
|
|
Syntax | wfrfor 4178 |
Extend wff notation to include the well-founded predicate.
|
FrFor    |
|
Syntax | wfr 4179 |
Extend wff notation to include the well-founded predicate. Read: '
is a well-founded relation on .'
|
 |
|
Syntax | wse 4180 |
Extend wff notation to include the set-like predicate. Read: ' is
set-like on .'
|
Se  |
|
Syntax | wwe 4181 |
Extend wff notation to include the well-ordering predicate. Read:
' well-orders
.'
|
 |
|
Definition | df-frfor 4182* |
Define the well-founded relation predicate where might be a proper
class. By passing in we allow it potentially to be a proper class
rather than a set. (Contributed by Jim Kingdon and Mario Carneiro,
22-Sep-2021.)
|
FrFor         
     |
|
Definition | df-frind 4183* |
Define the well-founded relation predicate. In the presence of excluded
middle, there are a variety of equivalent ways to define this. In our
case, this definition, in terms of an inductive principle, works better
than one along the lines of "there is an element which is minimal
when A
is ordered by R". Because is constrained to be a set (not a
proper class) here, sometimes it may be necessary to use FrFor
directly rather than via . (Contributed by Jim Kingdon and Mario
Carneiro, 21-Sep-2021.)
|
  FrFor     |
|
Definition | df-se 4184* |
Define the set-like predicate. (Contributed by Mario Carneiro,
19-Nov-2014.)
|
 Se  
     |
|
Definition | df-wetr 4185* |
Define the well-ordering predicate. It is unusual to define
"well-ordering" in the absence of excluded middle, but we mean
an
ordering which is like the ordering which we have for ordinals (for
example, it does not entail trichotomy because ordinals don't have that
as seen at ordtriexmid 4366). Given excluded middle, well-ordering is
usually defined to require trichotomy (and the defintion of is
typically also different). (Contributed by Mario Carneiro and Jim
Kingdon, 23-Sep-2021.)
|
   
              |
|
Theorem | seex 4186* |
The -preimage of an
element of the base set in a set-like relation
is a set. (Contributed by Mario Carneiro, 19-Nov-2014.)
|
  Se        |
|
Theorem | exse 4187 |
Any relation on a set is set-like on it. (Contributed by Mario
Carneiro, 22-Jun-2015.)
|
 Se   |
|
Theorem | sess1 4188 |
Subset theorem for the set-like predicate. (Contributed by Mario
Carneiro, 24-Jun-2015.)
|
  Se Se    |
|
Theorem | sess2 4189 |
Subset theorem for the set-like predicate. (Contributed by Mario
Carneiro, 24-Jun-2015.)
|
  Se Se    |
|
Theorem | seeq1 4190 |
Equality theorem for the set-like predicate. (Contributed by Mario
Carneiro, 24-Jun-2015.)
|
  Se
Se    |
|
Theorem | seeq2 4191 |
Equality theorem for the set-like predicate. (Contributed by Mario
Carneiro, 24-Jun-2015.)
|
  Se
Se    |
|
Theorem | nfse 4192 |
Bound-variable hypothesis builder for set-like relations. (Contributed
by Mario Carneiro, 24-Jun-2015.) (Revised by Mario Carneiro,
14-Oct-2016.)
|
     Se  |
|
Theorem | epse 4193 |
The epsilon relation is set-like on any class. (This is the origin of
the term "set-like": a set-like relation "acts like"
the epsilon
relation of sets and their elements.) (Contributed by Mario Carneiro,
22-Jun-2015.)
|
Se  |
|
Theorem | frforeq1 4194 |
Equality theorem for the well-founded predicate. (Contributed by Jim
Kingdon, 22-Sep-2021.)
|
 FrFor   FrFor      |
|
Theorem | freq1 4195 |
Equality theorem for the well-founded predicate. (Contributed by NM,
9-Mar-1997.)
|
     |
|
Theorem | frforeq2 4196 |
Equality theorem for the well-founded predicate. (Contributed by Jim
Kingdon, 22-Sep-2021.)
|
 FrFor   FrFor      |
|
Theorem | freq2 4197 |
Equality theorem for the well-founded predicate. (Contributed by NM,
3-Apr-1994.)
|
     |
|
Theorem | frforeq3 4198 |
Equality theorem for the well-founded predicate. (Contributed by Jim
Kingdon, 22-Sep-2021.)
|
 FrFor   FrFor      |
|
Theorem | nffrfor 4199 |
Bound-variable hypothesis builder for well-founded relations.
(Contributed by Stefan O'Rear, 20-Jan-2015.) (Revised by Mario
Carneiro, 14-Oct-2016.)
|
       FrFor
   |
|
Theorem | nffr 4200 |
Bound-variable hypothesis builder for well-founded relations.
(Contributed by Stefan O'Rear, 20-Jan-2015.) (Revised by Mario
Carneiro, 14-Oct-2016.)
|
      |