Type  Label  Description 
Statement 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

⊢ 𝑅 Po ∅ 

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

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

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

⊢ (𝑅 Or 𝐴 → 𝑅 Po 𝐴) 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

wff FrFor 𝑅𝐴𝑆 

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

wff 𝑅 Fr 𝐴 

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

wff 𝑅 Se 𝐴 

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

wff 𝑅 We 𝐴 

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

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

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

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

Theorem  seex 4134* 
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 4135 
Any relation on a set is setlike on it. (Contributed by Mario
Carneiro, 22Jun2015.)

⊢ (𝐴 ∈ 𝑉 → 𝑅 Se 𝐴) 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

⊢ 𝑅 Fr ∅ 

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

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

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

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

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

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

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

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

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

⊢ (𝑅 We 𝐴 → 𝑅 Fr 𝐴) 

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

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

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

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

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

⊢ 𝑅 We ∅ 

2.3.10 Ordinals


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

wff Ord 𝐴 

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

wff Lim 𝐴 

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

class suc 𝐴 

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

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

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

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

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

⊢ On = {𝑥 ∣ Ord 𝑥} 

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

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

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

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

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

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

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

⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ On ↔ Ord 𝐴)) 

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

⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 ∈ On ↔ Ord 𝐴) 

Theorem  eloni 4174 
An ordinal number has the ordinal property. (Contributed by NM,
5Jun1994.)

⊢ (𝐴 ∈ On → Ord 𝐴) 

Theorem  elon2 4175 
An ordinal number is an ordinal set. (Contributed by NM, 8Feb2004.)

⊢ (𝐴 ∈ On ↔ (Ord 𝐴 ∧ 𝐴 ∈ V)) 

Theorem  limeq 4176 
Equality theorem for the limit predicate. (Contributed by NM,
22Apr1994.) (Proof shortened by Andrew Salmon, 25Jul2011.)

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

Theorem  ordtr 4177 
An ordinal class is transitive. (Contributed by NM, 3Apr1994.)

⊢ (Ord 𝐴 → Tr 𝐴) 

Theorem  ordelss 4178 
An element of an ordinal class is a subset of it. (Contributed by NM,
30May1994.)

⊢ ((Ord 𝐴 ∧ 𝐵 ∈ 𝐴) → 𝐵 ⊆ 𝐴) 

Theorem  trssord 4179 
A transitive subclass of an ordinal class is ordinal. (Contributed by
NM, 29May1994.)

⊢ ((Tr 𝐴 ∧ 𝐴 ⊆ 𝐵 ∧ Ord 𝐵) → Ord 𝐴) 

Theorem  ordelord 4180 
An element of an ordinal class is ordinal. Proposition 7.6 of
[TakeutiZaring] p. 36.
(Contributed by NM, 23Apr1994.)

⊢ ((Ord 𝐴 ∧ 𝐵 ∈ 𝐴) → Ord 𝐵) 

Theorem  tron 4181 
The class of all ordinal numbers is transitive. (Contributed by NM,
4May2009.)

⊢ Tr On 

Theorem  ordelon 4182 
An element of an ordinal class is an ordinal number. (Contributed by NM,
26Oct2003.)

⊢ ((Ord 𝐴 ∧ 𝐵 ∈ 𝐴) → 𝐵 ∈ On) 

Theorem  onelon 4183 
An element of an ordinal number is an ordinal number. Theorem 2.2(iii) of
[BellMachover] p. 469. (Contributed
by NM, 26Oct2003.)

⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ 𝐴) → 𝐵 ∈ On) 

Theorem  ordin 4184 
The intersection of two ordinal classes is ordinal. Proposition 7.9 of
[TakeutiZaring] p. 37. (Contributed
by NM, 9May1994.)

⊢ ((Ord 𝐴 ∧ Ord 𝐵) → Ord (𝐴 ∩ 𝐵)) 

Theorem  onin 4185 
The intersection of two ordinal numbers is an ordinal number.
(Contributed by NM, 7Apr1995.)

⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ∩ 𝐵) ∈ On) 

Theorem  onelss 4186 
An element of an ordinal number is a subset of the number. (Contributed
by NM, 5Jun1994.) (Proof shortened by Andrew Salmon, 25Jul2011.)

⊢ (𝐴 ∈ On → (𝐵 ∈ 𝐴 → 𝐵 ⊆ 𝐴)) 

Theorem  ordtr1 4187 
Transitive law for ordinal classes. (Contributed by NM, 12Dec2004.)

⊢ (Ord 𝐶 → ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ 𝐶)) 

Theorem  ontr1 4188 
Transitive law for ordinal numbers. Theorem 7M(b) of [Enderton] p. 192.
(Contributed by NM, 11Aug1994.)

⊢ (𝐶 ∈ On → ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ 𝐶)) 

Theorem  onintss 4189* 
If a property is true for an ordinal number, then the minimum ordinal
number for which it is true is smaller or equal. Theorem Schema 61 of
[Suppes] p. 228. (Contributed by NM,
3Oct2003.)

⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ On → (𝜓 → ∩ {𝑥 ∈ On ∣ 𝜑} ⊆ 𝐴)) 

Theorem  ord0 4190 
The empty set is an ordinal class. (Contributed by NM, 11May1994.)

⊢ Ord ∅ 

Theorem  0elon 4191 
The empty set is an ordinal number. Corollary 7N(b) of [Enderton] p. 193.
(Contributed by NM, 17Sep1993.)

⊢ ∅ ∈ On 

Theorem  inton 4192 
The intersection of the class of ordinal numbers is the empty set.
(Contributed by NM, 20Oct2003.)

⊢ ∩ On =
∅ 

Theorem  nlim0 4193 
The empty set is not a limit ordinal. (Contributed by NM, 24Mar1995.)
(Proof shortened by Andrew Salmon, 25Jul2011.)

⊢ ¬ Lim ∅ 

Theorem  limord 4194 
A limit ordinal is ordinal. (Contributed by NM, 4May1995.)

⊢ (Lim 𝐴 → Ord 𝐴) 

Theorem  limuni 4195 
A limit ordinal is its own supremum (union). (Contributed by NM,
4May1995.)

⊢ (Lim 𝐴 → 𝐴 = ∪ 𝐴) 

Theorem  limuni2 4196 
The union of a limit ordinal is a limit ordinal. (Contributed by NM,
19Sep2006.)

⊢ (Lim 𝐴 → Lim ∪
𝐴) 

Theorem  0ellim 4197 
A limit ordinal contains the empty set. (Contributed by NM,
15May1994.)

⊢ (Lim 𝐴 → ∅ ∈ 𝐴) 

Theorem  limelon 4198 
A limit ordinal class that is also a set is an ordinal number.
(Contributed by NM, 26Apr2004.)

⊢ ((𝐴 ∈ 𝐵 ∧ Lim 𝐴) → 𝐴 ∈ On) 

Theorem  onn0 4199 
The class of all ordinal numbers is not empty. (Contributed by NM,
17Sep1995.)

⊢ On ≠ ∅ 

Theorem  onm 4200 
The class of all ordinal numbers is inhabited. (Contributed by Jim
Kingdon, 6Mar2019.)

⊢ ∃𝑥 𝑥 ∈ On 