Type  Label  Description 
Statement 

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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



2.3.9 Founded and setlike
relations


Syntax  wfrfor 4130 
Extend wff notation to include the wellfounded predicate.

FrFor 

Syntax  wfr 4131 
Extend wff notation to include the wellfounded predicate. Read: '
is a wellfounded relation on .'



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

Se 

Syntax  wwe 4133 
Extend wff notation to include the wellordering predicate. Read:
' wellorders
.'



Definition  dffrfor 4134* 
Define the wellfounded 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,
22Sep2021.)

FrFor


Definition  dffrind 4135* 
Define the wellfounded 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, 21Sep2021.)

FrFor 

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

Se


Definition  dfwetr 4137* 
Define the wellordering predicate. It is unusual to define
"wellordering" 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 4313). Given excluded middle, wellordering is
usually defined to require trichotomy (and the defintion of is
typically also different). (Contributed by Mario Carneiro and Jim
Kingdon, 23Sep2021.)



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

Se 

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

Se 

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

Se Se 

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

Se Se 

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

Se
Se 

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

Se
Se 

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

Se 

Theorem  epse 4145 
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 

Theorem  frforeq1 4146 
Equality theorem for the wellfounded predicate. (Contributed by Jim
Kingdon, 22Sep2021.)

FrFor FrFor 

Theorem  freq1 4147 
Equality theorem for the wellfounded predicate. (Contributed by NM,
9Mar1997.)



Theorem  frforeq2 4148 
Equality theorem for the wellfounded predicate. (Contributed by Jim
Kingdon, 22Sep2021.)

FrFor FrFor 

Theorem  freq2 4149 
Equality theorem for the wellfounded predicate. (Contributed by NM,
3Apr1994.)



Theorem  frforeq3 4150 
Equality theorem for the wellfounded predicate. (Contributed by Jim
Kingdon, 22Sep2021.)

FrFor FrFor 

Theorem  nffrfor 4151 
Boundvariable hypothesis builder for wellfounded relations.
(Contributed by Stefan O'Rear, 20Jan2015.) (Revised by Mario
Carneiro, 14Oct2016.)

FrFor


Theorem  nffr 4152 
Boundvariable hypothesis builder for wellfounded relations.
(Contributed by Stefan O'Rear, 20Jan2015.) (Revised by Mario
Carneiro, 14Oct2016.)



Theorem  frirrg 4153 
A wellfounded relation is irreflexive. This is the case where
exists. (Contributed by Jim Kingdon, 21Sep2021.)



Theorem  fr0 4154 
Any relation is wellfounded on the empty set. (Contributed by NM,
17Sep1993.)



Theorem  frind 4155* 
Induction over a wellfounded set. (Contributed by Jim Kingdon,
28Sep2021.)



Theorem  efrirr 4156 
Irreflexivity of the epsilon relation: a class founded by epsilon is not a
member of itself. (Contributed by NM, 18Apr1994.) (Revised by Mario
Carneiro, 22Jun2015.)



Theorem  tz7.2 4157 
Similar to Theorem 7.2 of [TakeutiZaring]
p. 35, of except that the Axiom
of Regularity is not required due to antecedent .
(Contributed by NM, 4May1994.)



Theorem  nfwe 4158 
Boundvariable hypothesis builder for wellorderings. (Contributed by
Stefan O'Rear, 20Jan2015.) (Revised by Mario Carneiro,
14Oct2016.)



Theorem  weeq1 4159 
Equality theorem for the wellordering predicate. (Contributed by NM,
9Mar1997.)



Theorem  weeq2 4160 
Equality theorem for the wellordering predicate. (Contributed by NM,
3Apr1994.)



Theorem  wefr 4161 
A wellordering is wellfounded. (Contributed by NM, 22Apr1994.)



Theorem  wepo 4162 
A wellordering is a partial ordering. (Contributed by Jim Kingdon,
23Sep2021.)



Theorem  wetrep 4163* 
An epsilon wellordering is a transitive relation. (Contributed by NM,
22Apr1994.)



Theorem  we0 4164 
Any relation is a wellordering of the empty set. (Contributed by NM,
16Mar1997.)



2.3.10 Ordinals


Syntax  word 4165 
Extend the definition of a wff to include the ordinal predicate.



Syntax  con0 4166 
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 4167 
Extend the definition of a wff to include the limit ordinal predicate.



Syntax  csuc 4168 
Extend class notation to include the successor function.



Definition  dfiord 4169* 
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 4170 instead for naming consistency with set.mm.
(New usage is discouraged.)



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



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



Definition  dfilim 4172 
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 4173 instead for naming
consistency with set.mm. (New usage is discouraged.)



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



Definition  dfsuc 4174 
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 4215). 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 4175 
Equality theorem for the ordinal predicate. (Contributed by NM,
17Sep1993.)



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



Theorem  onintss 4193* 
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 4194 
The empty set is an ordinal class. (Contributed by NM, 11May1994.)



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



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



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



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



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



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

