Type  Label  Description 
Statement 

Theorem  opelopabaf 4001* 
The law of concretion. Theorem 9.5 of [Quine] p.
61. This version of
opelopab 3999 uses boundvariable hypotheses in place of
distinct variable
conditions." (Contributed by Mario Carneiro, 19Dec2013.) (Proof
shortened by Mario Carneiro, 18Nov2016.)



Theorem  opelopabf 4002* 
The law of concretion. Theorem 9.5 of [Quine] p.
61. This version of
opelopab 3999 uses boundvariable hypotheses in place of
distinct variable
conditions." (Contributed by NM, 19Dec2008.)



Theorem  ssopab2 4003 
Equivalence of ordered pair abstraction subclass and implication.
(Contributed by NM, 27Dec1996.) (Revised by Mario Carneiro,
19May2013.)



Theorem  ssopab2b 4004 
Equivalence of ordered pair abstraction subclass and implication.
(Contributed by NM, 27Dec1996.) (Proof shortened by Mario Carneiro,
18Nov2016.)



Theorem  ssopab2i 4005 
Inference of ordered pair abstraction subclass from implication.
(Contributed by NM, 5Apr1995.)



Theorem  ssopab2dv 4006* 
Inference of ordered pair abstraction subclass from implication.
(Contributed by NM, 19Jan2014.) (Revised by Mario Carneiro,
24Jun2014.)



Theorem  eqopab2b 4007 
Equivalence of ordered pair abstraction equality and biconditional.
(Contributed by Mario Carneiro, 4Jan2017.)



Theorem  opabm 4008* 
Inhabited ordered pair class abstraction. (Contributed by Jim Kingdon,
29Sep2018.)



Theorem  iunopab 4009* 
Move indexed union inside an orderedpair abstraction. (Contributed by
Stefan O'Rear, 20Feb2015.)



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, 23Nov2003.)



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, 23Nov2003.)



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, 30Sep2018.)



Theorem  pwundifss 4013 
Break up the power class of a union into a union of smaller classes.
(Contributed by Jim Kingdon, 30Sep2018.)



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, 30Sep2018.)



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  dfeprel 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,
13Aug1995.)



Theorem  epelg 4018 
The epsilon relation and membership are the same. General version of
epel 4020. (Contributed by Scott Fenton, 27Mar2011.)
(Revised by Mario
Carneiro, 28Apr2015.)



Theorem  epelc 4019 
The epsilon relationship and the membership relation are the same.
(Contributed by Scott Fenton, 11Apr2012.)



Theorem  epel 4020 
The epsilon relation and the membership relation are the same.
(Contributed by NM, 13Aug1995.)



Definition  dfid 4021* 
Define the identity relation. Definition 9.15 of [Quine] p. 64. For
example, 5 5
and 4 5. (Contributed by NM,
13Aug1995.)



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  dfpo 4024* 
Define the strict partial order predicate. Definition of [Enderton]
p. 168. The expression means is a partial order on
.
(Contributed by NM, 16Mar1997.)



Definition  dfiso 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, 21Jan1996.) (Revised by Jim Kingdon, 4Oct2018.)



Theorem  poss 4026 
Subset theorem for the partial ordering predicate. (Contributed by NM,
27Mar1997.) (Proof shortened by Mario Carneiro, 18Nov2016.)



Theorem  poeq1 4027 
Equality theorem for partial ordering predicate. (Contributed by NM,
27Mar1997.)



Theorem  poeq2 4028 
Equality theorem for partial ordering predicate. (Contributed by NM,
27Mar1997.)



Theorem  nfpo 4029 
Boundvariable hypothesis builder for partial orders. (Contributed by
Stefan O'Rear, 20Jan2015.)



Theorem  nfso 4030 
Boundvariable hypothesis builder for total orders. (Contributed by
Stefan O'Rear, 20Jan2015.)



Theorem  pocl 4031 
Properties of partial order relation in class notation. (Contributed by
NM, 27Mar1997.)



Theorem  ispod 4032* 
Sufficient conditions for a partial order. (Contributed by NM,
9Jul2014.)



Theorem  swopolem 4033* 
Perform the substitutions into the strict weak ordering law.
(Contributed by Mario Carneiro, 31Dec2014.)



Theorem  swopo 4034* 
A strict weak order is a partial order. (Contributed by Mario Carneiro,
9Jul2014.)



Theorem  poirr 4035 
A partial order relation is irreflexive. (Contributed by NM,
27Mar1997.)



Theorem  potr 4036 
A partial order relation is a transitive relation. (Contributed by NM,
27Mar1997.)



Theorem  po2nr 4037 
A partial order relation has no 2cycle loops. (Contributed by NM,
27Mar1997.)



Theorem  po3nr 4038 
A partial order relation has no 3cycle loops. (Contributed by NM,
27Mar1997.)



Theorem  po0 4039 
Any relation is a partial ordering of the empty set. (Contributed by
NM, 28Mar1997.) (Proof shortened by Andrew Salmon, 25Jul2011.)



Theorem  pofun 4040* 
A function preserves a partial order relation. (Contributed by Jeff
Madsen, 18Jun2011.)



Theorem  sopo 4041 
A strict linear order is a strict partial order. (Contributed by NM,
28Mar1997.)



Theorem  soss 4042 
Subset theorem for the strict ordering predicate. (Contributed by NM,
16Mar1997.) (Proof shortened by Andrew Salmon, 25Jul2011.)



Theorem  soeq1 4043 
Equality theorem for the strict ordering predicate. (Contributed by NM,
16Mar1997.)



Theorem  soeq2 4044 
Equality theorem for the strict ordering predicate. (Contributed by NM,
16Mar1997.)



Theorem  sonr 4045 
A strict order relation is irreflexive. (Contributed by NM,
24Nov1995.)



Theorem  sotr 4046 
A strict order relation is a transitive relation. (Contributed by NM,
21Jan1996.)



Theorem  issod 4047* 
An irreflexive, transitive, trichotomous relation is a linear ordering
(in the sense of dfiso 4025). (Contributed by NM, 21Jan1996.)
(Revised by Mario Carneiro, 9Jul2014.)



Theorem  sowlin 4048 
A strict order relation satisfies weak linearity. (Contributed by Jim
Kingdon, 6Oct2018.)



Theorem  so2nr 4049 
A strict order relation has no 2cycle loops. (Contributed by NM,
21Jan1996.)



Theorem  so3nr 4050 
A strict order relation has no 3cycle loops. (Contributed by NM,
21Jan1996.)



Theorem  sotricim 4051 
One direction of sotritric 4052 holds for all weakly linear orders.
(Contributed by Jim Kingdon, 28Sep2019.)



Theorem  sotritric 4052 
A trichotomy relationship, given a trichotomous order. (Contributed by
Jim Kingdon, 28Sep2019.)



Theorem  sotritrieq 4053 
A trichotomy relationship, given a trichotomous order. (Contributed by
Jim Kingdon, 13Dec2019.)



Theorem  so0 4054 
Any relation is a strict ordering of the empty set. (Contributed by NM,
16Mar1997.) (Proof shortened by Andrew Salmon, 25Jul2011.)



2.3.8 Setlike relations


Syntax  wse 4055 
Extend wff notation to include the setlike predicate. Read: ' is
setlike on .'

Se 

Definition  dfse 4056* 
Define the setlike predicate. (Contributed by Mario Carneiro,
19Nov2014.)

Se


Theorem  seex 4057* 
The preimage of an
element of the base set in a setlike relation
is a set. (Contributed by Mario Carneiro, 19Nov2014.)

Se


Theorem  exse 4058 
Any relation on a set is setlike on it. (Contributed by Mario
Carneiro, 22Jun2015.)

Se 

Theorem  sess1 4059 
Subset theorem for the setlike predicate. (Contributed by Mario
Carneiro, 24Jun2015.)

Se Se 

Theorem  sess2 4060 
Subset theorem for the setlike predicate. (Contributed by Mario
Carneiro, 24Jun2015.)

Se Se 

Theorem  seeq1 4061 
Equality theorem for the setlike predicate. (Contributed by Mario
Carneiro, 24Jun2015.)

Se Se 

Theorem  seeq2 4062 
Equality theorem for the setlike predicate. (Contributed by Mario
Carneiro, 24Jun2015.)

Se Se 

Theorem  nfse 4063 
Boundvariable hypothesis builder for setlike relations. (Contributed
by Mario Carneiro, 24Jun2015.) (Revised by Mario Carneiro,
14Oct2016.)

Se 

Theorem  epse 4064 
The epsilon relation is setlike on any class. (This is the origin of
the term "setlike": a setlike relation "acts like"
the epsilon
relation of sets and their elements.) (Contributed by Mario Carneiro,
22Jun2015.)

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  dfiord 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. "Settheoretic
principles incompatible with
intuitionistic logic". (Contributed by Jim Kingdon, 10Oct2018.)
Use
its alias dford3 4070 instead for naming consistency with set.mm.
(New usage is discouraged.)



Theorem  dford3 4070* 
Alias for dfiord 4069. Use it instead of dfiord 4069 for naming
consistency with set.mm. (Contributed by Jim Kingdon, 10Oct2018.)



Definition  dfon 4071 
Define the class of all ordinal numbers. Definition 7.11 of
[TakeutiZaring] p. 38. (Contributed
by NM, 5Jun1994.)



Definition  dfilim 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, 11Nov2018.) Use its alias dflim2 4073 instead for naming
consistency with set.mm. (New usage is discouraged.)



Theorem  dflim2 4073 
Alias for dfilim 4072. Use it instead of dfilim 4072 for naming consistency
with set.mm. (Contributed by NM, 4Nov2004.)



Definition  dfsuc 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 (apostrophelike) 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 plussign
superscript. (Contributed by NM, 30Aug1993.)



Theorem  ordeq 4075 
Equality theorem for the ordinal predicate. (Contributed by NM,
17Sep1993.)



Theorem  elong 4076 
An ordinal number is an ordinal set. (Contributed by NM,
5Jun1994.)



Theorem  elon 4077 
An ordinal number is an ordinal set. (Contributed by NM,
5Jun1994.)



Theorem  eloni 4078 
An ordinal number has the ordinal property. (Contributed by NM,
5Jun1994.)



Theorem  elon2 4079 
An ordinal number is an ordinal set. (Contributed by NM, 8Feb2004.)



Theorem  limeq 4080 
Equality theorem for the limit predicate. (Contributed by NM,
22Apr1994.) (Proof shortened by Andrew Salmon, 25Jul2011.)



Theorem  ordtr 4081 
An ordinal class is transitive. (Contributed by NM, 3Apr1994.)



Theorem  ordelss 4082 
An element of an ordinal class is a subset of it. (Contributed by NM,
30May1994.)



Theorem  trssord 4083 
A transitive subclass of an ordinal class is ordinal. (Contributed by
NM, 29May1994.)



Theorem  ordelord 4084 
An element of an ordinal class is ordinal. Proposition 7.6 of
[TakeutiZaring] p. 36.
(Contributed by NM, 23Apr1994.)



Theorem  tron 4085 
The class of all ordinal numbers is transitive. (Contributed by NM,
4May2009.)



Theorem  ordelon 4086 
An element of an ordinal class is an ordinal number. (Contributed by NM,
26Oct2003.)



Theorem  onelon 4087 
An element of an ordinal number is an ordinal number. Theorem 2.2(iii) of
[BellMachover] p. 469. (Contributed
by NM, 26Oct2003.)



Theorem  ordin 4088 
The intersection of two ordinal classes is ordinal. Proposition 7.9 of
[TakeutiZaring] p. 37. (Contributed
by NM, 9May1994.)



Theorem  onin 4089 
The intersection of two ordinal numbers is an ordinal number.
(Contributed by NM, 7Apr1995.)



Theorem  onelss 4090 
An element of an ordinal number is a subset of the number. (Contributed
by NM, 5Jun1994.) (Proof shortened by Andrew Salmon, 25Jul2011.)



Theorem  ordtr1 4091 
Transitive law for ordinal classes. (Contributed by NM, 12Dec2004.)



Theorem  ontr1 4092 
Transitive law for ordinal numbers. Theorem 7M(b) of [Enderton] p. 192.
(Contributed by NM, 11Aug1994.)



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,
3Oct2003.)



Theorem  ord0 4094 
The empty set is an ordinal class. (Contributed by NM, 11May1994.)



Theorem  0elon 4095 
The empty set is an ordinal number. Corollary 7N(b) of [Enderton]
p. 193. (Contributed by NM, 17Sep1993.)



Theorem  inton 4096 
The intersection of the class of ordinal numbers is the empty set.
(Contributed by NM, 20Oct2003.)



Theorem  nlim0 4097 
The empty set is not a limit ordinal. (Contributed by NM, 24Mar1995.)
(Proof shortened by Andrew Salmon, 25Jul2011.)



Theorem  limord 4098 
A limit ordinal is ordinal. (Contributed by NM, 4May1995.)



Theorem  limuni 4099 
A limit ordinal is its own supremum (union). (Contributed by NM,
4May1995.)



Theorem  limuni2 4100 
The union of a limit ordinal is a limit ordinal. (Contributed by NM,
19Sep2006.)

