P. 83 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 8201-8300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	tfr3 8201*	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 8202	Alternate proof of tfr1 8199 using well-ordered recursion. (Contributed by Scott Fenton, 3-Aug-2020.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝐹 = recs(𝐺)    ⇒   ⊢ 𝐹 Fn On
Theorem	tfr2ALT 8203	Alternate proof of tfr2 8200 using well-ordered recursion. (Contributed by Scott Fenton, 3-Aug-2020.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝐹 = recs(𝐺)    ⇒   ⊢ (𝐴 ∈ On → (𝐹‘𝐴) = (𝐺‘(𝐹 ↾ 𝐴)))
Theorem	tfr3ALT 8204*	Alternate proof of tfr3 8201 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 8205	Strong transfinite recursion defines a function on ordinals. (Contributed by Stefan O'Rear, 18-Jan-2015.)
⊢ recs(𝐹) Fn On
Theorem	recsval 8206	Strong transfinite recursion in terms of all previous values. (Contributed by Stefan O'Rear, 18-Jan-2015.)
⊢ (𝐴 ∈ On → (recs(𝐹)‘𝐴) = (𝐹‘(recs(𝐹) ↾ 𝐴)))
Theorem	tz7.44lem1 8207*	The ordered pair abstraction 𝐺 defined in the hypothesis is a function. This was a lemma for tz7.44-1 8208, tz7.44-2 8209, and tz7.44-3 8210 when they used that definition of 𝐺. Now, they use the maps-to df-mpt 5154 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 8208*	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 8209*	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 8210*	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.18  Recursive definition generator
Syntax	crdg 8211	Extend class notation with the recursive definition generator, with characteristic function 𝐹 and initial value 𝐼.
class rec(𝐹, 𝐼)
Definition	df-rdg 8212*	Define a recursive definition generator on On (the class of ordinal numbers) with characteristic function 𝐹 and initial value 𝐼. This combines functions 𝐹 in tfr1 8199 and 𝐺 in tz7.44-1 8208 into one definition. 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 8173 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 8303, from which we prove the recursive textbook definition as Theorems oa0 8308, oasuc 8316, and oalim 8324 (with the help of Theorems rdg0 8223, rdgsuc 8226, and rdglim2a 8235). We can also restrict the rec operation to define otherwise recursive functions on the natural numbers ω; see fr0g 8237 and frsuc 8238. 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 4457) 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 13650 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 13916 and integer powers df-exp 13711. 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 8213	Equality theorem for the recursive definition generator. (Contributed by NM, 9-Apr-1995.) (Revised by Mario Carneiro, 9-May-2015.)
⊢ (𝐹 = 𝐺 → rec(𝐹, 𝐴) = rec(𝐺, 𝐴))
Theorem	rdgeq2 8214	Equality theorem for the recursive definition generator. (Contributed by NM, 9-Apr-1995.) (Revised by Mario Carneiro, 9-May-2015.)
⊢ (𝐴 = 𝐵 → rec(𝐹, 𝐴) = rec(𝐹, 𝐵))
Theorem	rdgeq12 8215	Equality theorem for the recursive definition generator. (Contributed by Scott Fenton, 28-Apr-2012.)
⊢ ((𝐹 = 𝐺 ∧ 𝐴 = 𝐵) → rec(𝐹, 𝐴) = rec(𝐺, 𝐵))
Theorem	nfrdg 8216	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 8217*	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 8218	The recursive definition generator is a function. (Contributed by Mario Carneiro, 16-Nov-2014.)
⊢ Fun rec(𝐹, 𝐴)
Theorem	rdgdmlim 8219	The domain of the recursive definition generator is a limit ordinal. (Contributed by NM, 16-Nov-2014.)
⊢ Lim dom rec(𝐹, 𝐴)
Theorem	rdgfnon 8220	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 8221*	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 8222*	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 8223	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 8224	The initial segments of the recursive definition generator are sets. (Contributed by Mario Carneiro, 16-Nov-2014.)
⊢ (𝐵 ∈ dom rec(𝐹, 𝐴) → (rec(𝐹, 𝐴) ↾ 𝐵) ∈ V)
Theorem	rdgsucg 8225	The value of the recursive definition generator at a successor. (Contributed by NM, 16-Nov-2014.)
⊢ (𝐵 ∈ dom rec(𝐹, 𝐴) → (rec(𝐹, 𝐴)‘suc 𝐵) = (𝐹‘(rec(𝐹, 𝐴)‘𝐵)))
Theorem	rdgsuc 8226	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 8227	The value of the recursive definition generator at a limit ordinal. (Contributed by NM, 16-Nov-2014.)
⊢ ((𝐵 ∈ dom rec(𝐹, 𝐴) ∧ Lim 𝐵) → (rec(𝐹, 𝐴)‘𝐵) = ∪ (rec(𝐹, 𝐴) “ 𝐵))
Theorem	rdglim 8228	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 8229	The initial value of the recursive definition generator. (Contributed by NM, 25-Apr-1995.)
⊢ (𝐴 ∈ 𝐶 → (rec(𝐹, 𝐴)‘∅) = 𝐴)
Theorem	rdgsucmptf 8230	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 8231	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 8230 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 8232*	This version of rdgsucmpt 8233 avoids the not-free hypothesis of rdgsucmptf 8230 by using two substitutions instead of one. (Contributed by Mario Carneiro, 11-Sep-2015.)
⊢ 𝐹 = rec((𝑥 ∈ V ↦ 𝐶), 𝐴)    &   ⊢ (𝑦 = 𝑥 → 𝐸 = 𝐶)    &   ⊢ (𝑦 = (𝐹‘𝐵) → 𝐸 = 𝐷)    ⇒   ⊢ ((𝐵 ∈ On ∧ 𝐷 ∈ 𝑉) → (𝐹‘suc 𝐵) = 𝐷)
Theorem	rdgsucmpt 8233*	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 8234*	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 8235*	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(𝐹, 𝐴)‘𝑥))
2.4.19  Finite recursion
Theorem	frfnom 8236	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 8237	The initial value resulting from finite recursive definition generation. (Contributed by NM, 15-Oct-1996.)
⊢ (𝐴 ∈ 𝐵 → ((rec(𝐹, 𝐴) ↾ ω)‘∅) = 𝐴)
Theorem	frsuc 8238	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 8239	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 8240	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 8239 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 8241*	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	tz7.48lem 8242*	A way of showing an ordinal function is one-to-one. (Contributed by NM, 9-Feb-1997.)
⊢ 𝐹 Fn On    ⇒   ⊢ ((𝐴 ⊆ On ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝑥 ¬ (𝐹‘𝑥) = (𝐹‘𝑦)) → Fun ◡(𝐹 ↾ 𝐴))
Theorem	tz7.48-2 8243*	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 8244*	Proposition 7.48(1) of [TakeutiZaring] p. 51. (Contributed by NM, 9-Feb-1997.)
⊢ 𝐹 Fn On    ⇒   ⊢ (∀𝑥 ∈ On (𝐹‘𝑥) ∈ (𝐴 ∖ (𝐹 “ 𝑥)) → ran 𝐹 ⊆ 𝐴)
Theorem	tz7.48-3 8245*	Proposition 7.48(3) of [TakeutiZaring] p. 51. (Contributed by NM, 9-Feb-1997.)
⊢ 𝐹 Fn On    ⇒   ⊢ (∀𝑥 ∈ On (𝐹‘𝑥) ∈ (𝐴 ∖ (𝐹 “ 𝑥)) → ¬ 𝐴 ∈ V)
Theorem	tz7.49 8246*	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 8247*	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-1-onto→𝐴)
Syntax	cseqom 8248	Extend class notation to include index-aware recursive definitions.
class seqω(𝐹, 𝐼)
Definition	df-seqom 8249*	Index-aware recursive definitions over ω. A mashup of df-rdg 8212 and df-seq 13650, 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 8250*	Lemma for seqω. Change bound variables. (Contributed by Stefan O'Rear, 1-Nov-2014.)
⊢ rec((𝑎 ∈ ω, 𝑏 ∈ V ↦ ⟨suc 𝑎, (𝑎𝐹𝑏)⟩), ⟨∅, ( I ‘𝐼)⟩) = rec((𝑐 ∈ ω, 𝑑 ∈ V ↦ ⟨suc 𝑐, (𝑐𝐹𝑑)⟩), ⟨∅, ( I ‘𝐼)⟩)
Theorem	seqomlem1 8251*	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 8252*	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 8253*	Lemma for seqω. (Contributed by Stefan O'Rear, 1-Nov-2014.)
⊢ 𝑄 = rec((𝑖 ∈ ω, 𝑣 ∈ V ↦ ⟨suc 𝑖, (𝑖𝐹𝑣)⟩), ⟨∅, ( I ‘𝐼)⟩)    ⇒   ⊢ ((𝑄 “ ω)‘∅) = ( I ‘𝐼)
Theorem	seqomlem4 8254*	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 8255	Equality theorem for seqω. (Contributed by Stefan O'Rear, 1-Nov-2014.)
⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → seqω(𝐴, 𝐶) = seqω(𝐵, 𝐷))
Theorem	fnseqom 8256	An index-aware recursive definition defines a function on the natural numbers. (Contributed by Stefan O'Rear, 1-Nov-2014.)
⊢ 𝐺 = seqω(𝐹, 𝐼)    ⇒   ⊢ 𝐺 Fn ω
Theorem	seqom0g 8257	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 8258	Value of an index-aware recursive definition at a successor. (Contributed by Stefan O'Rear, 1-Nov-2014.)
⊢ 𝐺 = seqω(𝐹, 𝐼)    ⇒   ⊢ (𝐴 ∈ ω → (𝐺‘suc 𝐴) = (𝐴𝐹(𝐺‘𝐴)))
Theorem	omsucelsucb 8259	Membership is inherited by successors for natural numbers. (Contributed by AV, 15-Sep-2023.)
⊢ (𝑁 ∈ ω ↔ suc 𝑁 ∈ suc ω)
2.4.20  Ordinal arithmetic
Syntax	c1o 8260	Extend the definition of a class to include the ordinal number 1.
class 1o
Syntax	c2o 8261	Extend the definition of a class to include the ordinal number 2.
class 2o
Syntax	c3o 8262	Extend the definition of a class to include the ordinal number 3.
class 3o
Syntax	c4o 8263	Extend the definition of a class to include the ordinal number 4.
class 4o
Syntax	coa 8264	Extend the definition of a class to include the ordinal addition operation.
class +o
Syntax	comu 8265	Extend the definition of a class to include the ordinal multiplication operation.
class ·o
Syntax	coe 8266	Extend the definition of a class to include the ordinal exponentiation operation.
class ↑o
Definition	df-1o 8267	Define the ordinal number 1. (Contributed by NM, 29-Oct-1995.)
⊢ 1o = suc ∅
Definition	df-2o 8268	Define the ordinal number 2. (Contributed by NM, 18-Feb-2004.)
⊢ 2o = suc 1o
Definition	df-3o 8269	Define the ordinal number 3. (Contributed by Mario Carneiro, 14-Jul-2013.)
⊢ 3o = suc 2o
Definition	df-4o 8270	Define the ordinal number 4. (Contributed by Mario Carneiro, 14-Jul-2013.)
⊢ 4o = suc 3o
Definition	df-oadd 8271*	Define the ordinal addition operation. (Contributed by NM, 3-May-1995.)
⊢ +o = (𝑥 ∈ On, 𝑦 ∈ On ↦ (rec((𝑧 ∈ V ↦ suc 𝑧), 𝑥)‘𝑦))
Definition	df-omul 8272*	Define the ordinal multiplication operation. (Contributed by NM, 26-Aug-1995.)
⊢ ·o = (𝑥 ∈ On, 𝑦 ∈ On ↦ (rec((𝑧 ∈ V ↦ (𝑧 +o 𝑥)), ∅)‘𝑦))
Definition	df-oexp 8273*	Define the ordinal exponentiation operation. (Contributed by NM, 30-Dec-2004.)
⊢ ↑o = (𝑥 ∈ On, 𝑦 ∈ On ↦ if(𝑥 = ∅, (1o ∖ 𝑦), (rec((𝑧 ∈ V ↦ (𝑧 ·o 𝑥)), 1o)‘𝑦)))
Theorem	1on 8274	Ordinal 1 is an ordinal number. (Contributed by NM, 29-Oct-1995.)
⊢ 1o ∈ On
Theorem	2on 8275	Ordinal 2 is an ordinal number. (Contributed by NM, 18-Feb-2004.) (Proof shortened by Andrew Salmon, 12-Aug-2011.)
⊢ 2o ∈ On
Theorem	2on0 8276	Ordinal two is not zero. (Contributed by Scott Fenton, 17-Jun-2011.)
⊢ 2o ≠ ∅
Theorem	3on 8277	Ordinal 3 is an ordinal number. (Contributed by Mario Carneiro, 5-Jan-2016.)
⊢ 3o ∈ On
Theorem	4on 8278	Ordinal 3 is an ordinal number. (Contributed by Mario Carneiro, 5-Jan-2016.)
⊢ 4o ∈ On
Theorem	df1o2 8279	Expanded value of the ordinal number 1. (Contributed by NM, 4-Nov-2002.)
⊢ 1o = {∅}
Theorem	1oex 8280	Ordinal 1 is a set. (Contributed by BJ, 6-Apr-2019.) (Proof shortened by AV, 1-Jul-2022.) Remove dependency on ax-10 2139, ax-11 2156, ax-12 2173, ax-un 7566. (Revised by Zhi Wang, 19-Sep-2024.)
⊢ 1o ∈ V
Theorem	1oexOLD 8281	Obsolete version of 1oex 8280 as of 19-Sep-2024. (Contributed by BJ, 6-Apr-2019.) (Proof shortened by AV, 1-Jul-2022.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 1o ∈ V
Theorem	df2o3 8282	Expanded value of the ordinal number 2. (Contributed by Mario Carneiro, 14-Aug-2015.)
⊢ 2o = {∅, 1o}
Theorem	df2o2 8283	Expanded value of the ordinal number 2. (Contributed by NM, 29-Jan-2004.)
⊢ 2o = {∅, {∅}}
Theorem	2oex 8284	2o is a set. (Contributed by BJ, 6-Apr-2019.) Remove dependency on ax-10 2139, ax-11 2156, ax-12 2173, ax-un 7566. (Proof shortened by Zhi Wang, 19-Sep-2024.)
⊢ 2o ∈ V
Theorem	2oexOLD 8285	Obsolete version of 2oex 8284 as of 19-Sep-2024. (Contributed by BJ, 6-Apr-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 2o ∈ V
Theorem	1n0 8286	Ordinal one is not equal to ordinal zero. (Contributed by NM, 26-Dec-2004.)
⊢ 1o ≠ ∅
Theorem	xp01disj 8287	Cartesian products with the singletons of ordinals 0 and 1 are disjoint. (Contributed by NM, 2-Jun-2007.)
⊢ ((𝐴 × {∅}) ∩ (𝐶 × {1o})) = ∅
Theorem	xp01disjl 8288	Cartesian products with the singletons of ordinals 0 and 1 are disjoint. (Contributed by Jim Kingdon, 11-Jul-2023.)
⊢ (({∅} × 𝐴) ∩ ({1o} × 𝐶)) = ∅
Theorem	ordgt0ge1 8289	Two ways to express that an ordinal class is positive. (Contributed by NM, 21-Dec-2004.)
⊢ (Ord 𝐴 → (∅ ∈ 𝐴 ↔ 1o ⊆ 𝐴))
Theorem	ordge1n0 8290	An ordinal greater than or equal to 1 is nonzero. (Contributed by NM, 21-Dec-2004.)
⊢ (Ord 𝐴 → (1o ⊆ 𝐴 ↔ 𝐴 ≠ ∅))
Theorem	el1o 8291	Membership in ordinal one. (Contributed by NM, 5-Jan-2005.)
⊢ (𝐴 ∈ 1o ↔ 𝐴 = ∅)
Theorem	dif1o 8292	Two ways to say that 𝐴 is a nonzero number of the set 𝐵. (Contributed by Mario Carneiro, 21-May-2015.)
⊢ (𝐴 ∈ (𝐵 ∖ 1o) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ≠ ∅))
Theorem	ondif1 8293	Two ways to say that 𝐴 is a nonzero ordinal number. (Contributed by Mario Carneiro, 21-May-2015.)
⊢ (𝐴 ∈ (On ∖ 1o) ↔ (𝐴 ∈ On ∧ ∅ ∈ 𝐴))
Theorem	ondif2 8294	Two ways to say that 𝐴 is an ordinal greater than one. (Contributed by Mario Carneiro, 21-May-2015.)
⊢ (𝐴 ∈ (On ∖ 2o) ↔ (𝐴 ∈ On ∧ 1o ∈ 𝐴))
Theorem	2oconcl 8295	Closure of the pair swapping function on 2o. (Contributed by Mario Carneiro, 27-Sep-2015.)
⊢ (𝐴 ∈ 2o → (1o ∖ 𝐴) ∈ 2o)
Theorem	0lt1o 8296	Ordinal zero is less than ordinal one. (Contributed by NM, 5-Jan-2005.)
⊢ ∅ ∈ 1o
Theorem	dif20el 8297	An ordinal greater than one is greater than zero. (Contributed by Mario Carneiro, 25-May-2015.)
⊢ (𝐴 ∈ (On ∖ 2o) → ∅ ∈ 𝐴)
Theorem	0we1 8298	The empty set is a well-ordering of ordinal one. (Contributed by Mario Carneiro, 9-Feb-2015.)
⊢ ∅ We 1o
Theorem	brwitnlem 8299	Lemma for relations which assert the existence of a witness in a two-parameter set. (Contributed by Stefan O'Rear, 25-Jan-2015.) (Revised by Mario Carneiro, 23-Aug-2015.)
⊢ 𝑅 = (◡𝑂 “ (V ∖ 1o))    &   ⊢ 𝑂 Fn 𝑋    ⇒   ⊢ (𝐴𝑅𝐵 ↔ (𝐴𝑂𝐵) ≠ ∅)
Theorem	fnoa 8300	Functionality and domain of ordinal addition. (Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro, 8-Sep-2013.)
⊢ +o Fn (On × On)