P. 85 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 8401-8500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	smoord 8401	A strictly monotone ordinal function preserves strict ordering. (Contributed by Mario Carneiro, 4-Mar-2013.)
⊢ (((𝐹 Fn 𝐴 ∧ Smo 𝐹) ∧ (𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → (𝐶 ∈ 𝐷 ↔ (𝐹‘𝐶) ∈ (𝐹‘𝐷)))
Theorem	smoword 8402	A strictly monotone ordinal function preserves weak ordering. (Contributed by Mario Carneiro, 4-Mar-2013.)
⊢ (((𝐹 Fn 𝐴 ∧ Smo 𝐹) ∧ (𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → (𝐶 ⊆ 𝐷 ↔ (𝐹‘𝐶) ⊆ (𝐹‘𝐷)))
Theorem	smogt 8403	A strictly monotone ordinal function is greater than or equal to its argument. Exercise 1 in [TakeutiZaring] p. 50. (Contributed by Andrew Salmon, 23-Nov-2011.) (Revised by Mario Carneiro, 28-Feb-2013.)
⊢ ((𝐹 Fn 𝐴 ∧ Smo 𝐹 ∧ 𝐶 ∈ 𝐴) → 𝐶 ⊆ (𝐹‘𝐶))
Theorem	smocdmdom 8404	The codomain of a strictly monotone ordinal function dominates the domain. (Contributed by Mario Carneiro, 13-Mar-2013.)
⊢ ((𝐹:𝐴⟶𝐵 ∧ Smo 𝐹 ∧ Ord 𝐵) → 𝐴 ⊆ 𝐵)
Theorem	smoiso2 8405	The strictly monotone ordinal functions are also isomorphisms of subclasses of On equipped with the membership relation. (Contributed by Mario Carneiro, 20-Mar-2013.)
⊢ ((Ord 𝐴 ∧ 𝐵 ⊆ On) → ((𝐹:𝐴⟶onto𝐵 ∧ Smo 𝐹) ↔ 𝐹 Isom E , E (𝐴, 𝐵)))
2.4.20  "Strong" transfinite recursion
Syntax	crecs 8406	Notation for a function defined by strong transfinite recursion.
class recs(𝐹)
Definition	df-recs 8407	Define a function recs(𝐹) on On, the class of ordinal numbers, by transfinite recursion given a rule 𝐹 which sets the next value given all values so far. See df-rdg 8446 for more details on why this definition is desirable. Unlike df-rdg 8446 which restricts the update rule to use only the previous value, this version allows the update rule to use all previous values, which is why it is described as "strong", although it is actually more primitive. See recsfnon 8439 and recsval 8440 for the primary contract of this definition. (Contributed by Stefan O'Rear, 18-Jan-2015.) (Revised by Scott Fenton, 3-Aug-2020.)
⊢ recs(𝐹) = wrecs( E , On, 𝐹)
Theorem	dfrecs3 8408*	The old definition of transfinite recursion. This version is preferred for development, as it demonstrates the properties of transfinite recursion without relying on well-ordered recursion. (Contributed by Scott Fenton, 3-Aug-2020.) (Proof revised by Scott Fenton, 18-Nov-2024.)
⊢ recs(𝐹) = ∪ {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))}
Theorem	recseq 8409	Equality theorem for recs. (Contributed by Stefan O'Rear, 18-Jan-2015.)
⊢ (𝐹 = 𝐺 → recs(𝐹) = recs(𝐺))
Theorem	nfrecs 8410	Bound-variable hypothesis builder for recs. (Contributed by Stefan O'Rear, 18-Jan-2015.)
⊢ Ⅎ𝑥𝐹    ⇒   ⊢ Ⅎ𝑥recs(𝐹)
Theorem	tfrlem1 8411*	A technical lemma for transfinite recursion. Compare Lemma 1 of [TakeutiZaring] p. 47. (Contributed by NM, 23-Mar-1995.) (Revised by Mario Carneiro, 24-May-2019.)
⊢ (𝜑 → 𝐴 ∈ On)    &   ⊢ (𝜑 → (Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹))    &   ⊢ (𝜑 → (Fun 𝐺 ∧ 𝐴 ⊆ dom 𝐺))    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐵‘(𝐹 ↾ 𝑥)))    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 (𝐺‘𝑥) = (𝐵‘(𝐺 ↾ 𝑥)))    ⇒   ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐺‘𝑥))
Theorem	tfrlem3a 8412*	Lemma for transfinite recursion. Let 𝐴 be the class of "acceptable" functions. The final thing we're interested in is the union of all these acceptable functions. This lemma just changes some bound variables in 𝐴 for later use. (Contributed by NM, 9-Apr-1995.)
⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))}    &   ⊢ 𝐺 ∈ V    ⇒   ⊢ (𝐺 ∈ 𝐴 ↔ ∃𝑧 ∈ On (𝐺 Fn 𝑧 ∧ ∀𝑤 ∈ 𝑧 (𝐺‘𝑤) = (𝐹‘(𝐺 ↾ 𝑤))))
Theorem	tfrlem3 8413*	Lemma for transfinite recursion. Let 𝐴 be the class of "acceptable" functions. The final thing we're interested in is the union of all these acceptable functions. This lemma just changes some bound variables in 𝐴 for later use. (Contributed by NM, 9-Apr-1995.)
⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))}    ⇒   ⊢ 𝐴 = {𝑔 ∣ ∃𝑧 ∈ On (𝑔 Fn 𝑧 ∧ ∀𝑤 ∈ 𝑧 (𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤)))}
Theorem	tfrlem4 8414*	Lemma for transfinite recursion. 𝐴 is the class of all "acceptable" functions, and 𝐹 is their union. First we show that an acceptable function is in fact a function. (Contributed by NM, 9-Apr-1995.)
⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))}    ⇒   ⊢ (𝑔 ∈ 𝐴 → Fun 𝑔)
Theorem	tfrlem5 8415*	Lemma for transfinite recursion. The values of two acceptable functions are the same within their domains. (Contributed by NM, 9-Apr-1995.) (Revised by Mario Carneiro, 24-May-2019.)
⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))}    ⇒   ⊢ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐴) → ((𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣) → 𝑢 = 𝑣))
Theorem	recsfval 8416*	Lemma for transfinite recursion. The definition recs is the union of all acceptable functions. (Contributed by Mario Carneiro, 9-May-2015.)
⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))}    ⇒   ⊢ recs(𝐹) = ∪ 𝐴
Theorem	tfrlem6 8417*	Lemma for transfinite recursion. The union of all acceptable functions is a relation. (Contributed by NM, 8-Aug-1994.) (Revised by Mario Carneiro, 9-May-2015.) Avoid ax-10 2180, ax-nul 5263, ax-pr 5395, ax-sep 5252 and ax-un 7775. (Revised by Umit Teoman Dogan, 10-Jun-2026.)
⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))}    ⇒   ⊢ Rel recs(𝐹)
Theorem	tfrlem6OLD 8418*	Obsolete version of tfrlem6 8417 as of 10-Jun-2026. (Contributed by NM, 8-Aug-1994.) (Revised by Mario Carneiro, 9-May-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))}    ⇒   ⊢ Rel recs(𝐹)
Theorem	tfrlem7 8419*	Lemma for transfinite recursion. The union of all acceptable functions is a function. (Contributed by NM, 9-Aug-1994.) (Revised by Mario Carneiro, 24-May-2019.)
⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))}    ⇒   ⊢ Fun recs(𝐹)
Theorem	tfrlem8 8420*	Lemma for transfinite recursion. The domain of recs is an ordinal. (Contributed by NM, 14-Aug-1994.) (Proof shortened by Alan Sare, 11-Mar-2008.)
⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))}    ⇒   ⊢ Ord dom recs(𝐹)
Theorem	tfrlem9 8421*	Lemma for transfinite recursion. Here we compute the value of recs (the union of all acceptable functions). (Contributed by NM, 17-Aug-1994.)
⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))}    ⇒   ⊢ (𝐵 ∈ dom recs(𝐹) → (recs(𝐹)‘𝐵) = (𝐹‘(recs(𝐹) ↾ 𝐵)))
Theorem	tfrlem9a 8422*	Lemma for transfinite recursion. Without using ax-rep 5235, show that all the restrictions of recs are sets. (Contributed by Mario Carneiro, 16-Nov-2014.)
⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))}    ⇒   ⊢ (𝐵 ∈ dom recs(𝐹) → (recs(𝐹) ↾ 𝐵) ∈ V)
Theorem	tfrlem10 8423*	Lemma for transfinite recursion. We define class 𝐶 by extending recs with one ordered pair. We will assume, falsely, that domain of recs is a member of, and thus not equal to, On. Using this assumption we will prove facts about 𝐶 that will lead to a contradiction in tfrlem14 8427, thus showing the domain of recs does in fact equal On. Here we show (under the false assumption) that 𝐶 is a function extending the domain of recs(𝐹) by one. (Contributed by NM, 14-Aug-1994.) (Revised by Mario Carneiro, 9-May-2015.)
⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))}    &   ⊢ 𝐶 = (recs(𝐹) ∪ {⟨dom recs(𝐹), (𝐹‘recs(𝐹))⟩})    ⇒   ⊢ (dom recs(𝐹) ∈ On → 𝐶 Fn suc dom recs(𝐹))
Theorem	tfrlem11 8424*	Lemma for transfinite recursion. Compute the value of 𝐶. (Contributed by NM, 18-Aug-1994.) (Revised by Mario Carneiro, 9-May-2015.)
⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))}    &   ⊢ 𝐶 = (recs(𝐹) ∪ {⟨dom recs(𝐹), (𝐹‘recs(𝐹))⟩})    ⇒   ⊢ (dom recs(𝐹) ∈ On → (𝐵 ∈ suc dom recs(𝐹) → (𝐶‘𝐵) = (𝐹‘(𝐶 ↾ 𝐵))))
Theorem	tfrlem12 8425*	Lemma for transfinite recursion. Show 𝐶 is an acceptable function. (Contributed by NM, 15-Aug-1994.) (Revised by Mario Carneiro, 9-May-2015.)
⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))}    &   ⊢ 𝐶 = (recs(𝐹) ∪ {⟨dom recs(𝐹), (𝐹‘recs(𝐹))⟩})    ⇒   ⊢ (recs(𝐹) ∈ V → 𝐶 ∈ 𝐴)
Theorem	tfrlem13 8426*	Lemma for transfinite recursion. If recs is a set function, then 𝐶 is acceptable, and thus a subset of recs, but dom 𝐶 is bigger than dom recs. This is a contradiction, so recs must be a proper class function. (Contributed by NM, 14-Aug-1994.) (Revised by Mario Carneiro, 14-Nov-2014.)
⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))}    ⇒   ⊢ ¬ recs(𝐹) ∈ V
Theorem	tfrlem14 8427*	Lemma for transfinite recursion. Assuming ax-rep 5235, dom recs ∈ V ↔ recs ∈ V, so since dom recs is an ordinal, it must be equal to On. (Contributed by NM, 14-Aug-1994.) (Revised by Mario Carneiro, 9-May-2015.)
⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))}    ⇒   ⊢ dom recs(𝐹) = On
Theorem	tfrlem15 8428*	Lemma for transfinite recursion. Without assuming ax-rep 5235, we can show that all proper initial subsets of recs are sets, while nothing larger is a set. (Contributed by Mario Carneiro, 14-Nov-2014.)
⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))}    ⇒   ⊢ (𝐵 ∈ On → (𝐵 ∈ dom recs(𝐹) ↔ (recs(𝐹) ↾ 𝐵) ∈ V))
Theorem	tfrlem16 8429*	Lemma for finite recursion. Without assuming ax-rep 5235, we can show that the domain of the constructed function is a limit ordinal, and hence contains all the finite ordinals. (Contributed by Mario Carneiro, 14-Nov-2014.)
⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))}    ⇒   ⊢ Lim dom recs(𝐹)
Theorem	tfr1a 8430	A weak version of tfr1 8433 which is useful for proofs that avoid the Axiom of Replacement. (Contributed by Mario Carneiro, 24-Jun-2015.)
⊢ 𝐹 = recs(𝐺)    ⇒   ⊢ (Fun 𝐹 ∧ Lim dom 𝐹)
Theorem	tfr2a 8431	A weak version of tfr2 8434 which is useful for proofs that avoid the Axiom of Replacement. (Contributed by Mario Carneiro, 24-Jun-2015.)
⊢ 𝐹 = recs(𝐺)    ⇒   ⊢ (𝐴 ∈ dom 𝐹 → (𝐹‘𝐴) = (𝐺‘(𝐹 ↾ 𝐴)))
Theorem	tfr2b 8432	Without assuming ax-rep 5235, we can show that all proper initial subsets of recs are sets, while nothing larger is a set. (Contributed by Mario Carneiro, 24-Jun-2015.)
⊢ 𝐹 = recs(𝐺)    ⇒   ⊢ (Ord 𝐴 → (𝐴 ∈ dom 𝐹 ↔ (𝐹 ↾ 𝐴) ∈ V))
Theorem	tfr1 8433	Principle of Transfinite Recursion, part 1 of 3. Theorem 7.41(1) of [TakeutiZaring] p. 47. We start with an arbitrary class 𝐺, normally a function, and define a class 𝐴 of all "acceptable" functions. The final function we're interested in is the union 𝐹 = recs(𝐺) of them. 𝐹 is then said to be defined by transfinite recursion. The purpose of the 3 parts of this theorem is to demonstrate properties of 𝐹. In this first part we show that 𝐹 is a function whose domain is all ordinal numbers. (Contributed by NM, 17-Aug-1994.) (Revised by Mario Carneiro, 18-Jan-2015.)
⊢ 𝐹 = recs(𝐺)    ⇒   ⊢ 𝐹 Fn On
Theorem	tfr2 8434	Principle of Transfinite Recursion, part 2 of 3. Theorem 7.41(2) of [TakeutiZaring] p. 47. Here we show that the function 𝐹 has the property that for any function 𝐺 whatsoever, the "next" value of 𝐹 is 𝐺 recursively applied to all "previous" values of 𝐹. (Contributed by NM, 9-Apr-1995.) (Revised by Stefan O'Rear, 18-Jan-2015.)
⊢ 𝐹 = recs(𝐺)    ⇒   ⊢ (𝐴 ∈ On → (𝐹‘𝐴) = (𝐺‘(𝐹 ↾ 𝐴)))
Theorem	tfr3 8435*	Principle of Transfinite Recursion, part 3 of 3. Theorem 7.41(3) of [TakeutiZaring] p. 47. Finally, we show that 𝐹 is unique. We do this by showing that any class 𝐵 with the same properties of 𝐹 that we showed in parts 1 and 2 is identical to 𝐹. (Contributed by NM, 18-Aug-1994.) (Revised by Mario Carneiro, 9-May-2015.)
⊢ 𝐹 = recs(𝐺)    ⇒   ⊢ ((𝐵 Fn On ∧ ∀𝑥 ∈ On (𝐵‘𝑥) = (𝐺‘(𝐵 ↾ 𝑥))) → 𝐵 = 𝐹)
Theorem	tfr1ALT 8436	Alternate proof of tfr1 8433 using well-ordered recursion. (Contributed by Scott Fenton, 3-Aug-2020.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝐹 = recs(𝐺)    ⇒   ⊢ 𝐹 Fn On
Theorem	tfr2ALT 8437	Alternate proof of tfr2 8434 using well-ordered recursion. (Contributed by Scott Fenton, 3-Aug-2020.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝐹 = recs(𝐺)    ⇒   ⊢ (𝐴 ∈ On → (𝐹‘𝐴) = (𝐺‘(𝐹 ↾ 𝐴)))
Theorem	tfr3ALT 8438*	Alternate proof of tfr3 8435 using well-ordered recursion. (Contributed by Scott Fenton, 3-Aug-2020.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝐹 = recs(𝐺)    ⇒   ⊢ ((𝐵 Fn On ∧ ∀𝑥 ∈ On (𝐵‘𝑥) = (𝐺‘(𝐵 ↾ 𝑥))) → 𝐵 = 𝐹)
Theorem	recsfnon 8439	Strong transfinite recursion defines a function on ordinals. (Contributed by Stefan O'Rear, 18-Jan-2015.)
⊢ recs(𝐹) Fn On
Theorem	recsval 8440	Strong transfinite recursion in terms of all previous values. (Contributed by Stefan O'Rear, 18-Jan-2015.)
⊢ (𝐴 ∈ On → (recs(𝐹)‘𝐴) = (𝐹‘(recs(𝐹) ↾ 𝐴)))
Theorem	tz7.44lem1 8441*	The ordered pair abstraction 𝐺 defined in the hypothesis is a function. This was a lemma for tz7.44-1 8442, tz7.44-2 8443, and tz7.44-3 8444 when they used that definition of 𝐺. Now, they use the maps-to df-mpt 5190 idiom so this lemma is not needed anymore, but is kept in case other applications (for instance in intuitionistic set theory) need it. (Contributed by NM, 23-Apr-1995.) (Revised by David Abernethy, 19-Jun-2012.)
⊢ 𝐺 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 = ∅ ∧ 𝑦 = 𝐴) ∨ (¬ (𝑥 = ∅ ∨ Lim dom 𝑥) ∧ 𝑦 = (𝐻‘(𝑥‘∪ dom 𝑥))) ∨ (Lim dom 𝑥 ∧ 𝑦 = ∪ ran 𝑥))}    ⇒   ⊢ Fun 𝐺
Theorem	tz7.44-1 8442*	The value of 𝐹 at ∅. Part 1 of Theorem 7.44 of [TakeutiZaring] p. 49. (Contributed by NM, 23-Apr-1995.) (Revised by Mario Carneiro, 14-Nov-2014.)
⊢ 𝐺 = (𝑥 ∈ V ↦ if(𝑥 = ∅, 𝐴, if(Lim dom 𝑥, ∪ ran 𝑥, (𝐻‘(𝑥‘∪ dom 𝑥)))))    &   ⊢ (𝑦 ∈ 𝑋 → (𝐹‘𝑦) = (𝐺‘(𝐹 ↾ 𝑦)))    &   ⊢ 𝐴 ∈ V    ⇒   ⊢ (∅ ∈ 𝑋 → (𝐹‘∅) = 𝐴)
Theorem	tz7.44-2 8443*	The value of 𝐹 at a successor ordinal. Part 2 of Theorem 7.44 of [TakeutiZaring] p. 49. (Contributed by NM, 23-Apr-1995.) Remove unnecessary distinct variable conditions. (Revised by David Abernethy, 19-Jun-2012.) (Revised by Mario Carneiro, 14-Nov-2014.)
⊢ 𝐺 = (𝑥 ∈ V ↦ if(𝑥 = ∅, 𝐴, if(Lim dom 𝑥, ∪ ran 𝑥, (𝐻‘(𝑥‘∪ dom 𝑥)))))    &   ⊢ (𝑦 ∈ 𝑋 → (𝐹‘𝑦) = (𝐺‘(𝐹 ↾ 𝑦)))    &   ⊢ (𝑦 ∈ 𝑋 → (𝐹 ↾ 𝑦) ∈ V)    &   ⊢ 𝐹 Fn 𝑋    &   ⊢ Ord 𝑋    ⇒   ⊢ (suc 𝐵 ∈ 𝑋 → (𝐹‘suc 𝐵) = (𝐻‘(𝐹‘𝐵)))
Theorem	tz7.44-3 8444*	The value of 𝐹 at a limit ordinal. Part 3 of Theorem 7.44 of [TakeutiZaring] p. 49. (Contributed by NM, 23-Apr-1995.) (Revised by David Abernethy, 19-Jun-2012.)
⊢ 𝐺 = (𝑥 ∈ V ↦ if(𝑥 = ∅, 𝐴, if(Lim dom 𝑥, ∪ ran 𝑥, (𝐻‘(𝑥‘∪ dom 𝑥)))))    &   ⊢ (𝑦 ∈ 𝑋 → (𝐹‘𝑦) = (𝐺‘(𝐹 ↾ 𝑦)))    &   ⊢ (𝑦 ∈ 𝑋 → (𝐹 ↾ 𝑦) ∈ V)    &   ⊢ 𝐹 Fn 𝑋    &   ⊢ Ord 𝑋    ⇒   ⊢ ((𝐵 ∈ 𝑋 ∧ Lim 𝐵) → (𝐹‘𝐵) = ∪ (𝐹 “ 𝐵))
2.4.21  Recursive definition generator
Syntax	crdg 8445	Extend class notation with the recursive definition generator, with characteristic function 𝐹 and initial value 𝐼.
class rec(𝐹, 𝐼)
Definition	df-rdg 8446*	Define a recursive definition generator on On (the class of ordinal numbers) with characteristic function 𝐹 and initial value 𝐼. This combines functions 𝐹 in tfr1 8433 and 𝐺 in tz7.44-1 8442 into one definition. This rather amazing operation allows to define, with compact direct definitions, functions that are usually defined in textbooks only with indirect self-referencing recursive definitions. A recursive definition requires advanced metalogic to justify - in particular, eliminating a recursive definition is very difficult and often not even shown in textbooks. On the other hand, the elimination of a direct definition is a matter of simple mechanical substitution. The price paid is the daunting complexity of our rec operation (especially when df-recs 8407 that it is built on is also eliminated). But once we get past this hurdle, definitions that would otherwise be recursive become relatively simple, as in for example oav 8547, from which we prove the recursive textbook definition as Theorems oa0 8552, oasuc 8560, and oalim 8568 (with the help of Theorems rdg0 8457, rdgsuc 8460, and rdglim2a 8469). We can also restrict the rec operation to define otherwise recursive functions on the natural numbers ω; see fr0g 8472 and frsuc 8473. Our rec operation apparently does not appear in published literature, although closely related is Definition 25.2 of [Quine] p. 177, which he uses to "turn...a recursion into a genuine or direct definition" (p. 174). Note that the if operations (see df-if 4486) select cases based on whether the domain of 𝑔 is zero, a successor, or a limit ordinal. An important use of this definition is in the recursive sequence generator df-seq 14172 on the natural numbers (as a subset of the complex numbers), allowing us to define, with direct definitions, recursive infinite sequences such as the factorial function df-fac 14445 and integer powers df-exp 14232. Note: We introduce rec with the philosophical goal of being able to eliminate all definitions with direct mechanical substitution and to verify easily the soundness of definitions. Metamath itself has no built-in technical limitation that prevents multiple-part recursive definitions in the traditional textbook style. (Contributed by NM, 9-Apr-1995.) (Revised by Mario Carneiro, 9-May-2015.)
⊢ rec(𝐹, 𝐼) = recs((𝑔 ∈ V ↦ if(𝑔 = ∅, 𝐼, if(Lim dom 𝑔, ∪ ran 𝑔, (𝐹‘(𝑔‘∪ dom 𝑔))))))
Theorem	rdgeq1 8447	Equality theorem for the recursive definition generator. (Contributed by NM, 9-Apr-1995.) (Revised by Mario Carneiro, 9-May-2015.)
⊢ (𝐹 = 𝐺 → rec(𝐹, 𝐴) = rec(𝐺, 𝐴))
Theorem	rdgeq2 8448	Equality theorem for the recursive definition generator. (Contributed by NM, 9-Apr-1995.) (Revised by Mario Carneiro, 9-May-2015.)
⊢ (𝐴 = 𝐵 → rec(𝐹, 𝐴) = rec(𝐹, 𝐵))
Theorem	rdgeq12 8449	Equality theorem for the recursive definition generator. (Contributed by Scott Fenton, 28-Apr-2012.)
⊢ ((𝐹 = 𝐺 ∧ 𝐴 = 𝐵) → rec(𝐹, 𝐴) = rec(𝐺, 𝐵))
Theorem	nfrdg 8450	Bound-variable hypothesis builder for the recursive definition generator. (Contributed by NM, 14-Sep-2003.) (Revised by Mario Carneiro, 8-Sep-2013.)
⊢ Ⅎ𝑥𝐹    &   ⊢ Ⅎ𝑥𝐴    ⇒   ⊢ Ⅎ𝑥rec(𝐹, 𝐴)
Theorem	rdglem1 8451*	Lemma used with the recursive definition generator. This is a trivial lemma that just changes bound variables for later use. (Contributed by NM, 9-Apr-1995.)
⊢ {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐺‘(𝑓 ↾ 𝑦)))} = {𝑔 ∣ ∃𝑧 ∈ On (𝑔 Fn 𝑧 ∧ ∀𝑤 ∈ 𝑧 (𝑔‘𝑤) = (𝐺‘(𝑔 ↾ 𝑤)))}
Theorem	rdgfun 8452	The recursive definition generator is a function. (Contributed by Mario Carneiro, 16-Nov-2014.)
⊢ Fun rec(𝐹, 𝐴)
Theorem	rdgdmlim 8453	The domain of the recursive definition generator is a limit ordinal. (Contributed by NM, 16-Nov-2014.)
⊢ Lim dom rec(𝐹, 𝐴)
Theorem	rdgfnon 8454	The recursive definition generator is a function on ordinal numbers. (Contributed by NM, 9-Apr-1995.) (Revised by Mario Carneiro, 9-May-2015.)
⊢ rec(𝐹, 𝐴) Fn On
Theorem	rdgvalg 8455*	Value of the recursive definition generator. (Contributed by NM, 9-Apr-1995.) (Revised by Mario Carneiro, 8-Sep-2013.)
⊢ (𝐵 ∈ dom rec(𝐹, 𝐴) → (rec(𝐹, 𝐴)‘𝐵) = ((𝑔 ∈ V ↦ if(𝑔 = ∅, 𝐴, if(Lim dom 𝑔, ∪ ran 𝑔, (𝐹‘(𝑔‘∪ dom 𝑔)))))‘(rec(𝐹, 𝐴) ↾ 𝐵)))
Theorem	rdgval 8456*	Value of the recursive definition generator. (Contributed by NM, 9-Apr-1995.) (Revised by Mario Carneiro, 8-Sep-2013.)
⊢ (𝐵 ∈ On → (rec(𝐹, 𝐴)‘𝐵) = ((𝑔 ∈ V ↦ if(𝑔 = ∅, 𝐴, if(Lim dom 𝑔, ∪ ran 𝑔, (𝐹‘(𝑔‘∪ dom 𝑔)))))‘(rec(𝐹, 𝐴) ↾ 𝐵)))
Theorem	rdg0 8457	The initial value of the recursive definition generator. (Contributed by NM, 23-Apr-1995.) (Revised by Mario Carneiro, 14-Nov-2014.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (rec(𝐹, 𝐴)‘∅) = 𝐴
Theorem	rdgseg 8458	The initial segments of the recursive definition generator are sets. (Contributed by Mario Carneiro, 16-Nov-2014.)
⊢ (𝐵 ∈ dom rec(𝐹, 𝐴) → (rec(𝐹, 𝐴) ↾ 𝐵) ∈ V)
Theorem	rdgsucg 8459	The value of the recursive definition generator at a successor. (Contributed by NM, 16-Nov-2014.)
⊢ (𝐵 ∈ dom rec(𝐹, 𝐴) → (rec(𝐹, 𝐴)‘suc 𝐵) = (𝐹‘(rec(𝐹, 𝐴)‘𝐵)))
Theorem	rdgsuc 8460	The value of the recursive definition generator at a successor. (Contributed by NM, 23-Apr-1995.) (Revised by Mario Carneiro, 14-Nov-2014.)
⊢ (𝐵 ∈ On → (rec(𝐹, 𝐴)‘suc 𝐵) = (𝐹‘(rec(𝐹, 𝐴)‘𝐵)))
Theorem	rdglimg 8461	The value of the recursive definition generator at a limit ordinal. (Contributed by NM, 16-Nov-2014.)
⊢ ((𝐵 ∈ dom rec(𝐹, 𝐴) ∧ Lim 𝐵) → (rec(𝐹, 𝐴)‘𝐵) = ∪ (rec(𝐹, 𝐴) “ 𝐵))
Theorem	rdglim 8462	The value of the recursive definition generator at a limit ordinal. (Contributed by NM, 23-Apr-1995.) (Revised by Mario Carneiro, 14-Nov-2014.)
⊢ ((𝐵 ∈ 𝐶 ∧ Lim 𝐵) → (rec(𝐹, 𝐴)‘𝐵) = ∪ (rec(𝐹, 𝐴) “ 𝐵))
Theorem	rdg0g 8463	The initial value of the recursive definition generator. (Contributed by NM, 25-Apr-1995.)
⊢ (𝐴 ∈ 𝐶 → (rec(𝐹, 𝐴)‘∅) = 𝐴)
Theorem	rdgsucmptf 8464	The value of the recursive definition generator at a successor (special case where the characteristic function uses the map operation). (Contributed by NM, 22-Oct-2003.) (Revised by Mario Carneiro, 15-Oct-2016.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    &   ⊢ Ⅎ𝑥𝐷    &   ⊢ 𝐹 = rec((𝑥 ∈ V ↦ 𝐶), 𝐴)    &   ⊢ (𝑥 = (𝐹‘𝐵) → 𝐶 = 𝐷)    ⇒   ⊢ ((𝐵 ∈ On ∧ 𝐷 ∈ 𝑉) → (𝐹‘suc 𝐵) = 𝐷)
Theorem	rdgsucmptnf 8465	The value of the recursive definition generator at a successor (special case where the characteristic function is an ordered-pair class abstraction and where the mapping class 𝐷 is a proper class). This is a technical lemma that can be used together with rdgsucmptf 8464 to help eliminate redundant sethood antecedents. (Contributed by NM, 22-Oct-2003.) (Revised by Mario Carneiro, 15-Oct-2016.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    &   ⊢ Ⅎ𝑥𝐷    &   ⊢ 𝐹 = rec((𝑥 ∈ V ↦ 𝐶), 𝐴)    &   ⊢ (𝑥 = (𝐹‘𝐵) → 𝐶 = 𝐷)    ⇒   ⊢ (¬ 𝐷 ∈ V → (𝐹‘suc 𝐵) = ∅)
Theorem	rdgsucmpt2 8466*	This version of rdgsucmpt 8467 avoids the not-free hypothesis of rdgsucmptf 8464 by using two substitutions instead of one. (Contributed by Mario Carneiro, 11-Sep-2015.)
⊢ 𝐹 = rec((𝑥 ∈ V ↦ 𝐶), 𝐴)    &   ⊢ (𝑦 = 𝑥 → 𝐸 = 𝐶)    &   ⊢ (𝑦 = (𝐹‘𝐵) → 𝐸 = 𝐷)    ⇒   ⊢ ((𝐵 ∈ On ∧ 𝐷 ∈ 𝑉) → (𝐹‘suc 𝐵) = 𝐷)
Theorem	rdgsucmpt 8467*	The value of the recursive definition generator at a successor (special case where the characteristic function uses the map operation). (Contributed by Mario Carneiro, 9-Sep-2013.)
⊢ 𝐹 = rec((𝑥 ∈ V ↦ 𝐶), 𝐴)    &   ⊢ (𝑥 = (𝐹‘𝐵) → 𝐶 = 𝐷)    ⇒   ⊢ ((𝐵 ∈ On ∧ 𝐷 ∈ 𝑉) → (𝐹‘suc 𝐵) = 𝐷)
Theorem	rdglim2 8468*	The value of the recursive definition generator at a limit ordinal, in terms of the union of all smaller values. (Contributed by NM, 23-Apr-1995.)
⊢ ((𝐵 ∈ 𝐶 ∧ Lim 𝐵) → (rec(𝐹, 𝐴)‘𝐵) = ∪ {𝑦 ∣ ∃𝑥 ∈ 𝐵 𝑦 = (rec(𝐹, 𝐴)‘𝑥)})
Theorem	rdglim2a 8469*	The value of the recursive definition generator at a limit ordinal, in terms of indexed union of all smaller values. (Contributed by NM, 28-Jun-1998.)
⊢ ((𝐵 ∈ 𝐶 ∧ Lim 𝐵) → (rec(𝐹, 𝐴)‘𝐵) = ∪ 𝑥 ∈ 𝐵 (rec(𝐹, 𝐴)‘𝑥))
Theorem	rdg0n 8470	If 𝐴 is a proper class, then the recursive function generator at ∅ is the empty set. (Contributed by Scott Fenton, 31-Oct-2024.)
⊢ (¬ 𝐴 ∈ V → (rec(𝐹, 𝐴)‘∅) = ∅)
2.4.22  Finite recursion
Theorem	frfnom 8471	The function generated by finite recursive definition generation is a function on omega. (Contributed by NM, 15-Oct-1996.) (Revised by Mario Carneiro, 14-Nov-2014.)
⊢ (rec(𝐹, 𝐴) ↾ ω) Fn ω
Theorem	fr0g 8472	The initial value resulting from finite recursive definition generation. (Contributed by NM, 15-Oct-1996.)
⊢ (𝐴 ∈ 𝐵 → ((rec(𝐹, 𝐴) ↾ ω)‘∅) = 𝐴)
Theorem	frsuc 8473	The successor value resulting from finite recursive definition generation. (Contributed by NM, 15-Oct-1996.) (Revised by Mario Carneiro, 16-Nov-2014.)
⊢ (𝐵 ∈ ω → ((rec(𝐹, 𝐴) ↾ ω)‘suc 𝐵) = (𝐹‘((rec(𝐹, 𝐴) ↾ ω)‘𝐵)))
Theorem	frsucmpt 8474	The successor value resulting from finite recursive definition generation (special case where the generation function is expressed in maps-to notation). (Contributed by NM, 14-Sep-2003.) (Revised by Scott Fenton, 2-Nov-2011.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    &   ⊢ Ⅎ𝑥𝐷    &   ⊢ 𝐹 = (rec((𝑥 ∈ V ↦ 𝐶), 𝐴) ↾ ω)    &   ⊢ (𝑥 = (𝐹‘𝐵) → 𝐶 = 𝐷)    ⇒   ⊢ ((𝐵 ∈ ω ∧ 𝐷 ∈ 𝑉) → (𝐹‘suc 𝐵) = 𝐷)
Theorem	frsucmptn 8475	The value of the finite recursive definition generator at a successor (special case where the characteristic function is a mapping abstraction and where the mapping class 𝐷 is a proper class). This is a technical lemma that can be used together with frsucmpt 8474 to help eliminate redundant sethood antecedents. (Contributed by Scott Fenton, 19-Feb-2011.) (Revised by Mario Carneiro, 11-Sep-2015.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    &   ⊢ Ⅎ𝑥𝐷    &   ⊢ 𝐹 = (rec((𝑥 ∈ V ↦ 𝐶), 𝐴) ↾ ω)    &   ⊢ (𝑥 = (𝐹‘𝐵) → 𝐶 = 𝐷)    ⇒   ⊢ (¬ 𝐷 ∈ V → (𝐹‘suc 𝐵) = ∅)
Theorem	frsucmpt2 8476*	The successor value resulting from finite recursive definition generation (special case where the generation function is expressed in maps-to notation), using double-substitution instead of a bound variable condition. (Contributed by Mario Carneiro, 11-Sep-2015.)
⊢ 𝐹 = (rec((𝑥 ∈ V ↦ 𝐶), 𝐴) ↾ ω)    &   ⊢ (𝑦 = 𝑥 → 𝐸 = 𝐶)    &   ⊢ (𝑦 = (𝐹‘𝐵) → 𝐸 = 𝐷)    ⇒   ⊢ ((𝐵 ∈ ω ∧ 𝐷 ∈ 𝑉) → (𝐹‘suc 𝐵) = 𝐷)
Theorem	onelfvnef1 8477*	A sufficient condition for a function on ordinals to be one-to-one. (Contributed by NM, 9-Feb-1997.) Extract from tz7.48lem 8478 and generalize statement. (Revised by Matthew House, 6-Sep-2026.)
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐴 ⊆ On ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑦 ∈ 𝑥 → (𝐹‘𝑥) ≠ (𝐹‘𝑦))) → 𝐹:𝐴⟶1-1𝐵)
Theorem	tz7.48lem 8478*	A way of showing an ordinal function is one-to-one. (Contributed by NM, 9-Feb-1997.) Extract onelfvnef1 8477. (Proof shortened by Matthew House, 6-Sep-2026.)
⊢ 𝐹 Fn On    ⇒   ⊢ ((𝐴 ⊆ On ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝑥 ¬ (𝐹‘𝑥) = (𝐹‘𝑦)) → Fun ◡(𝐹 ↾ 𝐴))
Theorem	tz7.48lemOLD 8479*	Obsolete version of tz7.48lem 8478 as of 6-Sep-2026. (Contributed by NM, 9-Feb-1997.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐹 Fn On    ⇒   ⊢ ((𝐴 ⊆ On ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝑥 ¬ (𝐹‘𝑥) = (𝐹‘𝑦)) → Fun ◡(𝐹 ↾ 𝐴))
Theorem	tz7.48-2 8480*	Proposition 7.48(2) of [TakeutiZaring] p. 51. (Contributed by NM, 9-Feb-1997.) (Revised by David Abernethy, 5-May-2013.)
⊢ 𝐹 Fn On    ⇒   ⊢ (∀𝑥 ∈ On (𝐹‘𝑥) ∈ (𝐴 ∖ (𝐹 “ 𝑥)) → Fun ◡𝐹)
Theorem	tz7.48-1 8481*	Proposition 7.48(1) of [TakeutiZaring] p. 51. (Contributed by NM, 9-Feb-1997.)
⊢ 𝐹 Fn On    ⇒   ⊢ (∀𝑥 ∈ On (𝐹‘𝑥) ∈ (𝐴 ∖ (𝐹 “ 𝑥)) → ran 𝐹 ⊆ 𝐴)
Theorem	tz7.48-3 8482*	Proposition 7.48(3) of [TakeutiZaring] p. 51. (Contributed by NM, 9-Feb-1997.)
⊢ 𝐹 Fn On    ⇒   ⊢ (∀𝑥 ∈ On (𝐹‘𝑥) ∈ (𝐴 ∖ (𝐹 “ 𝑥)) → ¬ 𝐴 ∈ V)
Theorem	tz7.49 8483*	Proposition 7.49 of [TakeutiZaring] p. 51. (Contributed by NM, 10-Feb-1997.) (Revised by Mario Carneiro, 10-Jan-2013.)
⊢ 𝐹 Fn On    &   ⊢ (𝜑 ↔ ∀𝑥 ∈ On ((𝐴 ∖ (𝐹 “ 𝑥)) ≠ ∅ → (𝐹‘𝑥) ∈ (𝐴 ∖ (𝐹 “ 𝑥))))    ⇒   ⊢ ((𝐴 ∈ 𝐵 ∧ 𝜑) → ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅ ∧ (𝐹 “ 𝑥) = 𝐴 ∧ Fun ◡(𝐹 ↾ 𝑥)))
Theorem	tz7.49c 8484*	Corollary of Proposition 7.49 of [TakeutiZaring] p. 51. (Contributed by NM, 10-Feb-1997.) (Revised by Mario Carneiro, 19-Jan-2013.)
⊢ 𝐹 Fn On    ⇒   ⊢ ((𝐴 ∈ 𝐵 ∧ ∀𝑥 ∈ On ((𝐴 ∖ (𝐹 “ 𝑥)) ≠ ∅ → (𝐹‘𝑥) ∈ (𝐴 ∖ (𝐹 “ 𝑥)))) → ∃𝑥 ∈ On (𝐹 ↾ 𝑥):𝑥⟶1-1onto𝐴)
Syntax	cseqom 8485	Extend class notation to include index-aware recursive definitions.
class seqω(𝐹, 𝐼)
Definition	df-seqom 8486*	Index-aware recursive definitions over ω. A mashup of df-rdg 8446 and df-seq 14172, this allows for recursive definitions that use an index in the recursion in cases where Infinity is not admitted. (Contributed by Stefan O'Rear, 1-Nov-2014.)
⊢ seqω(𝐹, 𝐼) = (rec((𝑖 ∈ ω, 𝑣 ∈ V ↦ ⟨suc 𝑖, (𝑖𝐹𝑣)⟩), ⟨∅, ( I ‘𝐼)⟩) “ ω)
Theorem	seqomlem0 8487*	Lemma for seqω. Change bound variables. (Contributed by Stefan O'Rear, 1-Nov-2014.)
⊢ rec((𝑎 ∈ ω, 𝑏 ∈ V ↦ ⟨suc 𝑎, (𝑎𝐹𝑏)⟩), ⟨∅, ( I ‘𝐼)⟩) = rec((𝑐 ∈ ω, 𝑑 ∈ V ↦ ⟨suc 𝑐, (𝑐𝐹𝑑)⟩), ⟨∅, ( I ‘𝐼)⟩)
Theorem	seqomlem1 8488*	Lemma for seqω. The underlying recursion generates a sequence of pairs with the expected first values. (Contributed by Stefan O'Rear, 1-Nov-2014.) (Revised by Mario Carneiro, 23-Jun-2015.)
⊢ 𝑄 = rec((𝑖 ∈ ω, 𝑣 ∈ V ↦ ⟨suc 𝑖, (𝑖𝐹𝑣)⟩), ⟨∅, ( I ‘𝐼)⟩)    ⇒   ⊢ (𝐴 ∈ ω → (𝑄‘𝐴) = ⟨𝐴, (2nd ‘(𝑄‘𝐴))⟩)
Theorem	seqomlem2 8489*	Lemma for seqω. (Contributed by Stefan O'Rear, 1-Nov-2014.) (Revised by Mario Carneiro, 23-Jun-2015.)
⊢ 𝑄 = rec((𝑖 ∈ ω, 𝑣 ∈ V ↦ ⟨suc 𝑖, (𝑖𝐹𝑣)⟩), ⟨∅, ( I ‘𝐼)⟩)    ⇒   ⊢ (𝑄 “ ω) Fn ω
Theorem	seqomlem3 8490*	Lemma for seqω. (Contributed by Stefan O'Rear, 1-Nov-2014.)
⊢ 𝑄 = rec((𝑖 ∈ ω, 𝑣 ∈ V ↦ ⟨suc 𝑖, (𝑖𝐹𝑣)⟩), ⟨∅, ( I ‘𝐼)⟩)    ⇒   ⊢ ((𝑄 “ ω)‘∅) = ( I ‘𝐼)
Theorem	seqomlem4 8491*	Lemma for seqω. (Contributed by Stefan O'Rear, 1-Nov-2014.) (Revised by Mario Carneiro, 23-Jun-2015.)
⊢ 𝑄 = rec((𝑖 ∈ ω, 𝑣 ∈ V ↦ ⟨suc 𝑖, (𝑖𝐹𝑣)⟩), ⟨∅, ( I ‘𝐼)⟩)    ⇒   ⊢ (𝐴 ∈ ω → ((𝑄 “ ω)‘suc 𝐴) = (𝐴𝐹((𝑄 “ ω)‘𝐴)))
Theorem	seqomeq12 8492	Equality theorem for seqω. (Contributed by Stefan O'Rear, 1-Nov-2014.)
⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → seqω(𝐴, 𝐶) = seqω(𝐵, 𝐷))
Theorem	fnseqom 8493	An index-aware recursive definition defines a function on the natural numbers. (Contributed by Stefan O'Rear, 1-Nov-2014.)
⊢ 𝐺 = seqω(𝐹, 𝐼)    ⇒   ⊢ 𝐺 Fn ω
Theorem	seqom0g 8494	Value of an index-aware recursive definition at 0. (Contributed by Stefan O'Rear, 1-Nov-2014.) (Revised by AV, 17-Sep-2021.)
⊢ 𝐺 = seqω(𝐹, 𝐼)    ⇒   ⊢ (𝐼 ∈ 𝑉 → (𝐺‘∅) = 𝐼)
Theorem	seqomsuc 8495	Value of an index-aware recursive definition at a successor. (Contributed by Stefan O'Rear, 1-Nov-2014.)
⊢ 𝐺 = seqω(𝐹, 𝐼)    ⇒   ⊢ (𝐴 ∈ ω → (𝐺‘suc 𝐴) = (𝐴𝐹(𝐺‘𝐴)))
Theorem	omsucelsucb 8496	Membership is inherited by successors for natural numbers. (Contributed by AV, 15-Sep-2023.)
⊢ (𝑁 ∈ ω ↔ suc 𝑁 ∈ suc ω)
2.4.23  Ordinal arithmetic
Syntax	c1o 8497	Extend the definition of a class to include the ordinal number 1.
class 1o
Syntax	c2o 8498	Extend the definition of a class to include the ordinal number 2.
class 2o
Syntax	c3o 8499	Extend the definition of a class to include the ordinal number 3.
class 3o
Syntax	c4o 8500	Extend the definition of a class to include the ordinal number 4.
class 4o