P. 76 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 7501-7600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	tz7.44lem1 7501*	𝐺 is a function. Lemma for tz7.44-1 7502, tz7.44-2 7503, and tz7.44-3 7504. (Contributed by NM, 23-Apr-1995.) (Revised by David Abernethy, 19-Jun-2012.)
⊢ 𝐺 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 = ∅ ∧ 𝑦 = 𝐴) ∨ (¬ (𝑥 = ∅ ∨ Lim dom 𝑥) ∧ 𝑦 = (𝐻‘(𝑥‘∪ dom 𝑥))) ∨ (Lim dom 𝑥 ∧ 𝑦 = ∪ ran 𝑥))}    ⇒   ⊢ Fun 𝐺
Theorem	tz7.44-1 7502*	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 7503*	The value of 𝐹 at a successor ordinal. Part 2 of Theorem 7.44 of [TakeutiZaring] p. 49. (Unnecessary distinct variable restrictions were removed by David Abernethy, 19-Jun-2012.) (Contributed by NM, 23-Apr-1995.) (Revised by Mario Carneiro, 14-Nov-2014.)
⊢ 𝐺 = (𝑥 ∈ V ↦ if(𝑥 = ∅, 𝐴, if(Lim dom 𝑥, ∪ ran 𝑥, (𝐻‘(𝑥‘∪ dom 𝑥)))))    &   ⊢ (𝑦 ∈ 𝑋 → (𝐹‘𝑦) = (𝐺‘(𝐹 ↾ 𝑦)))    &   ⊢ (𝑦 ∈ 𝑋 → (𝐹 ↾ 𝑦) ∈ V)    &   ⊢ 𝐹 Fn 𝑋    &   ⊢ Ord 𝑋    ⇒   ⊢ (suc 𝐵 ∈ 𝑋 → (𝐹‘suc 𝐵) = (𝐻‘(𝐹‘𝐵)))
Theorem	tz7.44-3 7504*	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.16  Recursive definition generator
Syntax	crdg 7505	Extend class notation with the recursive definition generator, with characteristic function 𝐹 and initial value 𝐼.
class rec(𝐹, 𝐼)
Definition	df-rdg 7506*	Define a recursive definition generator on On (the class of ordinal numbers) with characteristic function 𝐹 and initial value 𝐼. This combines functions 𝐹 in tfr1 7493 and 𝐺 in tz7.44-1 7502 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 7468 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 7591, from which we prove the recursive textbook definition as theorems oa0 7596, oasuc 7604, and oalim 7612 (with the help of theorems rdg0 7517, rdgsuc 7520, and rdglim2a 7529). We can also restrict the rec operation to define otherwise recursive functions on the natural numbers ω; see fr0g 7531 and frsuc 7532. 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 4087) 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 12802 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 13061 and integer powers df-exp 12861. 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 7507	Equality theorem for the recursive definition generator. (Contributed by NM, 9-Apr-1995.) (Revised by Mario Carneiro, 9-May-2015.)
⊢ (𝐹 = 𝐺 → rec(𝐹, 𝐴) = rec(𝐺, 𝐴))
Theorem	rdgeq2 7508	Equality theorem for the recursive definition generator. (Contributed by NM, 9-Apr-1995.) (Revised by Mario Carneiro, 9-May-2015.)
⊢ (𝐴 = 𝐵 → rec(𝐹, 𝐴) = rec(𝐹, 𝐵))
Theorem	rdgeq12 7509	Equality theorem for the recursive definition generator. (Contributed by Scott Fenton, 28-Apr-2012.)
⊢ ((𝐹 = 𝐺 ∧ 𝐴 = 𝐵) → rec(𝐹, 𝐴) = rec(𝐺, 𝐵))
Theorem	nfrdg 7510	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 7511*	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 7512	The recursive definition generator is a function. (Contributed by Mario Carneiro, 16-Nov-2014.)
⊢ Fun rec(𝐹, 𝐴)
Theorem	rdgdmlim 7513	The domain of the recursive definition generator is a limit ordinal. (Contributed by NM, 16-Nov-2014.)
⊢ Lim dom rec(𝐹, 𝐴)
Theorem	rdgfnon 7514	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 7515*	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 7516*	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 7517	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 7518	The initial segments of the recursive definition generator are sets. (Contributed by Mario Carneiro, 16-Nov-2014.)
⊢ (𝐵 ∈ dom rec(𝐹, 𝐴) → (rec(𝐹, 𝐴) ↾ 𝐵) ∈ V)
Theorem	rdgsucg 7519	The value of the recursive definition generator at a successor. (Contributed by NM, 16-Nov-2014.)
⊢ (𝐵 ∈ dom rec(𝐹, 𝐴) → (rec(𝐹, 𝐴)‘suc 𝐵) = (𝐹‘(rec(𝐹, 𝐴)‘𝐵)))
Theorem	rdgsuc 7520	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 7521	The value of the recursive definition generator at a limit ordinal. (Contributed by NM, 16-Nov-2014.)
⊢ ((𝐵 ∈ dom rec(𝐹, 𝐴) ∧ Lim 𝐵) → (rec(𝐹, 𝐴)‘𝐵) = ∪ (rec(𝐹, 𝐴) “ 𝐵))
Theorem	rdglim 7522	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 7523	The initial value of the recursive definition generator. (Contributed by NM, 25-Apr-1995.)
⊢ (𝐴 ∈ 𝐶 → (rec(𝐹, 𝐴)‘∅) = 𝐴)
Theorem	rdgsucmptf 7524	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 7525	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 7524 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 7526*	This version of rdgsucmpt 7527 avoids the not-free hypothesis of rdgsucmptf 7524 by using two substitutions instead of one. (Contributed by Mario Carneiro, 11-Sep-2015.)
⊢ 𝐹 = rec((𝑥 ∈ V ↦ 𝐶), 𝐴)    &   ⊢ (𝑦 = 𝑥 → 𝐸 = 𝐶)    &   ⊢ (𝑦 = (𝐹‘𝐵) → 𝐸 = 𝐷)    ⇒   ⊢ ((𝐵 ∈ On ∧ 𝐷 ∈ 𝑉) → (𝐹‘suc 𝐵) = 𝐷)
Theorem	rdgsucmpt 7527*	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 7528*	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 7529*	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.17  Finite recursion
Theorem	frfnom 7530	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 7531	The initial value resulting from finite recursive definition generation. (Contributed by NM, 15-Oct-1996.)
⊢ (𝐴 ∈ 𝐵 → ((rec(𝐹, 𝐴) ↾ ω)‘∅) = 𝐴)
Theorem	frsuc 7532	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 7533	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 7534	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 7533 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 7535*	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 7536*	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 7537*	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 7538*	Proposition 7.48(1) of [TakeutiZaring] p. 51. (Contributed by NM, 9-Feb-1997.)
⊢ 𝐹 Fn On    ⇒   ⊢ (∀𝑥 ∈ On (𝐹‘𝑥) ∈ (𝐴 ∖ (𝐹 “ 𝑥)) → ran 𝐹 ⊆ 𝐴)
Theorem	tz7.48-3 7539*	Proposition 7.48(3) of [TakeutiZaring] p. 51. (Contributed by NM, 9-Feb-1997.)
⊢ 𝐹 Fn On    ⇒   ⊢ (∀𝑥 ∈ On (𝐹‘𝑥) ∈ (𝐴 ∖ (𝐹 “ 𝑥)) → ¬ 𝐴 ∈ V)
Theorem	tz7.49 7540*	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 7541*	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 7542	Extend class notation to include index-aware recursive definitions.
class seq𝜔(𝐹, 𝐼)
Definition	df-seqom 7543*	Index-aware recursive definitions over ω. A mashup of df-rdg 7506 and df-seq 12802, 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 7544*	Lemma for seq𝜔. Change bound variables. (Contributed by Stefan O'Rear, 1-Nov-2014.)
⊢ rec((𝑎 ∈ ω, 𝑏 ∈ V ↦ ⟨suc 𝑎, (𝑎𝐹𝑏)⟩), ⟨∅, ( I ‘𝐼)⟩) = rec((𝑐 ∈ ω, 𝑑 ∈ V ↦ ⟨suc 𝑐, (𝑐𝐹𝑑)⟩), ⟨∅, ( I ‘𝐼)⟩)
Theorem	seqomlem1 7545*	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 7546*	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 7547*	Lemma for seq𝜔. (Contributed by Stefan O'Rear, 1-Nov-2014.)
⊢ 𝑄 = rec((𝑖 ∈ ω, 𝑣 ∈ V ↦ ⟨suc 𝑖, (𝑖𝐹𝑣)⟩), ⟨∅, ( I ‘𝐼)⟩)    ⇒   ⊢ ((𝑄 “ ω)‘∅) = ( I ‘𝐼)
Theorem	seqomlem4 7548*	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 7549	Equality theorem for seq𝜔. (Contributed by Stefan O'Rear, 1-Nov-2014.)
⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → seq𝜔(𝐴, 𝐶) = seq𝜔(𝐵, 𝐷))
Theorem	fnseqom 7550	An index-aware recursive definition defines a function on the natural numbers. (Contributed by Stefan O'Rear, 1-Nov-2014.)
⊢ 𝐺 = seq𝜔(𝐹, 𝐼)    ⇒   ⊢ 𝐺 Fn ω
Theorem	seqom0g 7551	Value of an index-aware recursive definition at 0. (Contributed by Stefan O'Rear, 1-Nov-2014.) (Revise by AV, 17-Sep-2021.)
⊢ 𝐺 = seq𝜔(𝐹, 𝐼)    ⇒   ⊢ (𝐼 ∈ 𝑉 → (𝐺‘∅) = 𝐼)
Theorem	seqomsuc 7552	Value of an index-aware recursive definition at a successor. (Contributed by Stefan O'Rear, 1-Nov-2014.)
⊢ 𝐺 = seq𝜔(𝐹, 𝐼)    ⇒   ⊢ (𝐴 ∈ ω → (𝐺‘suc 𝐴) = (𝐴𝐹(𝐺‘𝐴)))
2.4.18  Ordinal arithmetic
Syntax	c1o 7553	Extend the definition of a class to include the ordinal number 1.
class 1𝑜
Syntax	c2o 7554	Extend the definition of a class to include the ordinal number 2.
class 2𝑜
Syntax	c3o 7555	Extend the definition of a class to include the ordinal number 3.
class 3𝑜
Syntax	c4o 7556	Extend the definition of a class to include the ordinal number 4.
class 4𝑜
Syntax	coa 7557	Extend the definition of a class to include the ordinal addition operation.
class +𝑜
Syntax	comu 7558	Extend the definition of a class to include the ordinal multiplication operation.
class ·𝑜
Syntax	coe 7559	Extend the definition of a class to include the ordinal exponentiation operation.
class ↑𝑜
Definition	df-1o 7560	Define the ordinal number 1. (Contributed by NM, 29-Oct-1995.)
⊢ 1𝑜 = suc ∅
Definition	df-2o 7561	Define the ordinal number 2. (Contributed by NM, 18-Feb-2004.)
⊢ 2𝑜 = suc 1𝑜
Definition	df-3o 7562	Define the ordinal number 3. (Contributed by Mario Carneiro, 14-Jul-2013.)
⊢ 3𝑜 = suc 2𝑜
Definition	df-4o 7563	Define the ordinal number 4. (Contributed by Mario Carneiro, 14-Jul-2013.)
⊢ 4𝑜 = suc 3𝑜
Definition	df-oadd 7564*	Define the ordinal addition operation. (Contributed by NM, 3-May-1995.)
⊢ +𝑜 = (𝑥 ∈ On, 𝑦 ∈ On ↦ (rec((𝑧 ∈ V ↦ suc 𝑧), 𝑥)‘𝑦))
Definition	df-omul 7565*	Define the ordinal multiplication operation. (Contributed by NM, 26-Aug-1995.)
⊢ ·𝑜 = (𝑥 ∈ On, 𝑦 ∈ On ↦ (rec((𝑧 ∈ V ↦ (𝑧 +𝑜 𝑥)), ∅)‘𝑦))
Definition	df-oexp 7566*	Define the ordinal exponentiation operation. (Contributed by NM, 30-Dec-2004.)
⊢ ↑𝑜 = (𝑥 ∈ On, 𝑦 ∈ On ↦ if(𝑥 = ∅, (1𝑜 ∖ 𝑦), (rec((𝑧 ∈ V ↦ (𝑧 ·𝑜 𝑥)), 1𝑜)‘𝑦)))
Theorem	1on 7567	Ordinal 1 is an ordinal number. (Contributed by NM, 29-Oct-1995.)
⊢ 1𝑜 ∈ On
Theorem	2on 7568	Ordinal 2 is an ordinal number. (Contributed by NM, 18-Feb-2004.) (Proof shortened by Andrew Salmon, 12-Aug-2011.)
⊢ 2𝑜 ∈ On
Theorem	2on0 7569	Ordinal two is not zero. (Contributed by Scott Fenton, 17-Jun-2011.)
⊢ 2𝑜 ≠ ∅
Theorem	3on 7570	Ordinal 3 is an ordinal number. (Contributed by Mario Carneiro, 5-Jan-2016.)
⊢ 3𝑜 ∈ On
Theorem	4on 7571	Ordinal 3 is an ordinal number. (Contributed by Mario Carneiro, 5-Jan-2016.)
⊢ 4𝑜 ∈ On
Theorem	df1o2 7572	Expanded value of the ordinal number 1. (Contributed by NM, 4-Nov-2002.)
⊢ 1𝑜 = {∅}
Theorem	df2o3 7573	Expanded value of the ordinal number 2. (Contributed by Mario Carneiro, 14-Aug-2015.)
⊢ 2𝑜 = {∅, 1𝑜}
Theorem	df2o2 7574	Expanded value of the ordinal number 2. (Contributed by NM, 29-Jan-2004.)
⊢ 2𝑜 = {∅, {∅}}
Theorem	1n0 7575	Ordinal one is not equal to ordinal zero. (Contributed by NM, 26-Dec-2004.)
⊢ 1𝑜 ≠ ∅
Theorem	xp01disj 7576	Cartesian products with the singletons of ordinals 0 and 1 are disjoint. (Contributed by NM, 2-Jun-2007.)
⊢ ((𝐴 × {∅}) ∩ (𝐶 × {1𝑜})) = ∅
Theorem	ordgt0ge1 7577	Two ways to express that an ordinal class is positive. (Contributed by NM, 21-Dec-2004.)
⊢ (Ord 𝐴 → (∅ ∈ 𝐴 ↔ 1𝑜 ⊆ 𝐴))
Theorem	ordge1n0 7578	An ordinal greater than or equal to 1 is nonzero. (Contributed by NM, 21-Dec-2004.)
⊢ (Ord 𝐴 → (1𝑜 ⊆ 𝐴 ↔ 𝐴 ≠ ∅))
Theorem	el1o 7579	Membership in ordinal one. (Contributed by NM, 5-Jan-2005.)
⊢ (𝐴 ∈ 1𝑜 ↔ 𝐴 = ∅)
Theorem	dif1o 7580	Two ways to say that 𝐴 is a nonzero number of the set 𝐵. (Contributed by Mario Carneiro, 21-May-2015.)
⊢ (𝐴 ∈ (𝐵 ∖ 1𝑜) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ≠ ∅))
Theorem	ondif1 7581	Two ways to say that 𝐴 is a nonzero ordinal number. (Contributed by Mario Carneiro, 21-May-2015.)
⊢ (𝐴 ∈ (On ∖ 1𝑜) ↔ (𝐴 ∈ On ∧ ∅ ∈ 𝐴))
Theorem	ondif2 7582	Two ways to say that 𝐴 is an ordinal greater than one. (Contributed by Mario Carneiro, 21-May-2015.)
⊢ (𝐴 ∈ (On ∖ 2𝑜) ↔ (𝐴 ∈ On ∧ 1𝑜 ∈ 𝐴))
Theorem	2oconcl 7583	Closure of the pair swapping function on 2𝑜. (Contributed by Mario Carneiro, 27-Sep-2015.)
⊢ (𝐴 ∈ 2𝑜 → (1𝑜 ∖ 𝐴) ∈ 2𝑜)
Theorem	0lt1o 7584	Ordinal zero is less than ordinal one. (Contributed by NM, 5-Jan-2005.)
⊢ ∅ ∈ 1𝑜
Theorem	dif20el 7585	An ordinal greater than one is greater than zero. (Contributed by Mario Carneiro, 25-May-2015.)
⊢ (𝐴 ∈ (On ∖ 2𝑜) → ∅ ∈ 𝐴)
Theorem	0we1 7586	The empty set is a well-ordering of ordinal one. (Contributed by Mario Carneiro, 9-Feb-2015.)
⊢ ∅ We 1𝑜
Theorem	brwitnlem 7587	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 ∖ 1𝑜))    &   ⊢ 𝑂 Fn 𝑋    ⇒   ⊢ (𝐴𝑅𝐵 ↔ (𝐴𝑂𝐵) ≠ ∅)
Theorem	fnoa 7588	Functionality and domain of ordinal addition. (Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro, 8-Sep-2013.)
⊢ +𝑜 Fn (On × On)
Theorem	fnom 7589	Functionality and domain of ordinal multiplication. (Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro, 8-Sep-2013.)
⊢ ·𝑜 Fn (On × On)
Theorem	fnoe 7590	Functionality and domain of ordinal exponentiation. (Contributed by Mario Carneiro, 29-May-2015.)
⊢ ↑𝑜 Fn (On × On)
Theorem	oav 7591*	Value of ordinal addition. (Contributed by NM, 3-May-1995.) (Revised by Mario Carneiro, 8-Sep-2013.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 +𝑜 𝐵) = (rec((𝑥 ∈ V ↦ suc 𝑥), 𝐴)‘𝐵))
Theorem	omv 7592*	Value of ordinal multiplication. (Contributed by NM, 17-Sep-1995.) (Revised by Mario Carneiro, 23-Aug-2014.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ·𝑜 𝐵) = (rec((𝑥 ∈ V ↦ (𝑥 +𝑜 𝐴)), ∅)‘𝐵))
Theorem	oe0lem 7593	A helper lemma for oe0 7602 and others. (Contributed by NM, 6-Jan-2005.)
⊢ ((𝜑 ∧ 𝐴 = ∅) → 𝜓)    &   ⊢ (((𝐴 ∈ On ∧ 𝜑) ∧ ∅ ∈ 𝐴) → 𝜓)    ⇒   ⊢ ((𝐴 ∈ On ∧ 𝜑) → 𝜓)
Theorem	oev 7594*	Value of ordinal exponentiation. (Contributed by NM, 30-Dec-2004.) (Revised by Mario Carneiro, 23-Aug-2014.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ↑𝑜 𝐵) = if(𝐴 = ∅, (1𝑜 ∖ 𝐵), (rec((𝑥 ∈ V ↦ (𝑥 ·𝑜 𝐴)), 1𝑜)‘𝐵)))
Theorem	oevn0 7595*	Value of ordinal exponentiation at a nonzero mantissa. (Contributed by NM, 31-Dec-2004.) (Revised by Mario Carneiro, 8-Sep-2013.)
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ ∅ ∈ 𝐴) → (𝐴 ↑𝑜 𝐵) = (rec((𝑥 ∈ V ↦ (𝑥 ·𝑜 𝐴)), 1𝑜)‘𝐵))
Theorem	oa0 7596	Addition with zero. Proposition 8.3 of [TakeutiZaring] p. 57. (Contributed by NM, 3-May-1995.) (Revised by Mario Carneiro, 8-Sep-2013.)
⊢ (𝐴 ∈ On → (𝐴 +𝑜 ∅) = 𝐴)
Theorem	om0 7597	Ordinal multiplication with zero. Definition 8.15 of [TakeutiZaring] p. 62. (Contributed by NM, 17-Sep-1995.) (Revised by Mario Carneiro, 8-Sep-2013.)
⊢ (𝐴 ∈ On → (𝐴 ·𝑜 ∅) = ∅)
Theorem	oe0m 7598	Ordinal exponentiation with zero mantissa. (Contributed by NM, 31-Dec-2004.) (Revised by Mario Carneiro, 8-Sep-2013.)
⊢ (𝐴 ∈ On → (∅ ↑𝑜 𝐴) = (1𝑜 ∖ 𝐴))
Theorem	om0x 7599	Ordinal multiplication with zero. Definition 8.15 of [TakeutiZaring] p. 62. Unlike om0 7597, this version works whether or not 𝐴 is an ordinal. However, since it is an artifact of our particular function value definition outside the domain, we will not use it in order to be conventional and present it only as a curiosity. (Contributed by NM, 1-Feb-1996.)
⊢ (𝐴 ·𝑜 ∅) = ∅
Theorem	oe0m0 7600	Ordinal exponentiation with zero mantissa and zero exponent. Proposition 8.31 of [TakeutiZaring] p. 67. (Contributed by NM, 31-Dec-2004.)
⊢ (∅ ↑𝑜 ∅) = 1𝑜