P. 64 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 6301-6400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	predeq1 6301	Equality theorem for the predecessor class. (Contributed by Scott Fenton, 2-Feb-2011.)
⊢ (𝑅 = 𝑆 → Pred(𝑅, 𝐴, 𝑋) = Pred(𝑆, 𝐴, 𝑋))
Theorem	predeq2 6302	Equality theorem for the predecessor class. (Contributed by Scott Fenton, 2-Feb-2011.)
⊢ (𝐴 = 𝐵 → Pred(𝑅, 𝐴, 𝑋) = Pred(𝑅, 𝐵, 𝑋))
Theorem	predeq3 6303	Equality theorem for the predecessor class. (Contributed by Scott Fenton, 2-Feb-2011.)
⊢ (𝑋 = 𝑌 → Pred(𝑅, 𝐴, 𝑋) = Pred(𝑅, 𝐴, 𝑌))
Theorem	nfpred 6304	Bound-variable hypothesis builder for the predecessor class. (Contributed by Scott Fenton, 9-Jun-2018.)
⊢ Ⅎ𝑥𝑅    &   ⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝑋    ⇒   ⊢ Ⅎ𝑥Pred(𝑅, 𝐴, 𝑋)
Theorem	csbpredg 6305	Move class substitution in and out of the predecessor class of a relation. (Contributed by ML, 25-Oct-2020.)
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌Pred(𝑅, 𝐷, 𝑋) = Pred(⦋𝐴 / 𝑥⦌𝑅, ⦋𝐴 / 𝑥⦌𝐷, ⦋𝐴 / 𝑥⦌𝑋))
Theorem	predpredss 6306	If 𝐴 is a subset of 𝐵, then their predecessor classes are also subsets. (Contributed by Scott Fenton, 2-Feb-2011.)
⊢ (𝐴 ⊆ 𝐵 → Pred(𝑅, 𝐴, 𝑋) ⊆ Pred(𝑅, 𝐵, 𝑋))
Theorem	predss 6307	The predecessor class of 𝐴 is a subset of 𝐴. (Contributed by Scott Fenton, 2-Feb-2011.)
⊢ Pred(𝑅, 𝐴, 𝑋) ⊆ 𝐴
Theorem	sspred 6308	Another subset/predecessor class relationship. (Contributed by Scott Fenton, 6-Feb-2011.)
⊢ ((𝐵 ⊆ 𝐴 ∧ Pred(𝑅, 𝐴, 𝑋) ⊆ 𝐵) → Pred(𝑅, 𝐴, 𝑋) = Pred(𝑅, 𝐵, 𝑋))
Theorem	dfpred2 6309*	An alternate definition of predecessor class when 𝑋 is a set. (Contributed by Scott Fenton, 8-Feb-2011.)
⊢ 𝑋 ∈ V    ⇒   ⊢ Pred(𝑅, 𝐴, 𝑋) = (𝐴 ∩ {𝑦 ∣ 𝑦𝑅𝑋})
Theorem	dfpred3 6310*	An alternate definition of predecessor class when 𝑋 is a set. (Contributed by Scott Fenton, 13-Jun-2018.)
⊢ 𝑋 ∈ V    ⇒   ⊢ Pred(𝑅, 𝐴, 𝑋) = {𝑦 ∈ 𝐴 ∣ 𝑦𝑅𝑋}
Theorem	dfpred3g 6311*	An alternate definition of predecessor class when 𝑋 is a set. (Contributed by Scott Fenton, 13-Jun-2018.)
⊢ (𝑋 ∈ 𝑉 → Pred(𝑅, 𝐴, 𝑋) = {𝑦 ∈ 𝐴 ∣ 𝑦𝑅𝑋})
Theorem	elpredgg 6312	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 6313	Membership in a predecessor class. (Contributed by Scott Fenton, 17-Apr-2011.) (Proof shortened by BJ, 16-Oct-2024.)
⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐴) → (𝑌 ∈ Pred(𝑅, 𝐴, 𝑋) ↔ 𝑌𝑅𝑋))
Theorem	elpredimg 6314	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 6315	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 6316	Membership in a predecessor class. (Contributed by Scott Fenton, 4-Feb-2011.) (Proof shortened by BJ, 16-Oct-2024.)
⊢ 𝑌 ∈ V    ⇒   ⊢ (𝑋 ∈ 𝐷 → (𝑌 ∈ Pred(𝑅, 𝐴, 𝑋) ↔ (𝑌 ∈ 𝐴 ∧ 𝑌𝑅𝑋)))
Theorem	predexg 6317	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 6318	Obsolete form of predexg 6317 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 6319*	Alternate definition of well-founded relation. (Contributed by Scott Fenton, 2-Feb-2011.)
⊢ (𝑅 Fr 𝐴 ↔ ∀𝑥((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) → ∃𝑦 ∈ 𝑥 Pred(𝑅, 𝑥, 𝑦) = ∅))
Theorem	predel 6320	Membership in the predecessor class implies membership in the base class. (Contributed by Scott Fenton, 11-Feb-2011.)
⊢ (𝑌 ∈ Pred(𝑅, 𝐴, 𝑋) → 𝑌 ∈ 𝐴)
Theorem	predbrg 6321	Closed form of elpredim 6315. (Contributed by Scott Fenton, 13-Apr-2011.) (Revised by NM, 5-Apr-2016.)
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ Pred(𝑅, 𝐴, 𝑋)) → 𝑌𝑅𝑋)
Theorem	predtrss 6322	If 𝑅 is transitive over 𝐴 and 𝑌𝑅𝑋, then Pred(𝑅, 𝐴, 𝑌) is a subclass of Pred(𝑅, 𝐴, 𝑋). (Contributed by Scott Fenton, 28-Oct-2024.)
⊢ ((((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅 ∧ 𝑌 ∈ Pred(𝑅, 𝐴, 𝑋) ∧ 𝑋 ∈ 𝐴) → Pred(𝑅, 𝐴, 𝑌) ⊆ Pred(𝑅, 𝐴, 𝑋))
Theorem	predpo 6323	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 6324	Property of the predecessor class for strict total orders. (Contributed by Scott Fenton, 11-Feb-2011.)
⊢ ((𝑅 Or 𝐴 ∧ 𝑋 ∈ 𝐴) → (𝑌 ∈ Pred(𝑅, 𝐴, 𝑋) → Pred(𝑅, 𝐴, 𝑌) ⊆ Pred(𝑅, 𝐴, 𝑋)))
Theorem	setlikespec 6325	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 6326	Idempotent law for the predecessor class. (Contributed by Scott Fenton, 29-Mar-2011.)
⊢ Pred(𝑅, Pred(𝑅, 𝐴, 𝑋), 𝑋) = Pred(𝑅, 𝐴, 𝑋)
Theorem	predin 6327	Intersection law for predecessor classes. (Contributed by Scott Fenton, 29-Mar-2011.)
⊢ Pred(𝑅, (𝐴 ∩ 𝐵), 𝑋) = (Pred(𝑅, 𝐴, 𝑋) ∩ Pred(𝑅, 𝐵, 𝑋))
Theorem	predun 6328	Union law for predecessor classes. (Contributed by Scott Fenton, 29-Mar-2011.)
⊢ Pred(𝑅, (𝐴 ∪ 𝐵), 𝑋) = (Pred(𝑅, 𝐴, 𝑋) ∪ Pred(𝑅, 𝐵, 𝑋))
Theorem	preddif 6329	Difference law for predecessor classes. (Contributed by Scott Fenton, 14-Apr-2011.)
⊢ Pred(𝑅, (𝐴 ∖ 𝐵), 𝑋) = (Pred(𝑅, 𝐴, 𝑋) ∖ Pred(𝑅, 𝐵, 𝑋))
Theorem	predep 6330	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 6331	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 6332*	A property of classes that are downward closed under predecessor. (Contributed by Scott Fenton, 13-Apr-2011.)
⊢ ((𝐵 ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝐵 Pred(𝑅, 𝐴, 𝑥) ⊆ 𝐵) → (𝑋 ∈ 𝐵 → Pred(𝑅, 𝐵, 𝑋) = Pred(𝑅, 𝐴, 𝑋)))
Theorem	predpoirr 6333	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 6334	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 6335	The predecessor class over ∅ is always ∅. (Contributed by Scott Fenton, 16-Apr-2011.) (Proof shortened by AV, 11-Jun-2021.)
⊢ Pred(𝑅, ∅, 𝑋) = ∅
Theorem	dfse3 6336*	Alternate definition of set-like relationships. (Contributed by Scott Fenton, 19-Aug-2024.)
⊢ (𝑅 Se 𝐴 ↔ ∀𝑥 ∈ 𝐴 Pred(𝑅, 𝐴, 𝑥) ∈ V)
Theorem	predrelss 6337	Subset carries from relation to predecessor class. (Contributed by Scott Fenton, 25-Nov-2024.)
⊢ (𝑅 ⊆ 𝑆 → Pred(𝑅, 𝐴, 𝑋) ⊆ Pred(𝑆, 𝐴, 𝑋))
Theorem	predprc 6338	The predecessor of a proper class is empty. (Contributed by Scott Fenton, 25-Nov-2024.)
⊢ (¬ 𝑋 ∈ V → Pred(𝑅, 𝐴, 𝑋) = ∅)
Theorem	predres 6339	Predecessor class is unaffected by restriction to the base class. (Contributed by Scott Fenton, 25-Nov-2024.)
⊢ Pred(𝑅, 𝐴, 𝑋) = Pred((𝑅 ↾ 𝐴), 𝐴, 𝑋)
2.3.12  Well-founded induction (variant)
Theorem	frpomin 6340*	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 9746 enables avoiding the axiom of infinity. (Contributed by Scott Fenton, 11-Feb-2022.)
⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅)) → ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥)
Theorem	frpomin2 6341*	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 9746 enables avoiding the axiom of infinity. (Contributed by Scott Fenton, 11-Feb-2022.)
⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅)) → ∃𝑥 ∈ 𝐵 Pred(𝑅, 𝐵, 𝑥) = ∅)
Theorem	frpoind 6342*	The principle of well-founded induction over a partial order. This theorem is a version of frind 9747 that does not require the axiom of infinity and can be used to prove wfi 6350 and tfi 7844. (Contributed by Scott Fenton, 11-Feb-2022.)
⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝐵 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝐴 (Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵 → 𝑦 ∈ 𝐵))) → 𝐴 = 𝐵)
Theorem	frpoinsg 6343*	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 6344*	Well-Founded Induction schema, using implicit substitution. (Contributed by Scott Fenton, 24-Aug-2022.)
⊢ (𝑦 ∈ 𝐴 → (∀𝑧 ∈ Pred (𝑅, 𝐴, 𝑦)𝜓 → 𝜑))    &   ⊢ Ⅎ𝑦𝜓    &   ⊢ (𝑦 = 𝑧 → (𝜑 ↔ 𝜓))    ⇒   ⊢ ((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) → ∀𝑦 ∈ 𝐴 𝜑)
Theorem	frpoins2g 6345*	Well-Founded Induction schema, using implicit substitution. (Contributed by Scott Fenton, 24-Aug-2022.)
⊢ (𝑦 ∈ 𝐴 → (∀𝑧 ∈ Pred (𝑅, 𝐴, 𝑦)𝜓 → 𝜑))    &   ⊢ (𝑦 = 𝑧 → (𝜑 ↔ 𝜓))    ⇒   ⊢ ((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) → ∀𝑦 ∈ 𝐴 𝜑)
Theorem	frpoins3g 6346*	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 6347*	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 6348*	Obsolete proof of tz6.26 6347 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 6349*	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 6350*	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 6351*	Obsolete proof of wfi 6350 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 6352*	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 6353*	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 6354*	Obsolete version of wfisg 6353 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 6355*	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 6356*	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 6357*	Obsolete version of wfis2fg 6356 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 6358*	Well-Ordered Induction schema, using implicit substitution. (Contributed by Scott Fenton, 29-Jan-2011.)
⊢ 𝑅 We 𝐴    &   ⊢ 𝑅 Se 𝐴    &   ⊢ Ⅎ𝑦𝜓    &   ⊢ (𝑦 = 𝑧 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑦 ∈ 𝐴 → (∀𝑧 ∈ Pred (𝑅, 𝐴, 𝑦)𝜓 → 𝜑))    ⇒   ⊢ (𝑦 ∈ 𝐴 → 𝜑)
Theorem	wfis2g 6359*	Well-Ordered Induction Schema, using implicit substitution. (Contributed by Scott Fenton, 11-Feb-2011.)
⊢ (𝑦 = 𝑧 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑦 ∈ 𝐴 → (∀𝑧 ∈ Pred (𝑅, 𝐴, 𝑦)𝜓 → 𝜑))    ⇒   ⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴) → ∀𝑦 ∈ 𝐴 𝜑)
Theorem	wfis2 6360*	Well-Ordered Induction schema, using implicit substitution. (Contributed by Scott Fenton, 29-Jan-2011.)
⊢ 𝑅 We 𝐴    &   ⊢ 𝑅 Se 𝐴    &   ⊢ (𝑦 = 𝑧 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑦 ∈ 𝐴 → (∀𝑧 ∈ Pred (𝑅, 𝐴, 𝑦)𝜓 → 𝜑))    ⇒   ⊢ (𝑦 ∈ 𝐴 → 𝜑)
Theorem	wfis3 6361*	Well-Ordered Induction schema, using implicit substitution. (Contributed by Scott Fenton, 29-Jan-2011.)
⊢ 𝑅 We 𝐴    &   ⊢ 𝑅 Se 𝐴    &   ⊢ (𝑦 = 𝑧 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑦 = 𝐵 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑦 ∈ 𝐴 → (∀𝑧 ∈ Pred (𝑅, 𝐴, 𝑦)𝜓 → 𝜑))    ⇒   ⊢ (𝐵 ∈ 𝐴 → 𝜒)
2.3.14  Ordinals
Syntax	word 6362	Extend the definition of a wff to include the ordinal predicate.
wff Ord 𝐴
Syntax	con0 6363	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 6364	Extend the definition of a wff to include the limit ordinal predicate.
wff Lim 𝐴
Syntax	csuc 6365	Extend class notation to include the successor function.
class suc 𝐴
Definition	df-ord 6366	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 6367	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 6368	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 6420, dflim3 7838, and dflim4 for alternate definitions. (Contributed by NM, 22-Apr-1994.)
⊢ (Lim 𝐴 ↔ (Ord 𝐴 ∧ 𝐴 ≠ ∅ ∧ 𝐴 = ∪ 𝐴))
Definition	df-suc 6369	Define the successor of a class. When applied to an ordinal number, the successor means the same thing as "plus 1" (see oa1suc 8533). Definition 7.22 of [TakeutiZaring] p. 41, who use "+ 1" to denote this function. Definition 1.4 of [Schloeder] p. 1, similarly. 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 6439), so that the successor of any ordinal class is still an ordinal class (ordsuc 7803), 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 6370	Equality theorem for the ordinal predicate. (Contributed by NM, 17-Sep-1993.)
⊢ (𝐴 = 𝐵 → (Ord 𝐴 ↔ Ord 𝐵))
Theorem	elong 6371	An ordinal number is an ordinal set. (Contributed by NM, 5-Jun-1994.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ On ↔ Ord 𝐴))
Theorem	elon 6372	An ordinal number is an ordinal set. (Contributed by NM, 5-Jun-1994.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 ∈ On ↔ Ord 𝐴)
Theorem	eloni 6373	An ordinal number has the ordinal property. (Contributed by NM, 5-Jun-1994.)
⊢ (𝐴 ∈ On → Ord 𝐴)
Theorem	elon2 6374	An ordinal number is an ordinal set. Part of Definition 1.2 of [Schloeder] p. 1. (Contributed by NM, 8-Feb-2004.)
⊢ (𝐴 ∈ On ↔ (Ord 𝐴 ∧ 𝐴 ∈ V))
Theorem	limeq 6375	Equality theorem for the limit predicate. (Contributed by NM, 22-Apr-1994.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
⊢ (𝐴 = 𝐵 → (Lim 𝐴 ↔ Lim 𝐵))
Theorem	ordwe 6376	Membership well-orders every ordinal. Proposition 7.4 of [TakeutiZaring] p. 36. (Contributed by NM, 3-Apr-1994.)
⊢ (Ord 𝐴 → E We 𝐴)
Theorem	ordtr 6377	An ordinal class is transitive. (Contributed by NM, 3-Apr-1994.)
⊢ (Ord 𝐴 → Tr 𝐴)
Theorem	ordfr 6378	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 6379	An element of an ordinal class is a subset of it. (Contributed by NM, 30-May-1994.)
⊢ ((Ord 𝐴 ∧ 𝐵 ∈ 𝐴) → 𝐵 ⊆ 𝐴)
Theorem	trssord 6380	A transitive subclass of an ordinal class is ordinal. (Contributed by NM, 29-May-1994.)
⊢ ((Tr 𝐴 ∧ 𝐴 ⊆ 𝐵 ∧ Ord 𝐵) → Ord 𝐴)
Theorem	ordirr 6381	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. Theorem 1.9(i) of [Schloeder] p. 1. We prove this without invoking the Axiom of Regularity. (Contributed by NM, 2-Jan-1994.)
⊢ (Ord 𝐴 → ¬ 𝐴 ∈ 𝐴)
Theorem	nordeq 6382	A member of an ordinal class is not equal to it. (Contributed by NM, 25-May-1998.)
⊢ ((Ord 𝐴 ∧ 𝐵 ∈ 𝐴) → 𝐴 ≠ 𝐵)
Theorem	ordn2lp 6383	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 6384*	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 6385	An element of an ordinal class is ordinal. Proposition 7.6 of [TakeutiZaring] p. 36. Lemma 1.3 of [Schloeder] p. 1. (Contributed by NM, 23-Apr-1994.)
⊢ ((Ord 𝐴 ∧ 𝐵 ∈ 𝐴) → Ord 𝐵)
Theorem	tron 6386	The class of all ordinal numbers is transitive. (Contributed by NM, 4-May-2009.)
⊢ Tr On
Theorem	ordelon 6387	An element of an ordinal class is an ordinal number. Lemma 1.3 of [Schloeder] p. 1. (Contributed by NM, 26-Oct-2003.)
⊢ ((Ord 𝐴 ∧ 𝐵 ∈ 𝐴) → 𝐵 ∈ On)
Theorem	onelon 6388	An element of an ordinal number is an ordinal number. Theorem 2.2(iii) of [BellMachover] p. 469. Lemma 1.3 of [Schloeder] p. 1. (Contributed by NM, 26-Oct-2003.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ 𝐴) → 𝐵 ∈ On)
Theorem	tz7.7 6389	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 6390	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 6391	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 6392	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 6393	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 6394	The intersection of two ordinal numbers is an ordinal number. (Contributed by NM, 7-Apr-1995.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ∩ 𝐵) ∈ On)
Theorem	ordtri3or 6395	A trichotomy law for ordinals. Proposition 7.10 of [TakeutiZaring] p. 38. Theorem 1.9(iii) of [Schloeder] p. 1. (Contributed by NM, 10-May-1994.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴))
Theorem	ordtri1 6396	A trichotomy law for ordinals. (Contributed by NM, 25-Mar-1995.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴 ⊆ 𝐵 ↔ ¬ 𝐵 ∈ 𝐴))
Theorem	ontri1 6397	A trichotomy law for ordinal numbers. (Contributed by NM, 6-Nov-2003.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ⊆ 𝐵 ↔ ¬ 𝐵 ∈ 𝐴))
Theorem	ordtri2 6398	A trichotomy law for ordinals. (Contributed by NM, 25-Nov-1995.)
⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴 ∈ 𝐵 ↔ ¬ (𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴)))
Theorem	ordtri3 6399	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 6400	A trichotomy law for ordinals. (Contributed by NM, 1-Nov-2003.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ ¬ 𝐴 ∈ 𝐵)))