Type  Label  Description 
Statement 

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



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



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



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



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



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



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



2.3.6 Power class of union and
intersection


Theorem  pwin 4208 
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 4209 
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 4210 
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 4211 
Break up the power class of a union into a union of smaller classes.
(Contributed by Jim Kingdon, 30Sep2018.)



Theorem  pwunim 4212 
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.7 Epsilon and identity
relations


Syntax  cep 4213 
Extend class notation to include the epsilon relation.



Syntax  cid 4214 
Extend the definition of a class to include identity relation.



Definition  dfeprel 4215* 
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 4216. Thus, 5 { 1 , 5 }. (Contributed by NM,
13Aug1995.)



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



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



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



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



2.3.8 Partial and complete ordering


Syntax  wpo 4220 
Extend wff notation to include the strict partial ordering predicate.
Read: ' is a
partial order on .'



Syntax  wor 4221 
Extend wff notation to include the strict linear ordering predicate.
Read: ' orders
.'



Definition  dfpo 4222* 
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 4223* 
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 4224 
Subset theorem for the partial ordering predicate. (Contributed by NM,
27Mar1997.) (Proof shortened by Mario Carneiro, 18Nov2016.)



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



Theorem  so0 4252 
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 4253 
Extend wff notation to include the wellfounded predicate.

FrFor 

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



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

Se 

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



Definition  dffrfor 4257* 
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 4258* 
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 4259* 
Define the setlike predicate. (Contributed by Mario Carneiro,
19Nov2014.)

Se


Definition  dfwetr 4260* 
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 do not have that
as seen at ordtriexmid 4441). Given excluded middle, wellordering is
usually defined to require trichotomy (and the definition of is
typically also different). (Contributed by Mario Carneiro and Jim
Kingdon, 23Sep2021.)



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

Se 

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

Se 

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

Se Se 

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

Se Se 

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

Se
Se 

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

Se
Se 

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

Se 

Theorem  epse 4268 
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 4269 
Equality theorem for the wellfounded predicate. (Contributed by Jim
Kingdon, 22Sep2021.)

FrFor FrFor 

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



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

FrFor FrFor 

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



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

FrFor FrFor 

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

FrFor


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



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



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



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



Theorem  efrirr 4279 
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 4280 
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 4281 
Boundvariable hypothesis builder for wellorderings. (Contributed by
Stefan O'Rear, 20Jan2015.) (Revised by Mario Carneiro,
14Oct2016.)



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



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



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



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



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



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



2.3.10 Ordinals


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



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



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



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



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



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



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



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



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



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



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

