Type  Label  Description 
Statement 

Theorem  brabga 4001* 
The law of concretion for a binary relation. (Contributed by Mario
Carneiro, 19Dec2013.)



Theorem  opelopab2a 4002* 
Ordered pair membership in an ordered pair class abstraction.
(Contributed by Mario Carneiro, 19Dec2013.)



Theorem  opelopaba 4003* 
The law of concretion. Theorem 9.5 of [Quine] p.
61. (Contributed by
Mario Carneiro, 19Dec2013.)



Theorem  braba 4004* 
The law of concretion for a binary relation. (Contributed by NM,
19Dec2013.)



Theorem  opelopabg 4005* 
The law of concretion. Theorem 9.5 of [Quine] p.
61. (Contributed by
NM, 28May1995.) (Revised by Mario Carneiro, 19Dec2013.)



Theorem  brabg 4006* 
The law of concretion for a binary relation. (Contributed by NM,
16Aug1999.) (Revised by Mario Carneiro, 19Dec2013.)



Theorem  opelopab2 4007* 
Ordered pair membership in an ordered pair class abstraction.
(Contributed by NM, 14Oct2007.) (Revised by Mario Carneiro,
19Dec2013.)



Theorem  opelopab 4008* 
The law of concretion. Theorem 9.5 of [Quine] p.
61. (Contributed by
NM, 16May1995.)



Theorem  brab 4009* 
The law of concretion for a binary relation. (Contributed by NM,
16Aug1999.)



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



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



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



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



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



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



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



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



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



2.3.5 Power class of union and
intersection


Theorem  pwin 4019 
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 4020 
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 4021 
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 4022 
Break up the power class of a union into a union of smaller classes.
(Contributed by Jim Kingdon, 30Sep2018.)



Theorem  pwunim 4023 
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 4024 
Extend class notation to include the epsilon relation.



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



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



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



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



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



Definition  dfid 4030* 
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 4031 
Extend wff notation to include the strict partial ordering predicate.
Read: ' is a
partial order on .'



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



2.3.8 Founded and setlike
relations


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

FrFor 

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



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

Se 

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



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

Se


Definition  dfwetr 4071* 
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 4247). 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 4072* 
The preimage of an
element of the base set in a setlike relation
is a set. (Contributed by Mario Carneiro, 19Nov2014.)

Se 

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

Se 

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

Se Se 

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

Se Se 

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

Se
Se 

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

Se
Se 

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

Se 

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

FrFor FrFor 

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



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

FrFor FrFor 

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



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

FrFor FrFor 

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

FrFor


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



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



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



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



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



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



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



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



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



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



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



2.3.9 Ordinals


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



Syntax  con0 4100 
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.)

