P. 63 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 6201-6300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	dfpred2 6201*	An alternate definition of predecessor class when 𝑋 is a set. (Contributed by Scott Fenton, 8-Feb-2011.)
⊢ 𝑋 ∈ V    ⇒   ⊢ Pred(𝑅, 𝐴, 𝑋) = (𝐴 ∩ {𝑦 ∣ 𝑦𝑅𝑋})
Theorem	dfpred3 6202*	An alternate definition of predecessor class when 𝑋 is a set. (Contributed by Scott Fenton, 13-Jun-2018.)
⊢ 𝑋 ∈ V    ⇒   ⊢ Pred(𝑅, 𝐴, 𝑋) = {𝑦 ∈ 𝐴 ∣ 𝑦𝑅𝑋}
Theorem	dfpred3g 6203*	An alternate definition of predecessor class when 𝑋 is a set. (Contributed by Scott Fenton, 13-Jun-2018.)
⊢ (𝑋 ∈ 𝑉 → Pred(𝑅, 𝐴, 𝑋) = {𝑦 ∈ 𝐴 ∣ 𝑦𝑅𝑋})
Theorem	elpredgg 6204	Membership in a predecessor class. (Contributed by Scott Fenton, 17-Apr-2011.) Generalize to closed form. (Revised by BJ, 16-Oct-2024.)
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) → (𝑌 ∈ Pred(𝑅, 𝐴, 𝑋) ↔ (𝑌 ∈ 𝐴 ∧ 𝑌𝑅𝑋)))
Theorem	elpredg 6205	Membership in a predecessor class. (Contributed by Scott Fenton, 17-Apr-2011.) (Proof shortened by BJ, 16-Oct-2024.)
⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐴) → (𝑌 ∈ Pred(𝑅, 𝐴, 𝑋) ↔ 𝑌𝑅𝑋))
Theorem	elpredimg 6206	Membership in a predecessor class - implicative version. (Contributed by Scott Fenton, 9-May-2012.) Generalize to closed form. (Revised by BJ, 16-Oct-2024.)
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ Pred(𝑅, 𝐴, 𝑋)) → 𝑌𝑅𝑋)
Theorem	elpredim 6207	Membership in a predecessor class - implicative version. (Contributed by Scott Fenton, 9-May-2012.) (Proof shortened by BJ, 16-Oct-2024.)
⊢ 𝑋 ∈ V    ⇒   ⊢ (𝑌 ∈ Pred(𝑅, 𝐴, 𝑋) → 𝑌𝑅𝑋)
Theorem	elpred 6208	Membership in a predecessor class. (Contributed by Scott Fenton, 4-Feb-2011.) (Proof shortened by BJ, 16-Oct-2024.)
⊢ 𝑌 ∈ V    ⇒   ⊢ (𝑋 ∈ 𝐷 → (𝑌 ∈ Pred(𝑅, 𝐴, 𝑋) ↔ (𝑌 ∈ 𝐴 ∧ 𝑌𝑅𝑋)))
Theorem	predexg 6209	The predecessor class exists when 𝐴 does. (Contributed by Scott Fenton, 8-Feb-2011.) Generalize to closed form. (Revised by BJ, 27-Oct-2024.)
⊢ (𝐴 ∈ 𝑉 → Pred(𝑅, 𝐴, 𝑋) ∈ V)
Theorem	predasetexOLD 6210	Obsolete form of predexg 6209 as of 27-Oct-2024. (Contributed by Scott Fenton, 8-Feb-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐴 ∈ V    ⇒   ⊢ Pred(𝑅, 𝐴, 𝑋) ∈ V
Theorem	dffr4 6211*	Alternate definition of well-founded relation. (Contributed by Scott Fenton, 2-Feb-2011.)
⊢ (𝑅 Fr 𝐴 ↔ ∀𝑥((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) → ∃𝑦 ∈ 𝑥 Pred(𝑅, 𝑥, 𝑦) = ∅))
Theorem	predel 6212	Membership in the predecessor class implies membership in the base class. (Contributed by Scott Fenton, 11-Feb-2011.)
⊢ (𝑌 ∈ Pred(𝑅, 𝐴, 𝑋) → 𝑌 ∈ 𝐴)
Theorem	predbrg 6213	Closed form of elpredim 6207. (Contributed by Scott Fenton, 13-Apr-2011.) (Revised by NM, 5-Apr-2016.)
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ Pred(𝑅, 𝐴, 𝑋)) → 𝑌𝑅𝑋)
Theorem	predtrss 6214	If 𝑅 is transitive over 𝐴 and 𝑌𝑅𝑋, then Pred(𝑅, 𝐴, 𝑌) is a subclass of Pred(𝑅, 𝐴, 𝑋). (Contributed by Scott Fenton, 28-Oct-2024.)
⊢ ((((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅 ∧ 𝑌 ∈ Pred(𝑅, 𝐴, 𝑋) ∧ 𝑋 ∈ 𝐴) → Pred(𝑅, 𝐴, 𝑌) ⊆ Pred(𝑅, 𝐴, 𝑋))
Theorem	predpo 6215	Property of the predecessor class for partial orders. (Contributed by Scott Fenton, 28-Apr-2012.) (Proof shortened by Scott Fenton, 28-Oct-2024.)
⊢ ((𝑅 Po 𝐴 ∧ 𝑋 ∈ 𝐴) → (𝑌 ∈ Pred(𝑅, 𝐴, 𝑋) → Pred(𝑅, 𝐴, 𝑌) ⊆ Pred(𝑅, 𝐴, 𝑋)))
Theorem	predso 6216	Property of the predecessor class for strict total orders. (Contributed by Scott Fenton, 11-Feb-2011.)
⊢ ((𝑅 Or 𝐴 ∧ 𝑋 ∈ 𝐴) → (𝑌 ∈ Pred(𝑅, 𝐴, 𝑋) → Pred(𝑅, 𝐴, 𝑌) ⊆ Pred(𝑅, 𝐴, 𝑋)))
Theorem	setlikespec 6217	If 𝑅 is set-like in 𝐴, then all predecessor classes of elements of 𝐴 exist. (Contributed by Scott Fenton, 20-Feb-2011.) (Revised by Mario Carneiro, 26-Jun-2015.)
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) → Pred(𝑅, 𝐴, 𝑋) ∈ V)
Theorem	predidm 6218	Idempotent law for the predecessor class. (Contributed by Scott Fenton, 29-Mar-2011.)
⊢ Pred(𝑅, Pred(𝑅, 𝐴, 𝑋), 𝑋) = Pred(𝑅, 𝐴, 𝑋)
Theorem	predin 6219	Intersection law for predecessor classes. (Contributed by Scott Fenton, 29-Mar-2011.)
⊢ Pred(𝑅, (𝐴 ∩ 𝐵), 𝑋) = (Pred(𝑅, 𝐴, 𝑋) ∩ Pred(𝑅, 𝐵, 𝑋))
Theorem	predun 6220	Union law for predecessor classes. (Contributed by Scott Fenton, 29-Mar-2011.)
⊢ Pred(𝑅, (𝐴 ∪ 𝐵), 𝑋) = (Pred(𝑅, 𝐴, 𝑋) ∪ Pred(𝑅, 𝐵, 𝑋))
Theorem	preddif 6221	Difference law for predecessor classes. (Contributed by Scott Fenton, 14-Apr-2011.)
⊢ Pred(𝑅, (𝐴 ∖ 𝐵), 𝑋) = (Pred(𝑅, 𝐴, 𝑋) ∖ Pred(𝑅, 𝐵, 𝑋))
Theorem	predep 6222	The predecessor under the membership relation is equivalent to an intersection. (Contributed by Scott Fenton, 27-Mar-2011.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
⊢ (𝑋 ∈ 𝐵 → Pred( E , 𝐴, 𝑋) = (𝐴 ∩ 𝑋))
Theorem	trpred 6223	The class of predecessors of an element of a transitive class for the membership relation is that element. (Contributed by BJ, 12-Oct-2024.)
⊢ ((Tr 𝐴 ∧ 𝑋 ∈ 𝐴) → Pred( E , 𝐴, 𝑋) = 𝑋)
Theorem	preddowncl 6224*	A property of classes that are downward closed under predecessor. (Contributed by Scott Fenton, 13-Apr-2011.)
⊢ ((𝐵 ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝐵 Pred(𝑅, 𝐴, 𝑥) ⊆ 𝐵) → (𝑋 ∈ 𝐵 → Pred(𝑅, 𝐵, 𝑋) = Pred(𝑅, 𝐴, 𝑋)))
Theorem	predpoirr 6225	Given a partial ordering, a class is not a member of its predecessor class. (Contributed by Scott Fenton, 17-Apr-2011.)
⊢ (𝑅 Po 𝐴 → ¬ 𝑋 ∈ Pred(𝑅, 𝐴, 𝑋))
Theorem	predfrirr 6226	Given a well-founded relation, a class is not a member of its predecessor class. (Contributed by Scott Fenton, 22-Apr-2011.)
⊢ (𝑅 Fr 𝐴 → ¬ 𝑋 ∈ Pred(𝑅, 𝐴, 𝑋))
Theorem	pred0 6227	The predecessor class over ∅ is always ∅. (Contributed by Scott Fenton, 16-Apr-2011.) (Proof shortened by AV, 11-Jun-2021.)
⊢ Pred(𝑅, ∅, 𝑋) = ∅
2.3.12  Well-founded induction (variant)
Theorem	frpomin 6228*	Every nonempty (possibly proper) subclass of a class 𝐴 with a well-founded set-like partial order 𝑅 has a minimal element. The additional condition of partial order over frmin 9438 enables avoiding the axiom of infinity. (Contributed by Scott Fenton, 11-Feb-2022.)
⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅)) → ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥)
Theorem	frpomin2 6229*	Every nonempty (possibly proper) subclass of a class 𝐴 with a well-founded set-like partial order 𝑅 has a minimal element. The additional condition of partial order over frmin 9438 enables avoiding the axiom of infinity. (Contributed by Scott Fenton, 11-Feb-2022.)
⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅)) → ∃𝑥 ∈ 𝐵 Pred(𝑅, 𝐵, 𝑥) = ∅)
Theorem	frpoind 6230*	The principle of well-founded induction over a partial order. This theorem is a version of frind 9439 that does not require the axiom of infinity and can be used to prove wfi 6238 and tfi 7675. (Contributed by Scott Fenton, 11-Feb-2022.)
⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝐵 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝐴 (Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵 → 𝑦 ∈ 𝐵))) → 𝐴 = 𝐵)
Theorem	frpoinsg 6231*	Well-Founded Induction Schema (variant). If a property passes from all elements less than 𝑦 of a well-founded set-like partial order class 𝐴 to 𝑦 itself (induction hypothesis), then the property holds for all elements of 𝐴. (Contributed by Scott Fenton, 11-Feb-2022.)
⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) ∧ 𝑦 ∈ 𝐴) → (∀𝑧 ∈ Pred (𝑅, 𝐴, 𝑦)[𝑧 / 𝑦]𝜑 → 𝜑))    ⇒   ⊢ ((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) → ∀𝑦 ∈ 𝐴 𝜑)
Theorem	frpoins2fg 6232*	Well-Founded Induction schema, using implicit substitution. (Contributed by Scott Fenton, 24-Aug-2022.)
⊢ (𝑦 ∈ 𝐴 → (∀𝑧 ∈ Pred (𝑅, 𝐴, 𝑦)𝜓 → 𝜑))    &   ⊢ Ⅎ𝑦𝜓    &   ⊢ (𝑦 = 𝑧 → (𝜑 ↔ 𝜓))    ⇒   ⊢ ((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) → ∀𝑦 ∈ 𝐴 𝜑)
Theorem	frpoins2g 6233*	Well-Founded Induction schema, using implicit substitution. (Contributed by Scott Fenton, 24-Aug-2022.)
⊢ (𝑦 ∈ 𝐴 → (∀𝑧 ∈ Pred (𝑅, 𝐴, 𝑦)𝜓 → 𝜑))    &   ⊢ (𝑦 = 𝑧 → (𝜑 ↔ 𝜓))    ⇒   ⊢ ((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) → ∀𝑦 ∈ 𝐴 𝜑)
Theorem	frpoins3g 6234*	Well-Founded Induction schema, using implicit substitution. (Contributed by Scott Fenton, 19-Aug-2024.)
⊢ (𝑥 ∈ 𝐴 → (∀𝑦 ∈ Pred (𝑅, 𝐴, 𝑥)𝜓 → 𝜑))    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜒))    ⇒   ⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) ∧ 𝐵 ∈ 𝐴) → 𝜒)
2.3.13  Well-ordered induction
Theorem	tz6.26 6235*	All nonempty subclasses of a class having a well-ordered set-like relation have minimal elements for that relation. Proposition 6.26 of [TakeutiZaring] p. 31. (Contributed by Scott Fenton, 29-Jan-2011.) (Revised by Mario Carneiro, 26-Jun-2015.) (Proof shortened by Scott Fenton, 17-Nov-2024.)
⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅)) → ∃𝑦 ∈ 𝐵 Pred(𝑅, 𝐵, 𝑦) = ∅)
Theorem	tz6.26OLD 6236*	Obsolete proof of tz6.26 6235 as of 17-Nov-2024. (New usage is discouraged.) (Proof modification is discouraged.) (Contributed by Scott Fenton, 29-Jan-2011.) (Revised by Mario Carneiro, 26-Jun-2015.)
⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅)) → ∃𝑦 ∈ 𝐵 Pred(𝑅, 𝐵, 𝑦) = ∅)
Theorem	tz6.26i 6237*	All nonempty subclasses of a class having a well-ordered set-like relation 𝑅 have 𝑅-minimal elements. Proposition 6.26 of [TakeutiZaring] p. 31. (Contributed by Scott Fenton, 14-Apr-2011.) (Revised by Mario Carneiro, 26-Jun-2015.)
⊢ 𝑅 We 𝐴    &   ⊢ 𝑅 Se 𝐴    ⇒   ⊢ ((𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅) → ∃𝑦 ∈ 𝐵 Pred(𝑅, 𝐵, 𝑦) = ∅)
Theorem	wfi 6238*	The Principle of Well-Ordered Induction. Theorem 6.27 of [TakeutiZaring] p. 32. This principle states that if 𝐵 is a subclass of a well-ordered class 𝐴 with the property that every element of 𝐵 whose inital segment is included in 𝐴 is itself equal to 𝐴. (Contributed by Scott Fenton, 29-Jan-2011.) (Revised by Mario Carneiro, 26-Jun-2015.) (Proof shortened by Scott Fenton, 17-Nov-2024.)
⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝐵 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝐴 (Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵 → 𝑦 ∈ 𝐵))) → 𝐴 = 𝐵)
Theorem	wfiOLD 6239*	Obsolete proof of wfi 6238 as of 17-Nov-2024. (New usage is discouraged.) (Proof modification is discouraged.) (Contributed by Scott Fenton, 29-Jan-2011.) (Revised by Mario Carneiro, 26-Jun-2015.)
⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝐵 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝐴 (Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵 → 𝑦 ∈ 𝐵))) → 𝐴 = 𝐵)
Theorem	wfii 6240*	The Principle of Well-Ordered Induction. Theorem 6.27 of [TakeutiZaring] p. 32. This principle states that if 𝐵 is a subclass of a well-ordered class 𝐴 with the property that every element of 𝐵 whose inital segment is included in 𝐴 is itself equal to 𝐴. (Contributed by Scott Fenton, 29-Jan-2011.) (Revised by Mario Carneiro, 26-Jun-2015.)
⊢ 𝑅 We 𝐴    &   ⊢ 𝑅 Se 𝐴    ⇒   ⊢ ((𝐵 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝐴 (Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵 → 𝑦 ∈ 𝐵)) → 𝐴 = 𝐵)
Theorem	wfisg 6241*	Well-Ordered Induction Schema. If a property passes from all elements less than 𝑦 of a well-ordered class 𝐴 to 𝑦 itself (induction hypothesis), then the property holds for all elements of 𝐴. (Contributed by Scott Fenton, 11-Feb-2011.) (Proof shortened by Scott Fenton, 17-Nov-2024.)
⊢ (𝑦 ∈ 𝐴 → (∀𝑧 ∈ Pred (𝑅, 𝐴, 𝑦)[𝑧 / 𝑦]𝜑 → 𝜑))    ⇒   ⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴) → ∀𝑦 ∈ 𝐴 𝜑)
Theorem	wfisgOLD 6242*	Obsolete proof of wfisg 6241 as of 17-Nov-2024. (New usage is discouraged.) (Proof modification is discouraged.) (Contributed by Scott Fenton, 11-Feb-2011.)
⊢ (𝑦 ∈ 𝐴 → (∀𝑧 ∈ Pred (𝑅, 𝐴, 𝑦)[𝑧 / 𝑦]𝜑 → 𝜑))    ⇒   ⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴) → ∀𝑦 ∈ 𝐴 𝜑)
Theorem	wfis 6243*	Well-Ordered Induction Schema. If all elements less than a given set 𝑥 of the well-ordered class 𝐴 have a property (induction hypothesis), then all elements of 𝐴 have that property. (Contributed by Scott Fenton, 29-Jan-2011.)
⊢ 𝑅 We 𝐴    &   ⊢ 𝑅 Se 𝐴    &   ⊢ (𝑦 ∈ 𝐴 → (∀𝑧 ∈ Pred (𝑅, 𝐴, 𝑦)[𝑧 / 𝑦]𝜑 → 𝜑))    ⇒   ⊢ (𝑦 ∈ 𝐴 → 𝜑)
Theorem	wfis2fg 6244*	Well-Ordered Induction Schema, using implicit substitution. (Contributed by Scott Fenton, 11-Feb-2011.) (Proof shortened by Scott Fenton, 17-Nov-2024.)
⊢ Ⅎ𝑦𝜓    &   ⊢ (𝑦 = 𝑧 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑦 ∈ 𝐴 → (∀𝑧 ∈ Pred (𝑅, 𝐴, 𝑦)𝜓 → 𝜑))    ⇒   ⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴) → ∀𝑦 ∈ 𝐴 𝜑)
Theorem	wfis2fgOLD 6245*	Obsolete proof of wfis2fg 6244 as of 17-Nov-2024. (New usage is discouraged.) (Proof modification is discouraged.) (Contributed by Scott Fenton, 11-Feb-2011.)
⊢ Ⅎ𝑦𝜓    &   ⊢ (𝑦 = 𝑧 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑦 ∈ 𝐴 → (∀𝑧 ∈ Pred (𝑅, 𝐴, 𝑦)𝜓 → 𝜑))    ⇒   ⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴) → ∀𝑦 ∈ 𝐴 𝜑)
Theorem	wfis2f 6246*	Well-Ordered Induction schema, using implicit substitution. (Contributed by Scott Fenton, 29-Jan-2011.)
⊢ 𝑅 We 𝐴    &   ⊢ 𝑅 Se 𝐴    &   ⊢ Ⅎ𝑦𝜓    &   ⊢ (𝑦 = 𝑧 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑦 ∈ 𝐴 → (∀𝑧 ∈ Pred (𝑅, 𝐴, 𝑦)𝜓 → 𝜑))    ⇒   ⊢ (𝑦 ∈ 𝐴 → 𝜑)
Theorem	wfis2g 6247*	Well-Ordered Induction Schema, using implicit substitution. (Contributed by Scott Fenton, 11-Feb-2011.)
⊢ (𝑦 = 𝑧 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑦 ∈ 𝐴 → (∀𝑧 ∈ Pred (𝑅, 𝐴, 𝑦)𝜓 → 𝜑))    ⇒   ⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴) → ∀𝑦 ∈ 𝐴 𝜑)
Theorem	wfis2 6248*	Well-Ordered Induction schema, using implicit substitution. (Contributed by Scott Fenton, 29-Jan-2011.)
⊢ 𝑅 We 𝐴    &   ⊢ 𝑅 Se 𝐴    &   ⊢ (𝑦 = 𝑧 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑦 ∈ 𝐴 → (∀𝑧 ∈ Pred (𝑅, 𝐴, 𝑦)𝜓 → 𝜑))    ⇒   ⊢ (𝑦 ∈ 𝐴 → 𝜑)
Theorem	wfis3 6249*	Well-Ordered Induction schema, using implicit substitution. (Contributed by Scott Fenton, 29-Jan-2011.)
⊢ 𝑅 We 𝐴    &   ⊢ 𝑅 Se 𝐴    &   ⊢ (𝑦 = 𝑧 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑦 = 𝐵 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑦 ∈ 𝐴 → (∀𝑧 ∈ Pred (𝑅, 𝐴, 𝑦)𝜓 → 𝜑))    ⇒   ⊢ (𝐵 ∈ 𝐴 → 𝜒)
2.3.14  Ordinals
Syntax	word 6250	Extend the definition of a wff to include the ordinal predicate.
wff Ord 𝐴
Syntax	con0 6251	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 6252	Extend the definition of a wff to include the limit ordinal predicate.
wff Lim 𝐴
Syntax	csuc 6253	Extend class notation to include the successor function.
class suc 𝐴
Definition	df-ord 6254	Define the ordinal predicate, which is true for a class that is transitive and is well-ordered by the membership relation. Variant of definition of [BellMachover] p. 468. Some sources will define a notation for ordinal order corresponding to < and ≤ but we just use ∈ and ⊆ respectively. (Contributed by NM, 17-Sep-1993.)
⊢ (Ord 𝐴 ↔ (Tr 𝐴 ∧ E We 𝐴))
Definition	df-on 6255	Define the class of all ordinal numbers. Definition 7.11 of [TakeutiZaring] p. 38. (Contributed by NM, 5-Jun-1994.)
⊢ On = {𝑥 ∣ Ord 𝑥}
Definition	df-lim 6256	Define the limit ordinal predicate, which is true for a nonempty ordinal that 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. See dflim2 6307, dflim3 7669, and dflim4 for alternate definitions. (Contributed by NM, 22-Apr-1994.)
⊢ (Lim 𝐴 ↔ (Ord 𝐴 ∧ 𝐴 ≠ ∅ ∧ 𝐴 = ∪ 𝐴))
Definition	df-suc 6257	Define the successor of a class. When applied to an ordinal number, the successor means the same thing as "plus 1" (see oa1suc 8323). Definition 7.22 of [TakeutiZaring] p. 41, who use "+ 1" to denote this function. Ordinal natural numbers defined using this successor function and 0 as the empty set are also called von Neumann ordinals; 0 is the empty set {}, 1 is {0, {0}}, 2 is {1, {1}}, and so on. 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 6326), so that the successor of any ordinal class is still an ordinal class (ordsuc 7636), simplifying certain proofs. Some authors denote the successor operation with a prime (apostrophe-like) 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 plus-sign superscript. (Contributed by NM, 30-Aug-1993.)
⊢ suc 𝐴 = (𝐴 ∪ {𝐴})
Theorem	ordeq 6258	Equality theorem for the ordinal predicate. (Contributed by NM, 17-Sep-1993.)
⊢ (𝐴 = 𝐵 → (Ord 𝐴 ↔ Ord 𝐵))
Theorem	elong 6259	An ordinal number is an ordinal set. (Contributed by NM, 5-Jun-1994.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ On ↔ Ord 𝐴))
Theorem	elon 6260	An ordinal number is an ordinal set. (Contributed by NM, 5-Jun-1994.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 ∈ On ↔ Ord 𝐴)
Theorem	eloni 6261	An ordinal number has the ordinal property. (Contributed by NM, 5-Jun-1994.)
⊢ (𝐴 ∈ On → Ord 𝐴)
Theorem	elon2 6262	An ordinal number is an ordinal set. (Contributed by NM, 8-Feb-2004.)
⊢ (𝐴 ∈ On ↔ (Ord 𝐴 ∧ 𝐴 ∈ V))
Theorem	limeq 6263	Equality theorem for the limit predicate. (Contributed by NM, 22-Apr-1994.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
⊢ (𝐴 = 𝐵 → (Lim 𝐴 ↔ Lim 𝐵))
Theorem	ordwe 6264	Membership well-orders every ordinal. Proposition 7.4 of [TakeutiZaring] p. 36. (Contributed by NM, 3-Apr-1994.)
⊢ (Ord 𝐴 → E We 𝐴)
Theorem	ordtr 6265	An ordinal class is transitive. (Contributed by NM, 3-Apr-1994.)
⊢ (Ord 𝐴 → Tr 𝐴)
Theorem	ordfr 6266	Membership is well-founded on an ordinal class. In other words, an ordinal class is well-founded. (Contributed by NM, 22-Apr-1994.)
⊢ (Ord 𝐴 → E Fr 𝐴)
Theorem	ordelss 6267	An element of an ordinal class is a subset of it. (Contributed by NM, 30-May-1994.)
⊢ ((Ord 𝐴 ∧ 𝐵 ∈ 𝐴) → 𝐵 ⊆ 𝐴)
Theorem	trssord 6268	A transitive subclass of an ordinal class is ordinal. (Contributed by NM, 29-May-1994.)
⊢ ((Tr 𝐴 ∧ 𝐴 ⊆ 𝐵 ∧ Ord 𝐵) → Ord 𝐴)
Theorem	ordirr 6269	No ordinal class is a member of itself. In other words, the membership relation is irreflexive on ordinal classes. Theorem 2.2(i) of [BellMachover] p. 469, generalized to classes. We prove this without invoking the Axiom of Regularity. (Contributed by NM, 2-Jan-1994.)
⊢ (Ord 𝐴 → ¬ 𝐴 ∈ 𝐴)
Theorem	nordeq 6270	A member of an ordinal class is not equal to it. (Contributed by NM, 25-May-1998.)
⊢ ((Ord 𝐴 ∧ 𝐵 ∈ 𝐴) → 𝐴 ≠ 𝐵)
Theorem	ordn2lp 6271	An ordinal class cannot be an element of one of its members. Variant of first part of Theorem 2.2(vii) of [BellMachover] p. 469. (Contributed by NM, 3-Apr-1994.)
⊢ (Ord 𝐴 → ¬ (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐴))
Theorem	tz7.5 6272*	A nonempty subclass of an ordinal class has a minimal element. Proposition 7.5 of [TakeutiZaring] p. 36. (Contributed by NM, 18-Feb-2004.) (Revised by David Abernethy, 16-Mar-2011.)
⊢ ((Ord 𝐴 ∧ 𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅) → ∃𝑥 ∈ 𝐵 (𝐵 ∩ 𝑥) = ∅)
Theorem	ordelord 6273	An element of an ordinal class is ordinal. Proposition 7.6 of [TakeutiZaring] p. 36. (Contributed by NM, 23-Apr-1994.)
⊢ ((Ord 𝐴 ∧ 𝐵 ∈ 𝐴) → Ord 𝐵)
Theorem	tron 6274	The class of all ordinal numbers is transitive. (Contributed by NM, 4-May-2009.)
⊢ Tr On
Theorem	ordelon 6275	An element of an ordinal class is an ordinal number. (Contributed by NM, 26-Oct-2003.)
⊢ ((Ord 𝐴 ∧ 𝐵 ∈ 𝐴) → 𝐵 ∈ On)
Theorem	onelon 6276	An element of an ordinal number is an ordinal number. Theorem 2.2(iii) of [BellMachover] p. 469. (Contributed by NM, 26-Oct-2003.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ 𝐴) → 𝐵 ∈ On)
Theorem	tz7.7 6277	A transitive class belongs to an ordinal class iff it is strictly included in it. Proposition 7.7 of [TakeutiZaring] p. 37. (Contributed by NM, 5-May-1994.)
⊢ ((Ord 𝐴 ∧ Tr 𝐵) → (𝐵 ∈ 𝐴 ↔ (𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ 𝐴)))
Theorem	ordelssne 6278	For ordinal classes, membership is equivalent to strict inclusion. Corollary 7.8 of [TakeutiZaring] p. 37. (Contributed by NM, 25-Nov-1995.)
⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴 ∈ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵)))
Theorem	ordelpss 6279	For ordinal classes, membership is equivalent to strict inclusion. Corollary 7.8 of [TakeutiZaring] p. 37. (Contributed by NM, 17-Jun-1998.)
⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴 ∈ 𝐵 ↔ 𝐴 ⊊ 𝐵))
Theorem	ordsseleq 6280	For ordinal classes, inclusion is equivalent to membership or equality. (Contributed by NM, 25-Nov-1995.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴 ⊆ 𝐵 ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵)))
Theorem	ordin 6281	The intersection of two ordinal classes is ordinal. Proposition 7.9 of [TakeutiZaring] p. 37. (Contributed by NM, 9-May-1994.)
⊢ ((Ord 𝐴 ∧ Ord 𝐵) → Ord (𝐴 ∩ 𝐵))
Theorem	onin 6282	The intersection of two ordinal numbers is an ordinal number. (Contributed by NM, 7-Apr-1995.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ∩ 𝐵) ∈ On)
Theorem	ordtri3or 6283	A trichotomy law for ordinals. Proposition 7.10 of [TakeutiZaring] p. 38. (Contributed by NM, 10-May-1994.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴))
Theorem	ordtri1 6284	A trichotomy law for ordinals. (Contributed by NM, 25-Mar-1995.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴 ⊆ 𝐵 ↔ ¬ 𝐵 ∈ 𝐴))
Theorem	ontri1 6285	A trichotomy law for ordinal numbers. (Contributed by NM, 6-Nov-2003.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ⊆ 𝐵 ↔ ¬ 𝐵 ∈ 𝐴))
Theorem	ordtri2 6286	A trichotomy law for ordinals. (Contributed by NM, 25-Nov-1995.)
⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴 ∈ 𝐵 ↔ ¬ (𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴)))
Theorem	ordtri3 6287	A trichotomy law for ordinals. (Contributed by NM, 18-Oct-1995.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) (Proof shortened by JJ, 24-Sep-2021.)
⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴 = 𝐵 ↔ ¬ (𝐴 ∈ 𝐵 ∨ 𝐵 ∈ 𝐴)))
Theorem	ordtri4 6288	A trichotomy law for ordinals. (Contributed by NM, 1-Nov-2003.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ ¬ 𝐴 ∈ 𝐵)))
Theorem	orddisj 6289	An ordinal class and its singleton are disjoint. (Contributed by NM, 19-May-1998.)
⊢ (Ord 𝐴 → (𝐴 ∩ {𝐴}) = ∅)
Theorem	onfr 6290	The ordinal class is well-founded. This proof does not require the axiom of regularity. This lemma is used in ordon 7604 (through epweon 7603) in order to eliminate the need for the axiom of regularity. (Contributed by NM, 17-May-1994.)
⊢ E Fr On
Theorem	onelpss 6291	Relationship between membership and proper subset of an ordinal number. (Contributed by NM, 15-Sep-1995.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ∈ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵)))
Theorem	onsseleq 6292	Relationship between subset and membership of an ordinal number. (Contributed by NM, 15-Sep-1995.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ⊆ 𝐵 ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵)))
Theorem	onelss 6293	An element of an ordinal number is a subset of the number. (Contributed by NM, 5-Jun-1994.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
⊢ (𝐴 ∈ On → (𝐵 ∈ 𝐴 → 𝐵 ⊆ 𝐴))
Theorem	ordtr1 6294	Transitive law for ordinal classes. (Contributed by NM, 12-Dec-2004.)
⊢ (Ord 𝐶 → ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ 𝐶))
Theorem	ordtr2 6295	Transitive law for ordinal classes. (Contributed by NM, 12-Dec-2004.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
⊢ ((Ord 𝐴 ∧ Ord 𝐶) → ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ 𝐶))
Theorem	ordtr3 6296	Transitive law for ordinal classes. (Contributed by Mario Carneiro, 30-Dec-2014.) (Proof shortened by JJ, 24-Sep-2021.)
⊢ ((Ord 𝐵 ∧ Ord 𝐶) → (𝐴 ∈ 𝐵 → (𝐴 ∈ 𝐶 ∨ 𝐶 ∈ 𝐵)))
Theorem	ontr1 6297	Transitive law for ordinal numbers. Theorem 7M(b) of [Enderton] p. 192. (Contributed by NM, 11-Aug-1994.)
⊢ (𝐶 ∈ On → ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ 𝐶))
Theorem	ontr2 6298	Transitive law for ordinal numbers. Exercise 3 of [TakeutiZaring] p. 40. (Contributed by NM, 6-Nov-2003.)
⊢ ((𝐴 ∈ On ∧ 𝐶 ∈ On) → ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ 𝐶))
Theorem	ordunidif 6299	The union of an ordinal stays the same if a subset equal to one of its elements is removed. (Contributed by NM, 10-Dec-2004.)
⊢ ((Ord 𝐴 ∧ 𝐵 ∈ 𝐴) → ∪ (𝐴 ∖ 𝐵) = ∪ 𝐴)
Theorem	ordintdif 6300	If 𝐵 is smaller than 𝐴, then it equals the intersection of the difference. Exercise 11 in [TakeutiZaring] p. 44. (Contributed by Andrew Salmon, 14-Nov-2011.)
⊢ ((Ord 𝐴 ∧ Ord 𝐵 ∧ (𝐴 ∖ 𝐵) ≠ ∅) → 𝐵 = ∩ (𝐴 ∖ 𝐵))