Type  Label  Description 
Statement 

Theorem  opth1 4001 
Equality of the first members of equal ordered pairs. (Contributed by
NM, 28May2008.) (Revised by Mario Carneiro, 26Apr2015.)



Theorem  opth 4002 
The ordered pair theorem. If two ordered pairs are equal, their first
elements are equal and their second elements are equal. Exercise 6 of
[TakeutiZaring] p. 16. Note that
and are not required to be
sets due our specific ordered pair definition. (Contributed by NM,
28May1995.)



Theorem  opthg 4003 
Ordered pair theorem.
and are not required
to be sets under
our specific ordered pair definition. (Contributed by NM, 14Oct2005.)
(Revised by Mario Carneiro, 26Apr2015.)



Theorem  opthg2 4004 
Ordered pair theorem. (Contributed by NM, 14Oct2005.) (Revised by
Mario Carneiro, 26Apr2015.)



Theorem  opth2 4005 
Ordered pair theorem. (Contributed by NM, 21Sep2014.)



Theorem  otth2 4006 
Ordered triple theorem, with triple express with ordered pairs.
(Contributed by NM, 1May1995.) (Revised by Mario Carneiro,
26Apr2015.)



Theorem  otth 4007 
Ordered triple theorem. (Contributed by NM, 25Sep2014.) (Revised by
Mario Carneiro, 26Apr2015.)



Theorem  eqvinop 4008* 
A variable introduction law for ordered pairs. Analog of Lemma 15 of
[Monk2] p. 109. (Contributed by NM,
28May1995.)



Theorem  copsexg 4009* 
Substitution of class
for ordered pair .
(Contributed by NM, 27Dec1996.) (Revised by Andrew Salmon,
11Jul2011.)



Theorem  copsex2t 4010* 
Closed theorem form of copsex2g 4011. (Contributed by NM,
17Feb2013.)



Theorem  copsex2g 4011* 
Implicit substitution inference for ordered pairs. (Contributed by NM,
28May1995.)



Theorem  copsex4g 4012* 
An implicit substitution inference for 2 ordered pairs. (Contributed by
NM, 5Aug1995.)



Theorem  0nelop 4013 
A property of ordered pairs. (Contributed by Mario Carneiro,
26Apr2015.)



Theorem  opeqex 4014 
Equivalence of existence implied by equality of ordered pairs.
(Contributed by NM, 28May2008.)



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



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



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



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



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



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



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



2.3.4 Orderedpair class abstractions
(cont.)


Theorem  opabid 4022 
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 4023* 
Membership in a class abstraction of pairs. (Contributed by NM,
24Mar1998.)



Theorem  opelopabsbALT 4024* 
The law of concretion in terms of substitutions. Less general than
opelopabsb 4025, 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 4025* 
The law of concretion in terms of substitutions. (Contributed by NM,
30Sep2002.) (Revised by Mario Carneiro, 18Nov2016.)



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



2.3.5 Power class of union and
intersection


Theorem  pwin 4047 
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 4048 
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 4049 
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 4050 
Break up the power class of a union into a union of smaller classes.
(Contributed by Jim Kingdon, 30Sep2018.)



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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

FrFor 

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



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

Se 

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



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

Se


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

Se 