Type  Label  Description 
Statement 

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

⊢ Ⅎ𝑥𝜓
& ⊢ Ⅎ𝑦𝜓
& ⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓)) ⇒ ⊢ (⟨𝐴, 𝐵⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ 𝜓) 

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

⊢ Ⅎ𝑥𝜓
& ⊢ Ⅎ𝑦𝜒
& ⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (⟨𝐴, 𝐵⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ 𝜒) 

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

⊢ (∀𝑥∀𝑦(𝜑 → 𝜓) → {⟨𝑥, 𝑦⟩ ∣ 𝜑} ⊆ {⟨𝑥, 𝑦⟩ ∣ 𝜓}) 

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

⊢ ({⟨𝑥, 𝑦⟩ ∣ 𝜑} ⊆ {⟨𝑥, 𝑦⟩ ∣ 𝜓} ↔ ∀𝑥∀𝑦(𝜑 → 𝜓)) 

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

⊢ (𝜑 → 𝜓) ⇒ ⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ⊆ {⟨𝑥, 𝑦⟩ ∣ 𝜓} 

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

⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → {⟨𝑥, 𝑦⟩ ∣ 𝜓} ⊆ {⟨𝑥, 𝑦⟩ ∣ 𝜒}) 

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

⊢ ({⟨𝑥, 𝑦⟩ ∣ 𝜑} = {⟨𝑥, 𝑦⟩ ∣ 𝜓} ↔ ∀𝑥∀𝑦(𝜑 ↔ 𝜓)) 

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

⊢ (∃𝑧 𝑧 ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ ∃𝑥∃𝑦𝜑) 

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

⊢ ∪ 𝑧 ∈ 𝐴 {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧 ∈ 𝐴 𝜑} 

2.3.6 Power class of union and
intersection


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

⊢ ((𝒫 (𝐴 ∪ 𝐵) ∖ 𝒫 𝐴) ∪ 𝒫 𝐴) ⊆ 𝒫 (𝐴 ∪ 𝐵) 

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

class E 

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

class I 

Definition  dfeprel 4217* 
Define the epsilon relation. Similar to Definition 6.22 of
[TakeutiZaring] p. 30. The
epsilon relation and set membership are the
same, that is, (𝐴 E 𝐵 ↔ 𝐴 ∈ 𝐵) when 𝐵 is a set by
epelg 4218. Thus, 5 E { 1 , 5
}. (Contributed by NM,
13Aug1995.)

⊢ E = {⟨𝑥, 𝑦⟩ ∣ 𝑥 ∈ 𝑦} 

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

⊢ (𝐵 ∈ 𝑉 → (𝐴 E 𝐵 ↔ 𝐴 ∈ 𝐵)) 

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

⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴 E 𝐵 ↔ 𝐴 ∈ 𝐵) 

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

⊢ (𝑥 E 𝑦 ↔ 𝑥 ∈ 𝑦) 

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

⊢ I = {⟨𝑥, 𝑦⟩ ∣ 𝑥 = 𝑦} 

2.3.8 Partial and complete ordering


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

wff 𝑅 Po 𝐴 

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

wff 𝑅 Or 𝐴 

Definition  dfpo 4224* 
Define the strict partial order predicate. Definition of [Enderton]
p. 168. The expression 𝑅 Po 𝐴 means 𝑅 is a partial order on
𝐴. (Contributed by NM, 16Mar1997.)

⊢ (𝑅 Po 𝐴 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (¬ 𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧))) 

Definition  dfiso 4225* 
Define the strict linear order predicate. The expression 𝑅 Or 𝐴 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.)

⊢ (𝑅 Or 𝐴 ↔ (𝑅 Po 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (𝑥𝑅𝑦 → (𝑥𝑅𝑧 ∨ 𝑧𝑅𝑦)))) 

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

⊢ (𝐴 ⊆ 𝐵 → (𝑅 Po 𝐵 → 𝑅 Po 𝐴)) 

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

⊢ (𝑅 = 𝑆 → (𝑅 Po 𝐴 ↔ 𝑆 Po 𝐴)) 

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

⊢ (𝐴 = 𝐵 → (𝑅 Po 𝐴 ↔ 𝑅 Po 𝐵)) 

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

⊢ Ⅎ𝑥𝑅
& ⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥 𝑅 Po 𝐴 

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

⊢ Ⅎ𝑥𝑅
& ⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥 𝑅 Or 𝐴 

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

⊢ (𝑅 Po 𝐴 → ((𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴) → (¬ 𝐵𝑅𝐵 ∧ ((𝐵𝑅𝐶 ∧ 𝐶𝑅𝐷) → 𝐵𝑅𝐷)))) 

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

⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ¬ 𝑥𝑅𝑥)
& ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)) ⇒ ⊢ (𝜑 → 𝑅 Po 𝐴) 

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

⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → (𝑥𝑅𝑦 → (𝑥𝑅𝑧 ∨ 𝑧𝑅𝑦))) ⇒ ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ 𝑍 ∈ 𝐴)) → (𝑋𝑅𝑌 → (𝑋𝑅𝑍 ∨ 𝑍𝑅𝑌))) 

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

⊢ ((𝜑 ∧ (𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → (𝑦𝑅𝑧 → ¬ 𝑧𝑅𝑦))
& ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → (𝑥𝑅𝑦 → (𝑥𝑅𝑧 ∨ 𝑧𝑅𝑦))) ⇒ ⊢ (𝜑 → 𝑅 Po 𝐴) 

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

⊢ ((𝑅 Po 𝐴 ∧ 𝐵 ∈ 𝐴) → ¬ 𝐵𝑅𝐵) 

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

⊢ ((𝑅 Po 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → ((𝐵𝑅𝐶 ∧ 𝐶𝑅𝐷) → 𝐵𝑅𝐷)) 

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

⊢ ((𝑅 Po 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴)) → ¬ (𝐵𝑅𝐶 ∧ 𝐶𝑅𝐵)) 

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

⊢ ((𝑅 Po 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → ¬ (𝐵𝑅𝐶 ∧ 𝐶𝑅𝐷 ∧ 𝐷𝑅𝐵)) 

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

⊢ 𝑅 Po ∅ 

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

⊢ 𝑆 = {⟨𝑥, 𝑦⟩ ∣ 𝑋𝑅𝑌}
& ⊢ (𝑥 = 𝑦 → 𝑋 = 𝑌) ⇒ ⊢ ((𝑅 Po 𝐵 ∧ ∀𝑥 ∈ 𝐴 𝑋 ∈ 𝐵) → 𝑆 Po 𝐴) 

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

⊢ (𝑅 Or 𝐴 → 𝑅 Po 𝐴) 

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

⊢ (𝐴 ⊆ 𝐵 → (𝑅 Or 𝐵 → 𝑅 Or 𝐴)) 

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

⊢ (𝑅 = 𝑆 → (𝑅 Or 𝐴 ↔ 𝑆 Or 𝐴)) 

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

⊢ (𝐴 = 𝐵 → (𝑅 Or 𝐴 ↔ 𝑅 Or 𝐵)) 

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

⊢ ((𝑅 Or 𝐴 ∧ 𝐵 ∈ 𝐴) → ¬ 𝐵𝑅𝐵) 

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

⊢ ((𝑅 Or 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → ((𝐵𝑅𝐶 ∧ 𝐶𝑅𝐷) → 𝐵𝑅𝐷)) 

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

⊢ (𝜑 → 𝑅 Po 𝐴)
& ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)) ⇒ ⊢ (𝜑 → 𝑅 Or 𝐴) 

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

⊢ ((𝑅 Or 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → (𝐵𝑅𝐶 → (𝐵𝑅𝐷 ∨ 𝐷𝑅𝐶))) 

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

⊢ ((𝑅 Or 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴)) → ¬ (𝐵𝑅𝐶 ∧ 𝐶𝑅𝐵)) 

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

⊢ ((𝑅 Or 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → ¬ (𝐵𝑅𝐶 ∧ 𝐶𝑅𝐷 ∧ 𝐷𝑅𝐵)) 

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

⊢ ((𝑅 Or 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴)) → (𝐵𝑅𝐶 → ¬ (𝐵 = 𝐶 ∨ 𝐶𝑅𝐵))) 

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

⊢ 𝑅 Or 𝐴
& ⊢ ((𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴) → (𝐵𝑅𝐶 ∨ 𝐵 = 𝐶 ∨ 𝐶𝑅𝐵)) ⇒ ⊢ ((𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴) → (𝐵𝑅𝐶 ↔ ¬ (𝐵 = 𝐶 ∨ 𝐶𝑅𝐵))) 

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

⊢ 𝑅 Or 𝐴
& ⊢ ((𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴) → (𝐵𝑅𝐶 ∨ 𝐵 = 𝐶 ∨ 𝐶𝑅𝐵)) ⇒ ⊢ ((𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴) → (𝐵 = 𝐶 ↔ ¬ (𝐵𝑅𝐶 ∨ 𝐶𝑅𝐵))) 

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

⊢ 𝑅 Or ∅ 

2.3.9 Founded and setlike
relations


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

wff FrFor 𝑅𝐴𝑆 

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

wff 𝑅 Fr 𝐴 

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

wff 𝑅 Se 𝐴 

Syntax  wwe 4258 
Extend wff notation to include the wellordering predicate. Read:
' 𝑅 wellorders 𝐴.'

wff 𝑅 We 𝐴 

Definition  dffrfor 4259* 
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 4260* 
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 Fr. (Contributed by
Jim Kingdon and Mario
Carneiro, 21Sep2021.)

⊢ (𝑅 Fr 𝐴 ↔ ∀𝑠 FrFor 𝑅𝐴𝑠) 

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

⊢ (𝑅 Se 𝐴 ↔ ∀𝑥 ∈ 𝐴 {𝑦 ∈ 𝐴 ∣ 𝑦𝑅𝑥} ∈ V) 

Definition  dfwetr 4262* 
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 4443). Given excluded middle, wellordering is
usually defined to require trichotomy (and the definition of Fr is
typically also different). (Contributed by Mario Carneiro and Jim
Kingdon, 23Sep2021.)

⊢ (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧))) 

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

⊢ ((𝑅 Se 𝐴 ∧ 𝐵 ∈ 𝐴) → {𝑥 ∈ 𝐴 ∣ 𝑥𝑅𝐵} ∈ V) 

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

⊢ (𝐴 ∈ 𝑉 → 𝑅 Se 𝐴) 

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

⊢ (𝑅 ⊆ 𝑆 → (𝑆 Se 𝐴 → 𝑅 Se 𝐴)) 

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

⊢ (𝐴 ⊆ 𝐵 → (𝑅 Se 𝐵 → 𝑅 Se 𝐴)) 

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

⊢ (𝑅 = 𝑆 → (𝑅 Se 𝐴 ↔ 𝑆 Se 𝐴)) 

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

⊢ (𝐴 = 𝐵 → (𝑅 Se 𝐴 ↔ 𝑅 Se 𝐵)) 

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

⊢ Ⅎ𝑥𝑅
& ⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥 𝑅 Se 𝐴 

Theorem  epse 4270 
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.)

⊢ E Se 𝐴 

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

⊢ (𝑅 = 𝑆 → ( FrFor 𝑅𝐴𝑇 ↔ FrFor 𝑆𝐴𝑇)) 

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

⊢ (𝑅 = 𝑆 → (𝑅 Fr 𝐴 ↔ 𝑆 Fr 𝐴)) 

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

⊢ (𝐴 = 𝐵 → ( FrFor 𝑅𝐴𝑇 ↔ FrFor 𝑅𝐵𝑇)) 

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

⊢ (𝐴 = 𝐵 → (𝑅 Fr 𝐴 ↔ 𝑅 Fr 𝐵)) 

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

⊢ (𝑆 = 𝑇 → ( FrFor 𝑅𝐴𝑆 ↔ FrFor 𝑅𝐴𝑇)) 

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

⊢ Ⅎ𝑥𝑅
& ⊢ Ⅎ𝑥𝐴
& ⊢ Ⅎ𝑥𝑆 ⇒ ⊢ Ⅎ𝑥 FrFor 𝑅𝐴𝑆 

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

⊢ Ⅎ𝑥𝑅
& ⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥 𝑅 Fr 𝐴 

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

⊢ ((𝑅 Fr 𝐴 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝐴) → ¬ 𝐵𝑅𝐵) 

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

⊢ 𝑅 Fr ∅ 

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

⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) & ⊢ ((𝜒 ∧ 𝑥 ∈ 𝐴) → (∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → 𝜓) → 𝜑)) & ⊢ (𝜒 → 𝑅 Fr 𝐴)
& ⊢ (𝜒 → 𝐴 ∈ 𝑉) ⇒ ⊢ ((𝜒 ∧ 𝑥 ∈ 𝐴) → 𝜑) 

Theorem  efrirr 4281 
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.)

⊢ ( E Fr 𝐴 → ¬ 𝐴 ∈ 𝐴) 

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

⊢ ((Tr 𝐴 ∧ E Fr 𝐴 ∧ 𝐵 ∈ 𝐴) → (𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ 𝐴)) 

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

⊢ Ⅎ𝑥𝑅
& ⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥 𝑅 We 𝐴 

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

⊢ (𝑅 = 𝑆 → (𝑅 We 𝐴 ↔ 𝑆 We 𝐴)) 

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

⊢ (𝐴 = 𝐵 → (𝑅 We 𝐴 ↔ 𝑅 We 𝐵)) 

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

⊢ (𝑅 We 𝐴 → 𝑅 Fr 𝐴) 

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

⊢ ((𝑅 We 𝐴 ∧ 𝐴 ∈ 𝑉) → 𝑅 Po 𝐴) 

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

⊢ (( E We 𝐴 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → ((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝑧) → 𝑥 ∈ 𝑧)) 

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

⊢ 𝑅 We ∅ 

2.3.10 Ordinals


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

wff Ord 𝐴 

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

class On 

Syntax  wlim 4292 
Extend the definition of a wff to include the limit ordinal predicate.

wff Lim 𝐴 

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

class suc 𝐴 

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

⊢ (Ord 𝐴 ↔ (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 Tr 𝑥)) 

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

⊢ (Ord 𝐴 ↔ (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 Tr 𝑥)) 

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

⊢ On = {𝑥 ∣ Ord 𝑥} 

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

⊢ (Lim 𝐴 ↔ (Ord 𝐴 ∧ ∅ ∈ 𝐴 ∧ 𝐴 = ∪ 𝐴)) 

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

⊢ (Lim 𝐴 ↔ (Ord 𝐴 ∧ ∅ ∈ 𝐴 ∧ 𝐴 = ∪ 𝐴)) 

Definition  dfsuc 4299 
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 4340). 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.)

⊢ suc 𝐴 = (𝐴 ∪ {𝐴}) 

Theorem  ordeq 4300 
Equality theorem for the ordinal predicate. (Contributed by NM,
17Sep1993.)

⊢ (𝐴 = 𝐵 → (Ord 𝐴 ↔ Ord 𝐵)) 