Theorem List for Intuitionistic Logic Explorer - 4001-4100 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | opelopabaf 4001* |
The law of concretion. Theorem 9.5 of [Quine] p.
61. This version of
opelopab 3999 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 4002* |
The law of concretion. Theorem 9.5 of [Quine] p.
61. This version of
opelopab 3999 uses bound-variable hypotheses in place of
distinct variable
conditions." (Contributed by NM, 19-Dec-2008.)
|
                       |
|
Theorem | ssopab2 4003 |
Equivalence of ordered pair abstraction subclass and implication.
(Contributed by NM, 27-Dec-1996.) (Revised by Mario Carneiro,
19-May-2013.)
|
                   |
|
Theorem | ssopab2b 4004 |
Equivalence of ordered pair abstraction subclass and implication.
(Contributed by NM, 27-Dec-1996.) (Proof shortened by Mario Carneiro,
18-Nov-2016.)
|
                   |
|
Theorem | ssopab2i 4005 |
Inference of ordered pair abstraction subclass from implication.
(Contributed by NM, 5-Apr-1995.)
|
             |
|
Theorem | ssopab2dv 4006* |
Inference of ordered pair abstraction subclass from implication.
(Contributed by NM, 19-Jan-2014.) (Revised by Mario Carneiro,
24-Jun-2014.)
|
                 |
|
Theorem | eqopab2b 4007 |
Equivalence of ordered pair abstraction equality and biconditional.
(Contributed by Mario Carneiro, 4-Jan-2017.)
|
                   |
|
Theorem | opabm 4008* |
Inhabited ordered pair class abstraction. (Contributed by Jim Kingdon,
29-Sep-2018.)
|
             |
|
Theorem | iunopab 4009* |
Move indexed union inside an ordered-pair abstraction. (Contributed by
Stefan O'Rear, 20-Feb-2015.)
|

            |
|
2.3.5 Power class of union and
intersection
|
|
Theorem | pwin 4010 |
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 4011 |
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 4012 |
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 4013 |
Break up the power class of a union into a union of smaller classes.
(Contributed by Jim Kingdon, 30-Sep-2018.)
|
        
    |
|
Theorem | pwunim 4014 |
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.6 Epsilon and identity
relations
|
|
Syntax | cep 4015 |
Extend class notation to include the epsilon relation.
|
 |
|
Syntax | cid 4016 |
Extend the definition of a class to include identity relation.
|
 |
|
Definition | df-eprel 4017* |
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 4018. Thus, 5 { 1 , 5 }. (Contributed by NM,
13-Aug-1995.)
|
      |
|
Theorem | epelg 4018 |
The epsilon relation and membership are the same. General version of
epel 4020. (Contributed by Scott Fenton, 27-Mar-2011.)
(Revised by Mario
Carneiro, 28-Apr-2015.)
|
     |
|
Theorem | epelc 4019 |
The epsilon relationship and the membership relation are the same.
(Contributed by Scott Fenton, 11-Apr-2012.)
|
   |
|
Theorem | epel 4020 |
The epsilon relation and the membership relation are the same.
(Contributed by NM, 13-Aug-1995.)
|
   |
|
Definition | df-id 4021* |
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.7 Partial and complete ordering
|
|
Syntax | wpo 4022 |
Extend wff notation to include the strict partial ordering predicate.
Read: ' is a
partial order on .'
|
 |
|
Syntax | wor 4023 |
Extend wff notation to include the strict linear ordering predicate.
Read: ' orders
.'
|
 |
|
Definition | df-po 4024* |
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 4025* |
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 4026 |
Subset theorem for the partial ordering predicate. (Contributed by NM,
27-Mar-1997.) (Proof shortened by Mario Carneiro, 18-Nov-2016.)
|
     |
|
Theorem | poeq1 4027 |
Equality theorem for partial ordering predicate. (Contributed by NM,
27-Mar-1997.)
|
     |
|
Theorem | poeq2 4028 |
Equality theorem for partial ordering predicate. (Contributed by NM,
27-Mar-1997.)
|
     |
|
Theorem | nfpo 4029 |
Bound-variable hypothesis builder for partial orders. (Contributed by
Stefan O'Rear, 20-Jan-2015.)
|
      |
|
Theorem | nfso 4030 |
Bound-variable hypothesis builder for total orders. (Contributed by
Stefan O'Rear, 20-Jan-2015.)
|
      |
|
Theorem | pocl 4031 |
Properties of partial order relation in class notation. (Contributed by
NM, 27-Mar-1997.)
|
                     |
|
Theorem | ispod 4032* |
Sufficient conditions for a partial order. (Contributed by NM,
9-Jul-2014.)
|
                         |
|
Theorem | swopolem 4033* |
Perform the substitutions into the strict weak ordering law.
(Contributed by Mario Carneiro, 31-Dec-2014.)
|
                  
              |
|
Theorem | swopo 4034* |
A strict weak order is a partial order. (Contributed by Mario Carneiro,
9-Jul-2014.)
|
                               |
|
Theorem | poirr 4035 |
A partial order relation is irreflexive. (Contributed by NM,
27-Mar-1997.)
|
       |
|
Theorem | potr 4036 |
A partial order relation is a transitive relation. (Contributed by NM,
27-Mar-1997.)
|
                 |
|
Theorem | po2nr 4037 |
A partial order relation has no 2-cycle loops. (Contributed by NM,
27-Mar-1997.)
|
    
        |
|
Theorem | po3nr 4038 |
A partial order relation has no 3-cycle loops. (Contributed by NM,
27-Mar-1997.)
|
         
     |
|
Theorem | po0 4039 |
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 4040* |
A function preserves a partial order relation. (Contributed by Jeff
Madsen, 18-Jun-2011.)
|
           
   |
|
Theorem | sopo 4041 |
A strict linear order is a strict partial order. (Contributed by NM,
28-Mar-1997.)
|
   |
|
Theorem | soss 4042 |
Subset theorem for the strict ordering predicate. (Contributed by NM,
16-Mar-1997.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
|
     |
|
Theorem | soeq1 4043 |
Equality theorem for the strict ordering predicate. (Contributed by NM,
16-Mar-1997.)
|
     |
|
Theorem | soeq2 4044 |
Equality theorem for the strict ordering predicate. (Contributed by NM,
16-Mar-1997.)
|
     |
|
Theorem | sonr 4045 |
A strict order relation is irreflexive. (Contributed by NM,
24-Nov-1995.)
|
       |
|
Theorem | sotr 4046 |
A strict order relation is a transitive relation. (Contributed by NM,
21-Jan-1996.)
|
                 |
|
Theorem | issod 4047* |
An irreflexive, transitive, trichotomous relation is a linear ordering
(in the sense of df-iso 4025). (Contributed by NM, 21-Jan-1996.)
(Revised by Mario Carneiro, 9-Jul-2014.)
|
         
       |
|
Theorem | sowlin 4048 |
A strict order relation satisfies weak linearity. (Contributed by Jim
Kingdon, 6-Oct-2018.)
|
                 |
|
Theorem | so2nr 4049 |
A strict order relation has no 2-cycle loops. (Contributed by NM,
21-Jan-1996.)
|
    
        |
|
Theorem | so3nr 4050 |
A strict order relation has no 3-cycle loops. (Contributed by NM,
21-Jan-1996.)
|
         
     |
|
Theorem | sotricim 4051 |
One direction of sotritric 4052 holds for all weakly linear orders.
(Contributed by Jim Kingdon, 28-Sep-2019.)
|
    
   
      |
|
Theorem | sotritric 4052 |
A trichotomy relationship, given a trichotomous order. (Contributed by
Jim Kingdon, 28-Sep-2019.)
|
 
                     |
|
Theorem | sotritrieq 4053 |
A trichotomy relationship, given a trichotomous order. (Contributed by
Jim Kingdon, 13-Dec-2019.)
|
 
                     |
|
Theorem | so0 4054 |
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.8 Set-like relations
|
|
Syntax | wse 4055 |
Extend wff notation to include the set-like predicate. Read: ' is
set-like on .'
|
Se  |
|
Definition | df-se 4056* |
Define the set-like predicate. (Contributed by Mario Carneiro,
19-Nov-2014.)
|
 Se  
     |
|
Theorem | seex 4057* |
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 4058 |
Any relation on a set is set-like on it. (Contributed by Mario
Carneiro, 22-Jun-2015.)
|
 Se   |
|
Theorem | sess1 4059 |
Subset theorem for the set-like predicate. (Contributed by Mario
Carneiro, 24-Jun-2015.)
|
  Se Se    |
|
Theorem | sess2 4060 |
Subset theorem for the set-like predicate. (Contributed by Mario
Carneiro, 24-Jun-2015.)
|
  Se Se    |
|
Theorem | seeq1 4061 |
Equality theorem for the set-like predicate. (Contributed by Mario
Carneiro, 24-Jun-2015.)
|
  Se Se    |
|
Theorem | seeq2 4062 |
Equality theorem for the set-like predicate. (Contributed by Mario
Carneiro, 24-Jun-2015.)
|
  Se Se    |
|
Theorem | nfse 4063 |
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 4064 |
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  |
|
2.3.9 Ordinals
|
|
Syntax | word 4065 |
Extend the definition of a wff to include the ordinal predicate.
|
 |
|
Syntax | con0 4066 |
Extend the definition of a class to include the class of all ordinal
numbers. (The 0 in the name prevents creating a file called con.html,
which causes problems in Windows.)
|
 |
|
Syntax | wlim 4067 |
Extend the definition of a wff to include the limit ordinal predicate.
|
 |
|
Syntax | csuc 4068 |
Extend class notation to include the successor function.
|
 |
|
Definition | df-iord 4069* |
Define the ordinal predicate, which is true for a class that is
transitive and whose elements are transitive. Definition of ordinal in
[Crosilla], p. "Set-theoretic
principles incompatible with
intuitionistic logic". (Contributed by Jim Kingdon, 10-Oct-2018.)
Use
its alias dford3 4070 instead for naming consistency with set.mm.
(New usage is discouraged.)
|
      |
|
Theorem | dford3 4070* |
Alias for df-iord 4069. Use it instead of df-iord 4069 for naming
consistency with set.mm. (Contributed by Jim Kingdon, 10-Oct-2018.)
|
      |
|
Definition | df-on 4071 |
Define the class of all ordinal numbers. Definition 7.11 of
[TakeutiZaring] p. 38. (Contributed
by NM, 5-Jun-1994.)
|
   |
|
Definition | df-ilim 4072 |
Define the limit ordinal predicate, which is true for an ordinal that has
the empty set as an element and is not a successor (i.e. that is the union
of itself). Our definition combines the definition of Lim of
[BellMachover] p. 471 and Exercise 1
of [TakeutiZaring] p. 42, and then
changes to (which would be equivalent given the
law of the excluded middle, but which is not for us). (Contributed by Jim
Kingdon, 11-Nov-2018.) Use its alias dflim2 4073 instead for naming
consistency with set.mm. (New usage is discouraged.)
|
 
    |
|
Theorem | dflim2 4073 |
Alias for df-ilim 4072. Use it instead of df-ilim 4072 for naming consistency
with set.mm. (Contributed by NM, 4-Nov-2004.)
|
 
    |
|
Definition | df-suc 4074 |
Define the successor of a class. When applied to an ordinal number, the
successor means the same thing as "plus 1". Definition 7.22 of
[TakeutiZaring] p. 41, who use
"+ 1" to denote this function. Our
definition is a generalization to classes. Although it is not
conventional to use it with proper classes, it has no effect on a proper
class (sucprc 4115). Some authors denote the successor
operation with a
prime (apostrophe-like) symbol, such as Definition 6 of [Suppes] p. 134
and the definition of successor in [Mendelson] p. 246 (who uses the symbol
"Suc" as a predicate to mean "is a successor
ordinal"). The definition of
successor of [Enderton] p. 68 denotes the
operation with a plus-sign
superscript. (Contributed by NM, 30-Aug-1993.)
|
     |
|
Theorem | ordeq 4075 |
Equality theorem for the ordinal predicate. (Contributed by NM,
17-Sep-1993.)
|
     |
|
Theorem | elong 4076 |
An ordinal number is an ordinal set. (Contributed by NM,
5-Jun-1994.)
|
     |
|
Theorem | elon 4077 |
An ordinal number is an ordinal set. (Contributed by NM,
5-Jun-1994.)
|
   |
|
Theorem | eloni 4078 |
An ordinal number has the ordinal property. (Contributed by NM,
5-Jun-1994.)
|
   |
|
Theorem | elon2 4079 |
An ordinal number is an ordinal set. (Contributed by NM, 8-Feb-2004.)
|
 
   |
|
Theorem | limeq 4080 |
Equality theorem for the limit predicate. (Contributed by NM,
22-Apr-1994.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
|
     |
|
Theorem | ordtr 4081 |
An ordinal class is transitive. (Contributed by NM, 3-Apr-1994.)
|
   |
|
Theorem | ordelss 4082 |
An element of an ordinal class is a subset of it. (Contributed by NM,
30-May-1994.)
|
     |
|
Theorem | trssord 4083 |
A transitive subclass of an ordinal class is ordinal. (Contributed by
NM, 29-May-1994.)
|
     |
|
Theorem | ordelord 4084 |
An element of an ordinal class is ordinal. Proposition 7.6 of
[TakeutiZaring] p. 36.
(Contributed by NM, 23-Apr-1994.)
|
     |
|
Theorem | tron 4085 |
The class of all ordinal numbers is transitive. (Contributed by NM,
4-May-2009.)
|
 |
|
Theorem | ordelon 4086 |
An element of an ordinal class is an ordinal number. (Contributed by NM,
26-Oct-2003.)
|
     |
|
Theorem | onelon 4087 |
An element of an ordinal number is an ordinal number. Theorem 2.2(iii) of
[BellMachover] p. 469. (Contributed
by NM, 26-Oct-2003.)
|
     |
|
Theorem | ordin 4088 |
The intersection of two ordinal classes is ordinal. Proposition 7.9 of
[TakeutiZaring] p. 37. (Contributed
by NM, 9-May-1994.)
|
   
   |
|
Theorem | onin 4089 |
The intersection of two ordinal numbers is an ordinal number.
(Contributed by NM, 7-Apr-1995.)
|
       |
|
Theorem | onelss 4090 |
An element of an ordinal number is a subset of the number. (Contributed
by NM, 5-Jun-1994.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
|
 
   |
|
Theorem | ordtr1 4091 |
Transitive law for ordinal classes. (Contributed by NM, 12-Dec-2004.)
|
       |
|
Theorem | ontr1 4092 |
Transitive law for ordinal numbers. Theorem 7M(b) of [Enderton] p. 192.
(Contributed by NM, 11-Aug-1994.)
|
       |
|
Theorem | onintss 4093* |
If a property is true for an ordinal number, then the minimum ordinal
number for which it is true is smaller or equal. Theorem Schema 61 of
[Suppes] p. 228. (Contributed by NM,
3-Oct-2003.)
|
        
   |
|
Theorem | ord0 4094 |
The empty set is an ordinal class. (Contributed by NM, 11-May-1994.)
|
 |
|
Theorem | 0elon 4095 |
The empty set is an ordinal number. Corollary 7N(b) of [Enderton]
p. 193. (Contributed by NM, 17-Sep-1993.)
|
 |
|
Theorem | inton 4096 |
The intersection of the class of ordinal numbers is the empty set.
(Contributed by NM, 20-Oct-2003.)
|

 |
|
Theorem | nlim0 4097 |
The empty set is not a limit ordinal. (Contributed by NM, 24-Mar-1995.)
(Proof shortened by Andrew Salmon, 25-Jul-2011.)
|
 |
|
Theorem | limord 4098 |
A limit ordinal is ordinal. (Contributed by NM, 4-May-1995.)
|
   |
|
Theorem | limuni 4099 |
A limit ordinal is its own supremum (union). (Contributed by NM,
4-May-1995.)
|
    |
|
Theorem | limuni2 4100 |
The union of a limit ordinal is a limit ordinal. (Contributed by NM,
19-Sep-2006.)
|
    |