Type  Label  Description 
Statement 

Theorem  opcom 4101 
An ordered pair commutes iff its members are equal. (Contributed by NM,
28May2009.)



Theorem  moop2 4102* 
"At most one" property of an ordered pair. (Contributed by NM,
11Apr2004.) (Revised by Mario Carneiro, 26Apr2015.)



Theorem  opeqsn 4103 
Equivalence for an ordered pair equal to a singleton. (Contributed by
NM, 3Jun2008.)



Theorem  opeqpr 4104 
Equivalence for an ordered pair equal to an unordered pair.
(Contributed by NM, 3Jun2008.)



Theorem  euotd 4105* 
Prove existential uniqueness for an ordered triple. (Contributed by
Mario Carneiro, 20May2015.)



Theorem  uniop 4106 
The union of an ordered pair. Theorem 65 of [Suppes] p. 39.
(Contributed by NM, 17Aug2004.) (Revised by Mario Carneiro,
26Apr2015.)



Theorem  uniopel 4107 
Ordered pair membership is inherited by class union. (Contributed by
NM, 13May2008.) (Revised by Mario Carneiro, 26Apr2015.)



2.3.5 Orderedpair class abstractions
(cont.)


Theorem  opabid 4108 
The law of concretion. Special case of Theorem 9.5 of [Quine] p. 61.
(Contributed by NM, 14Apr1995.) (Proof shortened by Andrew Salmon,
25Jul2011.)



Theorem  elopab 4109* 
Membership in a class abstraction of pairs. (Contributed by NM,
24Mar1998.)



Theorem  opelopabsbALT 4110* 
The law of concretion in terms of substitutions. Less general than
opelopabsb 4111, but having a much shorter proof.
(Contributed by NM,
30Sep2002.) (Proof shortened by Andrew Salmon, 25Jul2011.)
(New usage is discouraged.) (Proof modification is discouraged.)



Theorem  opelopabsb 4111* 
The law of concretion in terms of substitutions. (Contributed by NM,
30Sep2002.) (Revised by Mario Carneiro, 18Nov2016.)



Theorem  brabsb 4112* 
The law of concretion in terms of substitutions. (Contributed by NM,
17Mar2008.)



Theorem  opelopabt 4113* 
Closed theorem form of opelopab 4122. (Contributed by NM,
19Feb2013.)



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



2.3.6 Power class of union and
intersection


Theorem  pwin 4133 
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 4134 
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 4135 
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 4136 
Break up the power class of a union into a union of smaller classes.
(Contributed by Jim Kingdon, 30Sep2018.)



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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

FrFor 

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



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

Se 

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



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

Se


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

Se 

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

Se 

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

Se Se 

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

Se Se 

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

Se
Se 

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

Se
Se 

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

Se 

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

FrFor FrFor 

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



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

FrFor FrFor 

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



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

FrFor FrFor 

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

FrFor


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

