P. 65 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 6401-6500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	smores 6401	A strictly monotone function restricted to an ordinal remains strictly monotone. (Contributed by Andrew Salmon, 16-Nov-2011.) (Proof shortened by Mario Carneiro, 5-Dec-2016.)
⊢ ((Smo 𝐴 ∧ 𝐵 ∈ dom 𝐴) → Smo (𝐴 ↾ 𝐵))
Theorem	smores3 6402	A strictly monotone function restricted to an ordinal remains strictly monotone. (Contributed by Andrew Salmon, 19-Nov-2011.)
⊢ ((Smo (𝐴 ↾ 𝐵) ∧ 𝐶 ∈ (dom 𝐴 ∩ 𝐵) ∧ Ord 𝐵) → Smo (𝐴 ↾ 𝐶))
Theorem	smores2 6403	A strictly monotone ordinal function restricted to an ordinal is still monotone. (Contributed by Mario Carneiro, 15-Mar-2013.)
⊢ ((Smo 𝐹 ∧ Ord 𝐴) → Smo (𝐹 ↾ 𝐴))
Theorem	smodm2 6404	The domain of a strictly monotone ordinal function is an ordinal. (Contributed by Mario Carneiro, 12-Mar-2013.)
⊢ ((𝐹 Fn 𝐴 ∧ Smo 𝐹) → Ord 𝐴)
Theorem	smofvon2dm 6405	The function values of a strictly monotone ordinal function are ordinals. (Contributed by Mario Carneiro, 12-Mar-2013.)
⊢ ((Smo 𝐹 ∧ 𝐵 ∈ dom 𝐹) → (𝐹‘𝐵) ∈ On)
Theorem	iordsmo 6406	The identity relation restricted to the ordinals is a strictly monotone function. (Contributed by Andrew Salmon, 16-Nov-2011.)
⊢ Ord 𝐴    ⇒   ⊢ Smo ( I ↾ 𝐴)
Theorem	smo0 6407	The null set is a strictly monotone ordinal function. (Contributed by Andrew Salmon, 20-Nov-2011.)
⊢ Smo ∅
Theorem	smofvon 6408	If 𝐵 is a strictly monotone ordinal function, and 𝐴 is in the domain of 𝐵, then the value of the function at 𝐴 is an ordinal. (Contributed by Andrew Salmon, 20-Nov-2011.)
⊢ ((Smo 𝐵 ∧ 𝐴 ∈ dom 𝐵) → (𝐵‘𝐴) ∈ On)
Theorem	smoel 6409	If 𝑥 is less than 𝑦 then a strictly monotone function's value will be strictly less at 𝑥 than at 𝑦. (Contributed by Andrew Salmon, 22-Nov-2011.)
⊢ ((Smo 𝐵 ∧ 𝐴 ∈ dom 𝐵 ∧ 𝐶 ∈ 𝐴) → (𝐵‘𝐶) ∈ (𝐵‘𝐴))
Theorem	smoiun 6410*	The value of a strictly monotone ordinal function contains its indexed union. (Contributed by Andrew Salmon, 22-Nov-2011.)
⊢ ((Smo 𝐵 ∧ 𝐴 ∈ dom 𝐵) → ∪ 𝑥 ∈ 𝐴 (𝐵‘𝑥) ⊆ (𝐵‘𝐴))
Theorem	smoiso 6411	If 𝐹 is an isomorphism from an ordinal 𝐴 onto 𝐵, which is a subset of the ordinals, then 𝐹 is a strictly monotonic function. Exercise 3 in [TakeutiZaring] p. 50. (Contributed by Andrew Salmon, 24-Nov-2011.)
⊢ ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ 𝐵 ⊆ On) → Smo 𝐹)
Theorem	smoel2 6412	A strictly monotone ordinal function preserves the epsilon relation. (Contributed by Mario Carneiro, 12-Mar-2013.)
⊢ (((𝐹 Fn 𝐴 ∧ Smo 𝐹) ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐵)) → (𝐹‘𝐶) ∈ (𝐹‘𝐵))
2.6.20  "Strong" transfinite recursion
Syntax	crecs 6413	Notation for a function defined by strong transfinite recursion.
class recs(𝐹)
Definition	df-recs 6414*	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-irdg 6479 for more details on why this definition is desirable. Unlike df-irdg 6479 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 tfri1d 6444 and tfri2d 6445 for the primary contract of this definition. (Contributed by Stefan O'Rear, 18-Jan-2015.)
⊢ recs(𝐹) = ∪ {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))}
Theorem	recseq 6415	Equality theorem for recs. (Contributed by Stefan O'Rear, 18-Jan-2015.)
⊢ (𝐹 = 𝐺 → recs(𝐹) = recs(𝐺))
Theorem	nfrecs 6416	Bound-variable hypothesis builder for recs. (Contributed by Stefan O'Rear, 18-Jan-2015.)
⊢ Ⅎ𝑥𝐹    ⇒   ⊢ Ⅎ𝑥recs(𝐹)
Theorem	tfrlem1 6417*	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	tfrlem3ag 6418*	Lemma for transfinite recursion. This lemma just changes some bound variables in 𝐴 for later use. (Contributed by Jim Kingdon, 5-Jul-2019.)
⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))}    ⇒   ⊢ (𝐺 ∈ V → (𝐺 ∈ 𝐴 ↔ ∃𝑧 ∈ On (𝐺 Fn 𝑧 ∧ ∀𝑤 ∈ 𝑧 (𝐺‘𝑤) = (𝐹‘(𝐺 ↾ 𝑤)))))
Theorem	tfrlem3a 6419*	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 6420*	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	tfrlem3-2d 6421*	Lemma for transfinite recursion which changes a bound variable (Contributed by Jim Kingdon, 2-Jul-2019.)
⊢ (𝜑 → ∀𝑥(Fun 𝐹 ∧ (𝐹‘𝑥) ∈ V))    ⇒   ⊢ (𝜑 → (Fun 𝐹 ∧ (𝐹‘𝑔) ∈ V))
Theorem	tfrlem4 6422*	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 6423*	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 6424*	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 6425*	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.)
⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))}    ⇒   ⊢ Rel recs(𝐹)
Theorem	tfrlem7 6426*	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 6427*	Lemma for transfinite recursion. The domain of recs is ordinal. (Contributed by NM, 14-Aug-1994.) (Proof shortened by Alan Sare, 11-Mar-2008.)
⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))}    ⇒   ⊢ Ord dom recs(𝐹)
Theorem	tfrlem9 6428*	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	tfrfun 6429	Transfinite recursion produces a function. (Contributed by Jim Kingdon, 20-Aug-2021.)
⊢ Fun recs(𝐹)
Theorem	tfr2a 6430	A weak version of transfinite recursion. (Contributed by Mario Carneiro, 24-Jun-2015.)
⊢ 𝐹 = recs(𝐺)    ⇒   ⊢ (𝐴 ∈ dom 𝐹 → (𝐹‘𝐴) = (𝐺‘(𝐹 ↾ 𝐴)))
Theorem	tfr0dm 6431	Transfinite recursion is defined at the empty set. (Contributed by Jim Kingdon, 8-Mar-2022.)
⊢ 𝐹 = recs(𝐺)    ⇒   ⊢ ((𝐺‘∅) ∈ 𝑉 → ∅ ∈ dom 𝐹)
Theorem	tfr0 6432	Transfinite recursion at the empty set. (Contributed by Jim Kingdon, 8-May-2020.)
⊢ 𝐹 = recs(𝐺)    ⇒   ⊢ ((𝐺‘∅) ∈ 𝑉 → (𝐹‘∅) = (𝐺‘∅))
Theorem	tfrlemisucfn 6433*	We can extend an acceptable function by one element to produce a function. Lemma for tfrlemi1 6441. (Contributed by Jim Kingdon, 2-Jul-2019.)
⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))}    &   ⊢ (𝜑 → ∀𝑥(Fun 𝐹 ∧ (𝐹‘𝑥) ∈ V))    &   ⊢ (𝜑 → 𝑧 ∈ On)    &   ⊢ (𝜑 → 𝑔 Fn 𝑧)    &   ⊢ (𝜑 → 𝑔 ∈ 𝐴)    ⇒   ⊢ (𝜑 → (𝑔 ∪ {⟨𝑧, (𝐹‘𝑔)⟩}) Fn suc 𝑧)
Theorem	tfrlemisucaccv 6434*	We can extend an acceptable function by one element to produce an acceptable function. Lemma for tfrlemi1 6441. (Contributed by Jim Kingdon, 4-Mar-2019.) (Proof shortened by Mario Carneiro, 24-May-2019.)
⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))}    &   ⊢ (𝜑 → ∀𝑥(Fun 𝐹 ∧ (𝐹‘𝑥) ∈ V))    &   ⊢ (𝜑 → 𝑧 ∈ On)    &   ⊢ (𝜑 → 𝑔 Fn 𝑧)    &   ⊢ (𝜑 → 𝑔 ∈ 𝐴)    ⇒   ⊢ (𝜑 → (𝑔 ∪ {⟨𝑧, (𝐹‘𝑔)⟩}) ∈ 𝐴)
Theorem	tfrlemibacc 6435*	Each element of 𝐵 is an acceptable function. Lemma for tfrlemi1 6441. (Contributed by Jim Kingdon, 14-Mar-2019.) (Proof shortened by Mario Carneiro, 24-May-2019.)
⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))}    &   ⊢ (𝜑 → ∀𝑥(Fun 𝐹 ∧ (𝐹‘𝑥) ∈ V))    &   ⊢ 𝐵 = {ℎ ∣ ∃𝑧 ∈ 𝑥 ∃𝑔(𝑔 Fn 𝑧 ∧ 𝑔 ∈ 𝐴 ∧ ℎ = (𝑔 ∪ {⟨𝑧, (𝐹‘𝑔)⟩}))}    &   ⊢ (𝜑 → 𝑥 ∈ On)    &   ⊢ (𝜑 → ∀𝑧 ∈ 𝑥 ∃𝑔(𝑔 Fn 𝑧 ∧ ∀𝑤 ∈ 𝑧 (𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))))    ⇒   ⊢ (𝜑 → 𝐵 ⊆ 𝐴)
Theorem	tfrlemibxssdm 6436*	The union of 𝐵 is defined on all ordinals. Lemma for tfrlemi1 6441. (Contributed by Jim Kingdon, 18-Mar-2019.) (Proof shortened by Mario Carneiro, 24-May-2019.)
⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))}    &   ⊢ (𝜑 → ∀𝑥(Fun 𝐹 ∧ (𝐹‘𝑥) ∈ V))    &   ⊢ 𝐵 = {ℎ ∣ ∃𝑧 ∈ 𝑥 ∃𝑔(𝑔 Fn 𝑧 ∧ 𝑔 ∈ 𝐴 ∧ ℎ = (𝑔 ∪ {⟨𝑧, (𝐹‘𝑔)⟩}))}    &   ⊢ (𝜑 → 𝑥 ∈ On)    &   ⊢ (𝜑 → ∀𝑧 ∈ 𝑥 ∃𝑔(𝑔 Fn 𝑧 ∧ ∀𝑤 ∈ 𝑧 (𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))))    ⇒   ⊢ (𝜑 → 𝑥 ⊆ dom ∪ 𝐵)
Theorem	tfrlemibfn 6437*	The union of 𝐵 is a function defined on 𝑥. Lemma for tfrlemi1 6441. (Contributed by Jim Kingdon, 18-Mar-2019.) (Proof shortened by Mario Carneiro, 24-May-2019.)
⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))}    &   ⊢ (𝜑 → ∀𝑥(Fun 𝐹 ∧ (𝐹‘𝑥) ∈ V))    &   ⊢ 𝐵 = {ℎ ∣ ∃𝑧 ∈ 𝑥 ∃𝑔(𝑔 Fn 𝑧 ∧ 𝑔 ∈ 𝐴 ∧ ℎ = (𝑔 ∪ {⟨𝑧, (𝐹‘𝑔)⟩}))}    &   ⊢ (𝜑 → 𝑥 ∈ On)    &   ⊢ (𝜑 → ∀𝑧 ∈ 𝑥 ∃𝑔(𝑔 Fn 𝑧 ∧ ∀𝑤 ∈ 𝑧 (𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))))    ⇒   ⊢ (𝜑 → ∪ 𝐵 Fn 𝑥)
Theorem	tfrlemibex 6438*	The set 𝐵 exists. Lemma for tfrlemi1 6441. (Contributed by Jim Kingdon, 17-Mar-2019.) (Proof shortened by Mario Carneiro, 24-May-2019.)
⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))}    &   ⊢ (𝜑 → ∀𝑥(Fun 𝐹 ∧ (𝐹‘𝑥) ∈ V))    &   ⊢ 𝐵 = {ℎ ∣ ∃𝑧 ∈ 𝑥 ∃𝑔(𝑔 Fn 𝑧 ∧ 𝑔 ∈ 𝐴 ∧ ℎ = (𝑔 ∪ {⟨𝑧, (𝐹‘𝑔)⟩}))}    &   ⊢ (𝜑 → 𝑥 ∈ On)    &   ⊢ (𝜑 → ∀𝑧 ∈ 𝑥 ∃𝑔(𝑔 Fn 𝑧 ∧ ∀𝑤 ∈ 𝑧 (𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))))    ⇒   ⊢ (𝜑 → 𝐵 ∈ V)
Theorem	tfrlemiubacc 6439*	The union of 𝐵 satisfies the recursion rule (lemma for tfrlemi1 6441). (Contributed by Jim Kingdon, 22-Apr-2019.) (Proof shortened by Mario Carneiro, 24-May-2019.)
⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))}    &   ⊢ (𝜑 → ∀𝑥(Fun 𝐹 ∧ (𝐹‘𝑥) ∈ V))    &   ⊢ 𝐵 = {ℎ ∣ ∃𝑧 ∈ 𝑥 ∃𝑔(𝑔 Fn 𝑧 ∧ 𝑔 ∈ 𝐴 ∧ ℎ = (𝑔 ∪ {⟨𝑧, (𝐹‘𝑔)⟩}))}    &   ⊢ (𝜑 → 𝑥 ∈ On)    &   ⊢ (𝜑 → ∀𝑧 ∈ 𝑥 ∃𝑔(𝑔 Fn 𝑧 ∧ ∀𝑤 ∈ 𝑧 (𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))))    ⇒   ⊢ (𝜑 → ∀𝑢 ∈ 𝑥 (∪ 𝐵‘𝑢) = (𝐹‘(∪ 𝐵 ↾ 𝑢)))
Theorem	tfrlemiex 6440*	Lemma for tfrlemi1 6441. (Contributed by Jim Kingdon, 18-Mar-2019.) (Proof shortened by Mario Carneiro, 24-May-2019.)
⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))}    &   ⊢ (𝜑 → ∀𝑥(Fun 𝐹 ∧ (𝐹‘𝑥) ∈ V))    &   ⊢ 𝐵 = {ℎ ∣ ∃𝑧 ∈ 𝑥 ∃𝑔(𝑔 Fn 𝑧 ∧ 𝑔 ∈ 𝐴 ∧ ℎ = (𝑔 ∪ {⟨𝑧, (𝐹‘𝑔)⟩}))}    &   ⊢ (𝜑 → 𝑥 ∈ On)    &   ⊢ (𝜑 → ∀𝑧 ∈ 𝑥 ∃𝑔(𝑔 Fn 𝑧 ∧ ∀𝑤 ∈ 𝑧 (𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))))    ⇒   ⊢ (𝜑 → ∃𝑓(𝑓 Fn 𝑥 ∧ ∀𝑢 ∈ 𝑥 (𝑓‘𝑢) = (𝐹‘(𝑓 ↾ 𝑢))))
Theorem	tfrlemi1 6441*	We can define an acceptable function on any ordinal. As with many of the transfinite recursion theorems, we have a hypothesis that states that 𝐹 is a function and that it is defined for all ordinals. (Contributed by Jim Kingdon, 4-Mar-2019.) (Proof shortened by Mario Carneiro, 24-May-2019.)
⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))}    &   ⊢ (𝜑 → ∀𝑥(Fun 𝐹 ∧ (𝐹‘𝑥) ∈ V))    ⇒   ⊢ ((𝜑 ∧ 𝐶 ∈ On) → ∃𝑔(𝑔 Fn 𝐶 ∧ ∀𝑢 ∈ 𝐶 (𝑔‘𝑢) = (𝐹‘(𝑔 ↾ 𝑢))))
Theorem	tfrlemi14d 6442*	The domain of recs is all ordinals (lemma for transfinite recursion). (Contributed by Jim Kingdon, 9-Jul-2019.)
⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))}    &   ⊢ (𝜑 → ∀𝑥(Fun 𝐹 ∧ (𝐹‘𝑥) ∈ V))    ⇒   ⊢ (𝜑 → dom recs(𝐹) = On)
Theorem	tfrexlem 6443*	The transfinite recursion function is set-like if the input is. (Contributed by Mario Carneiro, 3-Jul-2019.)
⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))}    &   ⊢ (𝜑 → ∀𝑥(Fun 𝐹 ∧ (𝐹‘𝑥) ∈ V))    ⇒   ⊢ ((𝜑 ∧ 𝐶 ∈ 𝑉) → (recs(𝐹)‘𝐶) ∈ V)
Theorem	tfri1d 6444*	Principle of Transfinite Recursion, part 1 of 3. Theorem 7.41(1) of [TakeutiZaring] p. 47, with an additional condition. The condition is that 𝐺 is defined "everywhere", which is stated here as (𝐺‘𝑥) ∈ V. Alternately, ∀𝑥 ∈ On∀𝑓(𝑓 Fn 𝑥 → 𝑓 ∈ dom 𝐺) would suffice. Given a function 𝐺 satisfying that condition, we 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 Jim Kingdon, 4-May-2019.) (Revised by Mario Carneiro, 24-May-2019.)
⊢ 𝐹 = recs(𝐺)    &   ⊢ (𝜑 → ∀𝑥(Fun 𝐺 ∧ (𝐺‘𝑥) ∈ V))    ⇒   ⊢ (𝜑 → 𝐹 Fn On)
Theorem	tfri2d 6445*	Principle of Transfinite Recursion, part 2 of 3. Theorem 7.41(2) of [TakeutiZaring] p. 47, with an additional condition on the recursion rule 𝐺 ( as described at tfri1 6474). Here we show that the function 𝐹 has the property that for any function 𝐺 satisfying that condition, the "next" value of 𝐹 is 𝐺 recursively applied to all "previous" values of 𝐹. (Contributed by Jim Kingdon, 4-May-2019.)
⊢ 𝐹 = recs(𝐺)    &   ⊢ (𝜑 → ∀𝑥(Fun 𝐺 ∧ (𝐺‘𝑥) ∈ V))    ⇒   ⊢ ((𝜑 ∧ 𝐴 ∈ On) → (𝐹‘𝐴) = (𝐺‘(𝐹 ↾ 𝐴)))
Theorem	tfr1onlem3ag 6446*	Lemma for transfinite recursion. This lemma changes some bound variables in 𝐴 (version of tfrlem3ag 6418 but for tfr1on 6459 related lemmas). (Contributed by Jim Kingdon, 13-Mar-2022.)
⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ 𝑋 (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐺‘(𝑓 ↾ 𝑦)))}    ⇒   ⊢ (𝐻 ∈ 𝑉 → (𝐻 ∈ 𝐴 ↔ ∃𝑧 ∈ 𝑋 (𝐻 Fn 𝑧 ∧ ∀𝑤 ∈ 𝑧 (𝐻‘𝑤) = (𝐺‘(𝐻 ↾ 𝑤)))))
Theorem	tfr1onlem3 6447*	Lemma for transfinite recursion. This lemma changes some bound variables in 𝐴 (version of tfrlem3 6420 but for tfr1on 6459 related lemmas). (Contributed by Jim Kingdon, 14-Mar-2022.)
⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ 𝑋 (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐺‘(𝑓 ↾ 𝑦)))}    ⇒   ⊢ 𝐴 = {𝑔 ∣ ∃𝑧 ∈ 𝑋 (𝑔 Fn 𝑧 ∧ ∀𝑤 ∈ 𝑧 (𝑔‘𝑤) = (𝐺‘(𝑔 ↾ 𝑤)))}
Theorem	tfr1onlemssrecs 6448*	Lemma for tfr1on 6459. The union of functions acceptable for tfr1on 6459 is a subset of recs. (Contributed by Jim Kingdon, 15-Mar-2022.)
⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ 𝑋 (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐺‘(𝑓 ↾ 𝑦)))}    &   ⊢ (𝜑 → Ord 𝑋)    ⇒   ⊢ (𝜑 → ∪ 𝐴 ⊆ recs(𝐺))
Theorem	tfr1onlemsucfn 6449*	We can extend an acceptable function by one element to produce a function. Lemma for tfr1on 6459. (Contributed by Jim Kingdon, 12-Mar-2022.)
⊢ 𝐹 = recs(𝐺)    &   ⊢ (𝜑 → Fun 𝐺)    &   ⊢ (𝜑 → Ord 𝑋)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑓 Fn 𝑥) → (𝐺‘𝑓) ∈ V)    &   ⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ 𝑋 (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐺‘(𝑓 ↾ 𝑦)))}    &   ⊢ (𝜑 → 𝑧 ∈ 𝑋)    &   ⊢ (𝜑 → 𝑔 Fn 𝑧)    &   ⊢ (𝜑 → 𝑔 ∈ 𝐴)    ⇒   ⊢ (𝜑 → (𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩}) Fn suc 𝑧)
Theorem	tfr1onlemsucaccv 6450*	Lemma for tfr1on 6459. We can extend an acceptable function by one element to produce an acceptable function. (Contributed by Jim Kingdon, 12-Mar-2022.)
⊢ 𝐹 = recs(𝐺)    &   ⊢ (𝜑 → Fun 𝐺)    &   ⊢ (𝜑 → Ord 𝑋)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑓 Fn 𝑥) → (𝐺‘𝑓) ∈ V)    &   ⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ 𝑋 (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐺‘(𝑓 ↾ 𝑦)))}    &   ⊢ (𝜑 → 𝑌 ∈ 𝑋)    &   ⊢ (𝜑 → 𝑧 ∈ 𝑌)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝑋) → suc 𝑥 ∈ 𝑋)    &   ⊢ (𝜑 → 𝑔 Fn 𝑧)    &   ⊢ (𝜑 → 𝑔 ∈ 𝐴)    ⇒   ⊢ (𝜑 → (𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩}) ∈ 𝐴)
Theorem	tfr1onlembacc 6451*	Lemma for tfr1on 6459. Each element of 𝐵 is an acceptable function. (Contributed by Jim Kingdon, 14-Mar-2022.)
⊢ 𝐹 = recs(𝐺)    &   ⊢ (𝜑 → Fun 𝐺)    &   ⊢ (𝜑 → Ord 𝑋)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑓 Fn 𝑥) → (𝐺‘𝑓) ∈ V)    &   ⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ 𝑋 (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐺‘(𝑓 ↾ 𝑦)))}    &   ⊢ 𝐵 = {ℎ ∣ ∃𝑧 ∈ 𝐷 ∃𝑔(𝑔 Fn 𝑧 ∧ 𝑔 ∈ 𝐴 ∧ ℎ = (𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩}))}    &   ⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝑋) → suc 𝑥 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑋)    &   ⊢ (𝜑 → ∀𝑧 ∈ 𝐷 ∃𝑔(𝑔 Fn 𝑧 ∧ ∀𝑤 ∈ 𝑧 (𝑔‘𝑤) = (𝐺‘(𝑔 ↾ 𝑤))))    ⇒   ⊢ (𝜑 → 𝐵 ⊆ 𝐴)
Theorem	tfr1onlembxssdm 6452*	Lemma for tfr1on 6459. The union of 𝐵 is defined on all elements of 𝑋. (Contributed by Jim Kingdon, 14-Mar-2022.)
⊢ 𝐹 = recs(𝐺)    &   ⊢ (𝜑 → Fun 𝐺)    &   ⊢ (𝜑 → Ord 𝑋)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑓 Fn 𝑥) → (𝐺‘𝑓) ∈ V)    &   ⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ 𝑋 (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐺‘(𝑓 ↾ 𝑦)))}    &   ⊢ 𝐵 = {ℎ ∣ ∃𝑧 ∈ 𝐷 ∃𝑔(𝑔 Fn 𝑧 ∧ 𝑔 ∈ 𝐴 ∧ ℎ = (𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩}))}    &   ⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝑋) → suc 𝑥 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑋)    &   ⊢ (𝜑 → ∀𝑧 ∈ 𝐷 ∃𝑔(𝑔 Fn 𝑧 ∧ ∀𝑤 ∈ 𝑧 (𝑔‘𝑤) = (𝐺‘(𝑔 ↾ 𝑤))))    ⇒   ⊢ (𝜑 → 𝐷 ⊆ dom ∪ 𝐵)
Theorem	tfr1onlembfn 6453*	Lemma for tfr1on 6459. The union of 𝐵 is a function defined on 𝑥. (Contributed by Jim Kingdon, 15-Mar-2022.)
⊢ 𝐹 = recs(𝐺)    &   ⊢ (𝜑 → Fun 𝐺)    &   ⊢ (𝜑 → Ord 𝑋)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑓 Fn 𝑥) → (𝐺‘𝑓) ∈ V)    &   ⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ 𝑋 (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐺‘(𝑓 ↾ 𝑦)))}    &   ⊢ 𝐵 = {ℎ ∣ ∃𝑧 ∈ 𝐷 ∃𝑔(𝑔 Fn 𝑧 ∧ 𝑔 ∈ 𝐴 ∧ ℎ = (𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩}))}    &   ⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝑋) → suc 𝑥 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑋)    &   ⊢ (𝜑 → ∀𝑧 ∈ 𝐷 ∃𝑔(𝑔 Fn 𝑧 ∧ ∀𝑤 ∈ 𝑧 (𝑔‘𝑤) = (𝐺‘(𝑔 ↾ 𝑤))))    ⇒   ⊢ (𝜑 → ∪ 𝐵 Fn 𝐷)
Theorem	tfr1onlembex 6454*	Lemma for tfr1on 6459. The set 𝐵 exists. (Contributed by Jim Kingdon, 14-Mar-2022.)
⊢ 𝐹 = recs(𝐺)    &   ⊢ (𝜑 → Fun 𝐺)    &   ⊢ (𝜑 → Ord 𝑋)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑓 Fn 𝑥) → (𝐺‘𝑓) ∈ V)    &   ⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ 𝑋 (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐺‘(𝑓 ↾ 𝑦)))}    &   ⊢ 𝐵 = {ℎ ∣ ∃𝑧 ∈ 𝐷 ∃𝑔(𝑔 Fn 𝑧 ∧ 𝑔 ∈ 𝐴 ∧ ℎ = (𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩}))}    &   ⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝑋) → suc 𝑥 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑋)    &   ⊢ (𝜑 → ∀𝑧 ∈ 𝐷 ∃𝑔(𝑔 Fn 𝑧 ∧ ∀𝑤 ∈ 𝑧 (𝑔‘𝑤) = (𝐺‘(𝑔 ↾ 𝑤))))    ⇒   ⊢ (𝜑 → 𝐵 ∈ V)
Theorem	tfr1onlemubacc 6455*	Lemma for tfr1on 6459. The union of 𝐵 satisfies the recursion rule. (Contributed by Jim Kingdon, 15-Mar-2022.)
⊢ 𝐹 = recs(𝐺)    &   ⊢ (𝜑 → Fun 𝐺)    &   ⊢ (𝜑 → Ord 𝑋)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑓 Fn 𝑥) → (𝐺‘𝑓) ∈ V)    &   ⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ 𝑋 (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐺‘(𝑓 ↾ 𝑦)))}    &   ⊢ 𝐵 = {ℎ ∣ ∃𝑧 ∈ 𝐷 ∃𝑔(𝑔 Fn 𝑧 ∧ 𝑔 ∈ 𝐴 ∧ ℎ = (𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩}))}    &   ⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝑋) → suc 𝑥 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑋)    &   ⊢ (𝜑 → ∀𝑧 ∈ 𝐷 ∃𝑔(𝑔 Fn 𝑧 ∧ ∀𝑤 ∈ 𝑧 (𝑔‘𝑤) = (𝐺‘(𝑔 ↾ 𝑤))))    ⇒   ⊢ (𝜑 → ∀𝑢 ∈ 𝐷 (∪ 𝐵‘𝑢) = (𝐺‘(∪ 𝐵 ↾ 𝑢)))
Theorem	tfr1onlemex 6456*	Lemma for tfr1on 6459. (Contributed by Jim Kingdon, 16-Mar-2022.)
⊢ 𝐹 = recs(𝐺)    &   ⊢ (𝜑 → Fun 𝐺)    &   ⊢ (𝜑 → Ord 𝑋)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑓 Fn 𝑥) → (𝐺‘𝑓) ∈ V)    &   ⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ 𝑋 (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐺‘(𝑓 ↾ 𝑦)))}    &   ⊢ 𝐵 = {ℎ ∣ ∃𝑧 ∈ 𝐷 ∃𝑔(𝑔 Fn 𝑧 ∧ 𝑔 ∈ 𝐴 ∧ ℎ = (𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩}))}    &   ⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝑋) → suc 𝑥 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑋)    &   ⊢ (𝜑 → ∀𝑧 ∈ 𝐷 ∃𝑔(𝑔 Fn 𝑧 ∧ ∀𝑤 ∈ 𝑧 (𝑔‘𝑤) = (𝐺‘(𝑔 ↾ 𝑤))))    ⇒   ⊢ (𝜑 → ∃𝑓(𝑓 Fn 𝐷 ∧ ∀𝑢 ∈ 𝐷 (𝑓‘𝑢) = (𝐺‘(𝑓 ↾ 𝑢))))
Theorem	tfr1onlemaccex 6457*	We can define an acceptable function on any element of 𝑋. As with many of the transfinite recursion theorems, we have hypotheses that state that 𝐹 is a function and that it is defined up to 𝑋. (Contributed by Jim Kingdon, 16-Mar-2022.)
⊢ 𝐹 = recs(𝐺)    &   ⊢ (𝜑 → Fun 𝐺)    &   ⊢ (𝜑 → Ord 𝑋)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑓 Fn 𝑥) → (𝐺‘𝑓) ∈ V)    &   ⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ 𝑋 (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐺‘(𝑓 ↾ 𝑦)))}    &   ⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝑋) → suc 𝑥 ∈ 𝑋)    ⇒   ⊢ ((𝜑 ∧ 𝐶 ∈ 𝑋) → ∃𝑔(𝑔 Fn 𝐶 ∧ ∀𝑢 ∈ 𝐶 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))
Theorem	tfr1onlemres 6458*	Lemma for tfr1on 6459. Recursion is defined on an ordinal if the characteristic function is defined up to a suitable point. (Contributed by Jim Kingdon, 18-Mar-2022.)
⊢ 𝐹 = recs(𝐺)    &   ⊢ (𝜑 → Fun 𝐺)    &   ⊢ (𝜑 → Ord 𝑋)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑓 Fn 𝑥) → (𝐺‘𝑓) ∈ V)    &   ⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ 𝑋 (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐺‘(𝑓 ↾ 𝑦)))}    &   ⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝑋) → suc 𝑥 ∈ 𝑋)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑋)    ⇒   ⊢ (𝜑 → 𝑌 ⊆ dom 𝐹)
Theorem	tfr1on 6459*	Recursion is defined on an ordinal if the characteristic function is defined up to a suitable point. (Contributed by Jim Kingdon, 12-Mar-2022.)
⊢ 𝐹 = recs(𝐺)    &   ⊢ (𝜑 → Fun 𝐺)    &   ⊢ (𝜑 → Ord 𝑋)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑓 Fn 𝑥) → (𝐺‘𝑓) ∈ V)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝑋) → suc 𝑥 ∈ 𝑋)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑋)    ⇒   ⊢ (𝜑 → 𝑌 ⊆ dom 𝐹)
Theorem	tfri1dALT 6460*	Alternate proof of tfri1d 6444 in terms of tfr1on 6459. Although this does show that the tfr1on 6459 proof is general enough to also prove tfri1d 6444, the tfri1d 6444 proof is simpler in places because it does not need to deal with 𝑋 being any ordinal. For that reason, we have both proofs. (Proof modification is discouraged.) (New usage is discouraged.) (Contributed by Jim Kingdon, 20-Mar-2022.)
⊢ 𝐹 = recs(𝐺)    &   ⊢ (𝜑 → ∀𝑥(Fun 𝐺 ∧ (𝐺‘𝑥) ∈ V))    ⇒   ⊢ (𝜑 → 𝐹 Fn On)
Theorem	tfrcllemssrecs 6461*	Lemma for tfrcl 6473. The union of functions acceptable for tfrcl 6473 is a subset of recs. (Contributed by Jim Kingdon, 25-Mar-2022.)
⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ 𝑋 (𝑓:𝑥⟶𝑆 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐺‘(𝑓 ↾ 𝑦)))}    &   ⊢ (𝜑 → Ord 𝑋)    ⇒   ⊢ (𝜑 → ∪ 𝐴 ⊆ recs(𝐺))
Theorem	tfrcllemsucfn 6462*	We can extend an acceptable function by one element to produce a function. Lemma for tfrcl 6473. (Contributed by Jim Kingdon, 24-Mar-2022.)
⊢ 𝐹 = recs(𝐺)    &   ⊢ (𝜑 → Fun 𝐺)    &   ⊢ (𝜑 → Ord 𝑋)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑓:𝑥⟶𝑆) → (𝐺‘𝑓) ∈ 𝑆)    &   ⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ 𝑋 (𝑓:𝑥⟶𝑆 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐺‘(𝑓 ↾ 𝑦)))}    &   ⊢ (𝜑 → 𝑧 ∈ 𝑋)    &   ⊢ (𝜑 → 𝑔:𝑧⟶𝑆)    &   ⊢ (𝜑 → 𝑔 ∈ 𝐴)    ⇒   ⊢ (𝜑 → (𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩}):suc 𝑧⟶𝑆)
Theorem	tfrcllemsucaccv 6463*	Lemma for tfrcl 6473. We can extend an acceptable function by one element to produce an acceptable function. (Contributed by Jim Kingdon, 24-Mar-2022.)
⊢ 𝐹 = recs(𝐺)    &   ⊢ (𝜑 → Fun 𝐺)    &   ⊢ (𝜑 → Ord 𝑋)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑓:𝑥⟶𝑆) → (𝐺‘𝑓) ∈ 𝑆)    &   ⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ 𝑋 (𝑓:𝑥⟶𝑆 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐺‘(𝑓 ↾ 𝑦)))}    &   ⊢ (𝜑 → 𝑌 ∈ 𝑋)    &   ⊢ (𝜑 → 𝑧 ∈ 𝑌)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝑋) → suc 𝑥 ∈ 𝑋)    &   ⊢ (𝜑 → 𝑔:𝑧⟶𝑆)    &   ⊢ (𝜑 → 𝑔 ∈ 𝐴)    ⇒   ⊢ (𝜑 → (𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩}) ∈ 𝐴)
Theorem	tfrcllembacc 6464*	Lemma for tfrcl 6473. Each element of 𝐵 is an acceptable function. (Contributed by Jim Kingdon, 25-Mar-2022.)
⊢ 𝐹 = recs(𝐺)    &   ⊢ (𝜑 → Fun 𝐺)    &   ⊢ (𝜑 → Ord 𝑋)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑓:𝑥⟶𝑆) → (𝐺‘𝑓) ∈ 𝑆)    &   ⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ 𝑋 (𝑓:𝑥⟶𝑆 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐺‘(𝑓 ↾ 𝑦)))}    &   ⊢ 𝐵 = {ℎ ∣ ∃𝑧 ∈ 𝐷 ∃𝑔(𝑔:𝑧⟶𝑆 ∧ 𝑔 ∈ 𝐴 ∧ ℎ = (𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩}))}    &   ⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝑋) → suc 𝑥 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑋)    &   ⊢ (𝜑 → ∀𝑧 ∈ 𝐷 ∃𝑔(𝑔:𝑧⟶𝑆 ∧ ∀𝑤 ∈ 𝑧 (𝑔‘𝑤) = (𝐺‘(𝑔 ↾ 𝑤))))    ⇒   ⊢ (𝜑 → 𝐵 ⊆ 𝐴)
Theorem	tfrcllembxssdm 6465*	Lemma for tfrcl 6473. The union of 𝐵 is defined on all elements of 𝑋. (Contributed by Jim Kingdon, 25-Mar-2022.)
⊢ 𝐹 = recs(𝐺)    &   ⊢ (𝜑 → Fun 𝐺)    &   ⊢ (𝜑 → Ord 𝑋)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑓:𝑥⟶𝑆) → (𝐺‘𝑓) ∈ 𝑆)    &   ⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ 𝑋 (𝑓:𝑥⟶𝑆 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐺‘(𝑓 ↾ 𝑦)))}    &   ⊢ 𝐵 = {ℎ ∣ ∃𝑧 ∈ 𝐷 ∃𝑔(𝑔:𝑧⟶𝑆 ∧ 𝑔 ∈ 𝐴 ∧ ℎ = (𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩}))}    &   ⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝑋) → suc 𝑥 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑋)    &   ⊢ (𝜑 → ∀𝑧 ∈ 𝐷 ∃𝑔(𝑔:𝑧⟶𝑆 ∧ ∀𝑤 ∈ 𝑧 (𝑔‘𝑤) = (𝐺‘(𝑔 ↾ 𝑤))))    ⇒   ⊢ (𝜑 → 𝐷 ⊆ dom ∪ 𝐵)
Theorem	tfrcllembfn 6466*	Lemma for tfrcl 6473. The union of 𝐵 is a function defined on 𝑥. (Contributed by Jim Kingdon, 25-Mar-2022.)
⊢ 𝐹 = recs(𝐺)    &   ⊢ (𝜑 → Fun 𝐺)    &   ⊢ (𝜑 → Ord 𝑋)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑓:𝑥⟶𝑆) → (𝐺‘𝑓) ∈ 𝑆)    &   ⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ 𝑋 (𝑓:𝑥⟶𝑆 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐺‘(𝑓 ↾ 𝑦)))}    &   ⊢ 𝐵 = {ℎ ∣ ∃𝑧 ∈ 𝐷 ∃𝑔(𝑔:𝑧⟶𝑆 ∧ 𝑔 ∈ 𝐴 ∧ ℎ = (𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩}))}    &   ⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝑋) → suc 𝑥 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑋)    &   ⊢ (𝜑 → ∀𝑧 ∈ 𝐷 ∃𝑔(𝑔:𝑧⟶𝑆 ∧ ∀𝑤 ∈ 𝑧 (𝑔‘𝑤) = (𝐺‘(𝑔 ↾ 𝑤))))    ⇒   ⊢ (𝜑 → ∪ 𝐵:𝐷⟶𝑆)
Theorem	tfrcllembex 6467*	Lemma for tfrcl 6473. The set 𝐵 exists. (Contributed by Jim Kingdon, 25-Mar-2022.)
⊢ 𝐹 = recs(𝐺)    &   ⊢ (𝜑 → Fun 𝐺)    &   ⊢ (𝜑 → Ord 𝑋)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑓:𝑥⟶𝑆) → (𝐺‘𝑓) ∈ 𝑆)    &   ⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ 𝑋 (𝑓:𝑥⟶𝑆 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐺‘(𝑓 ↾ 𝑦)))}    &   ⊢ 𝐵 = {ℎ ∣ ∃𝑧 ∈ 𝐷 ∃𝑔(𝑔:𝑧⟶𝑆 ∧ 𝑔 ∈ 𝐴 ∧ ℎ = (𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩}))}    &   ⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝑋) → suc 𝑥 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑋)    &   ⊢ (𝜑 → ∀𝑧 ∈ 𝐷 ∃𝑔(𝑔:𝑧⟶𝑆 ∧ ∀𝑤 ∈ 𝑧 (𝑔‘𝑤) = (𝐺‘(𝑔 ↾ 𝑤))))    ⇒   ⊢ (𝜑 → 𝐵 ∈ V)
Theorem	tfrcllemubacc 6468*	Lemma for tfrcl 6473. The union of 𝐵 satisfies the recursion rule. (Contributed by Jim Kingdon, 25-Mar-2022.)
⊢ 𝐹 = recs(𝐺)    &   ⊢ (𝜑 → Fun 𝐺)    &   ⊢ (𝜑 → Ord 𝑋)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑓:𝑥⟶𝑆) → (𝐺‘𝑓) ∈ 𝑆)    &   ⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ 𝑋 (𝑓:𝑥⟶𝑆 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐺‘(𝑓 ↾ 𝑦)))}    &   ⊢ 𝐵 = {ℎ ∣ ∃𝑧 ∈ 𝐷 ∃𝑔(𝑔:𝑧⟶𝑆 ∧ 𝑔 ∈ 𝐴 ∧ ℎ = (𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩}))}    &   ⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝑋) → suc 𝑥 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑋)    &   ⊢ (𝜑 → ∀𝑧 ∈ 𝐷 ∃𝑔(𝑔:𝑧⟶𝑆 ∧ ∀𝑤 ∈ 𝑧 (𝑔‘𝑤) = (𝐺‘(𝑔 ↾ 𝑤))))    ⇒   ⊢ (𝜑 → ∀𝑢 ∈ 𝐷 (∪ 𝐵‘𝑢) = (𝐺‘(∪ 𝐵 ↾ 𝑢)))
Theorem	tfrcllemex 6469*	Lemma for tfrcl 6473. (Contributed by Jim Kingdon, 26-Mar-2022.)
⊢ 𝐹 = recs(𝐺)    &   ⊢ (𝜑 → Fun 𝐺)    &   ⊢ (𝜑 → Ord 𝑋)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑓:𝑥⟶𝑆) → (𝐺‘𝑓) ∈ 𝑆)    &   ⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ 𝑋 (𝑓:𝑥⟶𝑆 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐺‘(𝑓 ↾ 𝑦)))}    &   ⊢ 𝐵 = {ℎ ∣ ∃𝑧 ∈ 𝐷 ∃𝑔(𝑔:𝑧⟶𝑆 ∧ 𝑔 ∈ 𝐴 ∧ ℎ = (𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩}))}    &   ⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝑋) → suc 𝑥 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑋)    &   ⊢ (𝜑 → ∀𝑧 ∈ 𝐷 ∃𝑔(𝑔:𝑧⟶𝑆 ∧ ∀𝑤 ∈ 𝑧 (𝑔‘𝑤) = (𝐺‘(𝑔 ↾ 𝑤))))    ⇒   ⊢ (𝜑 → ∃𝑓(𝑓:𝐷⟶𝑆 ∧ ∀𝑢 ∈ 𝐷 (𝑓‘𝑢) = (𝐺‘(𝑓 ↾ 𝑢))))
Theorem	tfrcllemaccex 6470*	We can define an acceptable function on any element of 𝑋. As with many of the transfinite recursion theorems, we have hypotheses that state that 𝐹 is a function and that it is defined up to 𝑋. (Contributed by Jim Kingdon, 26-Mar-2022.)
⊢ 𝐹 = recs(𝐺)    &   ⊢ (𝜑 → Fun 𝐺)    &   ⊢ (𝜑 → Ord 𝑋)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑓:𝑥⟶𝑆) → (𝐺‘𝑓) ∈ 𝑆)    &   ⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ 𝑋 (𝑓:𝑥⟶𝑆 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐺‘(𝑓 ↾ 𝑦)))}    &   ⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝑋) → suc 𝑥 ∈ 𝑋)    ⇒   ⊢ ((𝜑 ∧ 𝐶 ∈ 𝑋) → ∃𝑔(𝑔:𝐶⟶𝑆 ∧ ∀𝑢 ∈ 𝐶 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))
Theorem	tfrcllemres 6471*	Lemma for tfr1on 6459. Recursion is defined on an ordinal if the characteristic function is defined up to a suitable point. (Contributed by Jim Kingdon, 18-Mar-2022.)
⊢ 𝐹 = recs(𝐺)    &   ⊢ (𝜑 → Fun 𝐺)    &   ⊢ (𝜑 → Ord 𝑋)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑓:𝑥⟶𝑆) → (𝐺‘𝑓) ∈ 𝑆)    &   ⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ 𝑋 (𝑓:𝑥⟶𝑆 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐺‘(𝑓 ↾ 𝑦)))}    &   ⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝑋) → suc 𝑥 ∈ 𝑋)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑋)    ⇒   ⊢ (𝜑 → 𝑌 ⊆ dom 𝐹)
Theorem	tfrcldm 6472*	Recursion is defined on an ordinal if the characteristic function satisfies a closure hypothesis up to a suitable point. (Contributed by Jim Kingdon, 26-Mar-2022.)
⊢ 𝐹 = recs(𝐺)    &   ⊢ (𝜑 → Fun 𝐺)    &   ⊢ (𝜑 → Ord 𝑋)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑓:𝑥⟶𝑆) → (𝐺‘𝑓) ∈ 𝑆)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝑋) → suc 𝑥 ∈ 𝑋)    &   ⊢ (𝜑 → 𝑌 ∈ ∪ 𝑋)    ⇒   ⊢ (𝜑 → 𝑌 ∈ dom 𝐹)
Theorem	tfrcl 6473*	Closure for transfinite recursion. As with tfr1on 6459, the characteristic function must be defined up to a suitable point, not necessarily on all ordinals. (Contributed by Jim Kingdon, 25-Mar-2022.)
⊢ 𝐹 = recs(𝐺)    &   ⊢ (𝜑 → Fun 𝐺)    &   ⊢ (𝜑 → Ord 𝑋)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑓:𝑥⟶𝑆) → (𝐺‘𝑓) ∈ 𝑆)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝑋) → suc 𝑥 ∈ 𝑋)    &   ⊢ (𝜑 → 𝑌 ∈ ∪ 𝑋)    ⇒   ⊢ (𝜑 → (𝐹‘𝑌) ∈ 𝑆)
Theorem	tfri1 6474*	Principle of Transfinite Recursion, part 1 of 3. Theorem 7.41(1) of [TakeutiZaring] p. 47, with an additional condition. The condition is that 𝐺 is defined "everywhere", which is stated here as (𝐺‘𝑥) ∈ V. Alternately, ∀𝑥 ∈ On∀𝑓(𝑓 Fn 𝑥 → 𝑓 ∈ dom 𝐺) would suffice. Given a function 𝐺 satisfying that condition, we 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 Jim Kingdon, 4-May-2019.) (Revised by Mario Carneiro, 24-May-2019.)
⊢ 𝐹 = recs(𝐺)    &   ⊢ (Fun 𝐺 ∧ (𝐺‘𝑥) ∈ V)    ⇒   ⊢ 𝐹 Fn On
Theorem	tfri2 6475*	Principle of Transfinite Recursion, part 2 of 3. Theorem 7.41(2) of [TakeutiZaring] p. 47, with an additional condition on the recursion rule 𝐺 ( as described at tfri1 6474). Here we show that the function 𝐹 has the property that for any function 𝐺 satisfying that condition, the "next" value of 𝐹 is 𝐺 recursively applied to all "previous" values of 𝐹. (Contributed by Jim Kingdon, 4-May-2019.)
⊢ 𝐹 = recs(𝐺)    &   ⊢ (Fun 𝐺 ∧ (𝐺‘𝑥) ∈ V)    ⇒   ⊢ (𝐴 ∈ On → (𝐹‘𝐴) = (𝐺‘(𝐹 ↾ 𝐴)))
Theorem	tfri3 6476*	Principle of Transfinite Recursion, part 3 of 3. Theorem 7.41(3) of [TakeutiZaring] p. 47, with an additional condition on the recursion rule 𝐺 ( as described at tfri1 6474). 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 Jim Kingdon, 4-May-2019.)
⊢ 𝐹 = recs(𝐺)    &   ⊢ (Fun 𝐺 ∧ (𝐺‘𝑥) ∈ V)    ⇒   ⊢ ((𝐵 Fn On ∧ ∀𝑥 ∈ On (𝐵‘𝑥) = (𝐺‘(𝐵 ↾ 𝑥))) → 𝐵 = 𝐹)
Theorem	tfrex 6477*	The transfinite recursion function is set-like if the input is. (Contributed by Mario Carneiro, 3-Jul-2019.)
⊢ 𝐹 = recs(𝐺)    &   ⊢ (𝜑 → ∀𝑥(Fun 𝐺 ∧ (𝐺‘𝑥) ∈ V))    ⇒   ⊢ ((𝜑 ∧ 𝐴 ∈ 𝑉) → (𝐹‘𝐴) ∈ V)
2.6.21  Recursive definition generator
Syntax	crdg 6478	Extend class notation with the recursive definition generator, with characteristic function 𝐹 and initial value 𝐼.
class rec(𝐹, 𝐼)
Definition	df-irdg 6479*	Define a recursive definition generator on On (the class of ordinal numbers) with characteristic function 𝐹 and initial value 𝐼. This rather amazing operation allows us 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 6414 that it is built on is also eliminated). But once we get past this hurdle, definitions that would otherwise be recursive become relatively simple. In classical logic it would be easier to divide this definition into cases based on whether the domain of 𝑔 is zero, a successor, or a limit ordinal. Cases do not (in general) work that way in intuitionistic logic, so instead we choose a definition which takes the union of all the results of the characteristic function for ordinals in the domain of 𝑔. This means that this definition has the expected properties for increasing and continuous ordinal functions, which include ordinal addition and multiplication. For finite recursion we also define df-frec 6500 and for suitable characteristic functions df-frec 6500 yields the same result as rec restricted to ω, as seen at frecrdg 6517. 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 Jim Kingdon, 19-May-2019.)
⊢ rec(𝐹, 𝐼) = recs((𝑔 ∈ V ↦ (𝐼 ∪ ∪ 𝑥 ∈ dom 𝑔(𝐹‘(𝑔‘𝑥)))))
Theorem	rdgeq1 6480	Equality theorem for the recursive definition generator. (Contributed by NM, 9-Apr-1995.) (Revised by Mario Carneiro, 9-May-2015.)
⊢ (𝐹 = 𝐺 → rec(𝐹, 𝐴) = rec(𝐺, 𝐴))
Theorem	rdgeq2 6481	Equality theorem for the recursive definition generator. (Contributed by NM, 9-Apr-1995.) (Revised by Mario Carneiro, 9-May-2015.)
⊢ (𝐴 = 𝐵 → rec(𝐹, 𝐴) = rec(𝐹, 𝐵))
Theorem	rdgfun 6482	The recursive definition generator is a function. (Contributed by Mario Carneiro, 16-Nov-2014.)
⊢ Fun rec(𝐹, 𝐴)
Theorem	rdgtfr 6483*	The recursion rule for the recursive definition generator is defined everywhere. (Contributed by Jim Kingdon, 14-May-2020.)
⊢ ((∀𝑧(𝐹‘𝑧) ∈ V ∧ 𝐴 ∈ 𝑉) → (Fun (𝑔 ∈ V ↦ (𝐴 ∪ ∪ 𝑥 ∈ dom 𝑔(𝐹‘(𝑔‘𝑥)))) ∧ ((𝑔 ∈ V ↦ (𝐴 ∪ ∪ 𝑥 ∈ dom 𝑔(𝐹‘(𝑔‘𝑥))))‘𝑓) ∈ V))
Theorem	rdgruledefgg 6484*	The recursion rule for the recursive definition generator is defined everywhere. (Contributed by Jim Kingdon, 4-Jul-2019.)
⊢ ((𝐹 Fn V ∧ 𝐴 ∈ 𝑉) → (Fun (𝑔 ∈ V ↦ (𝐴 ∪ ∪ 𝑥 ∈ dom 𝑔(𝐹‘(𝑔‘𝑥)))) ∧ ((𝑔 ∈ V ↦ (𝐴 ∪ ∪ 𝑥 ∈ dom 𝑔(𝐹‘(𝑔‘𝑥))))‘𝑓) ∈ V))
Theorem	rdgruledefg 6485*	The recursion rule for the recursive definition generator is defined everywhere. (Contributed by Jim Kingdon, 4-Jul-2019.)
⊢ 𝐹 Fn V    ⇒   ⊢ (𝐴 ∈ 𝑉 → (Fun (𝑔 ∈ V ↦ (𝐴 ∪ ∪ 𝑥 ∈ dom 𝑔(𝐹‘(𝑔‘𝑥)))) ∧ ((𝑔 ∈ V ↦ (𝐴 ∪ ∪ 𝑥 ∈ dom 𝑔(𝐹‘(𝑔‘𝑥))))‘𝑓) ∈ V))
Theorem	rdgexggg 6486	The recursive definition generator produces a set on a set input. (Contributed by Jim Kingdon, 4-Jul-2019.)
⊢ ((𝐹 Fn V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (rec(𝐹, 𝐴)‘𝐵) ∈ V)
Theorem	rdgexgg 6487	The recursive definition generator produces a set on a set input. (Contributed by Jim Kingdon, 4-Jul-2019.)
⊢ 𝐹 Fn V    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (rec(𝐹, 𝐴)‘𝐵) ∈ V)
Theorem	rdgifnon 6488	The recursive definition generator is a function on ordinal numbers. The 𝐹 Fn V condition states that the characteristic function is defined for all sets (being defined for all ordinals might be enough if being used in a manner similar to rdgon 6495; in cases like df-oadd 6529 either presumably could work). (Contributed by Jim Kingdon, 13-Jul-2019.)
⊢ ((𝐹 Fn V ∧ 𝐴 ∈ 𝑉) → rec(𝐹, 𝐴) Fn On)
Theorem	rdgifnon2 6489*	The recursive definition generator is a function on ordinal numbers. (Contributed by Jim Kingdon, 14-May-2020.)
⊢ ((∀𝑧(𝐹‘𝑧) ∈ V ∧ 𝐴 ∈ 𝑉) → rec(𝐹, 𝐴) Fn On)
Theorem	rdgivallem 6490*	Value of the recursive definition generator. Lemma for rdgival 6491 which simplifies the value further. (Contributed by Jim Kingdon, 13-Jul-2019.) (New usage is discouraged.)
⊢ ((𝐹 Fn V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ On) → (rec(𝐹, 𝐴)‘𝐵) = (𝐴 ∪ ∪ 𝑥 ∈ 𝐵 (𝐹‘((rec(𝐹, 𝐴) ↾ 𝐵)‘𝑥))))
Theorem	rdgival 6491*	Value of the recursive definition generator. (Contributed by Jim Kingdon, 26-Jul-2019.)
⊢ ((𝐹 Fn V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ On) → (rec(𝐹, 𝐴)‘𝐵) = (𝐴 ∪ ∪ 𝑥 ∈ 𝐵 (𝐹‘(rec(𝐹, 𝐴)‘𝑥))))
Theorem	rdgss 6492	Subset and recursive definition generator. (Contributed by Jim Kingdon, 15-Jul-2019.)
⊢ (𝜑 → 𝐹 Fn V)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐴 ∈ On)    &   ⊢ (𝜑 → 𝐵 ∈ On)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → (rec(𝐹, 𝐼)‘𝐴) ⊆ (rec(𝐹, 𝐼)‘𝐵))
Theorem	rdgisuc1 6493*	One way of describing the value of the recursive definition generator at a successor. There is no condition on the characteristic function 𝐹 other than 𝐹 Fn V. Given that, the resulting expression encompasses both the expected successor term (𝐹‘(rec(𝐹, 𝐴)‘𝐵)) but also terms that correspond to the initial value 𝐴 and to limit ordinals ∪ 𝑥 ∈ 𝐵(𝐹‘(rec(𝐹, 𝐴)‘𝑥)). If we add conditions on the characteristic function, we can show tighter results such as rdgisucinc 6494. (Contributed by Jim Kingdon, 9-Jun-2019.)
⊢ (𝜑 → 𝐹 Fn V)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ On)    ⇒   ⊢ (𝜑 → (rec(𝐹, 𝐴)‘suc 𝐵) = (𝐴 ∪ (∪ 𝑥 ∈ 𝐵 (𝐹‘(rec(𝐹, 𝐴)‘𝑥)) ∪ (𝐹‘(rec(𝐹, 𝐴)‘𝐵)))))
Theorem	rdgisucinc 6494*	Value of the recursive definition generator at a successor. This can be thought of as a generalization of oasuc 6573 and omsuc 6581. (Contributed by Jim Kingdon, 29-Aug-2019.)
⊢ (𝜑 → 𝐹 Fn V)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ On)    &   ⊢ (𝜑 → ∀𝑥 𝑥 ⊆ (𝐹‘𝑥))    ⇒   ⊢ (𝜑 → (rec(𝐹, 𝐴)‘suc 𝐵) = (𝐹‘(rec(𝐹, 𝐴)‘𝐵)))
Theorem	rdgon 6495*	Evaluating the recursive definition generator produces an ordinal. There is a hypothesis that the characteristic function produces ordinals on ordinal arguments. (Contributed by Jim Kingdon, 26-Jul-2019.) (Revised by Jim Kingdon, 13-Apr-2022.)
⊢ (𝜑 → 𝐴 ∈ On)    &   ⊢ (𝜑 → ∀𝑥 ∈ On (𝐹‘𝑥) ∈ On)    ⇒   ⊢ ((𝜑 ∧ 𝐵 ∈ On) → (rec(𝐹, 𝐴)‘𝐵) ∈ On)
Theorem	rdg0 6496	The initial value of the recursive definition generator. (Contributed by NM, 23-Apr-1995.) (Revised by Mario Carneiro, 14-Nov-2014.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (rec(𝐹, 𝐴)‘∅) = 𝐴
Theorem	rdg0g 6497	The initial value of the recursive definition generator. (Contributed by NM, 25-Apr-1995.)
⊢ (𝐴 ∈ 𝐶 → (rec(𝐹, 𝐴)‘∅) = 𝐴)
Theorem	rdgexg 6498	The recursive definition generator produces a set on a set input. (Contributed by Mario Carneiro, 3-Jul-2019.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐹 Fn V    ⇒   ⊢ (𝐵 ∈ 𝑉 → (rec(𝐹, 𝐴)‘𝐵) ∈ V)
2.6.22  Finite recursion
Syntax	cfrec 6499	Extend class notation with the finite recursive definition generator, with characteristic function 𝐹 and initial value 𝐼.
class frec(𝐹, 𝐼)
Definition	df-frec 6500*	Define a recursive definition generator on ω (the class of finite ordinals) with characteristic function 𝐹 and initial value 𝐼. This rather amazing operation allows us 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 frec operation (especially when df-recs 6414 that it is built on is also eliminated). But once we get past this hurdle, definitions that would otherwise be recursive become relatively simple; see frec0g 6506 and frecsuc 6516. Unlike with transfinite recursion, finite recurson can readily divide definitions and proofs into zero and successor cases, because even without excluded middle we have theorems such as nn0suc 4670. The analogous situation with transfinite recursion - being able to say that an ordinal is zero, successor, or limit - is enabled by excluded middle and thus is not available to us. For the characteristic functions which satisfy the conditions given at frecrdg 6517, this definition and df-irdg 6479 restricted to ω produce the same result. Note: We introduce frec 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 Mario Carneiro and Jim Kingdon, 10-Aug-2019.)
⊢ frec(𝐹, 𝐼) = (recs((𝑔 ∈ V ↦ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝑔‘𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥 ∈ 𝐼))})) ↾ ω)