How is transifnite recursion applied?

Question

I've been struggling to understand how ordinal addition, multiplication, and exponentiation, along with the Aleph function $\aleph$, are defined using Transfinite Recursion in Jech's Set Theory or Holz's, Steffens' & Weitz' Introduction to Cardinal Arithmetic. The former, for example, simply writes

We shall now define addition, multiplication and exponentiation of ordinal numbers, using Transfinite Recursion.

Definition 2.18 (Addition). For all ordinal numbers $α$

1. $α +0= α$,
2. $α + (β + 1) = (α + β) + 1$, for all $β$,
3. $α + β = \lim_{ξ→β}(α + ξ)$ for all limit $β > 0$.

Definition 2.19 (Multiplication). For all ordinal numbers $α$...

Definition 2.20 (Exponentiation). For all ordinal numbers $α$...

before continuing as if the definition was fully clear to the reader (perhaps it usually is, but it has remained unclear to me). My understanding, after reading this and this post, is that there is an intermediate step (Theorem(?) below) that is used implicitly. I'm writing the current post to check whether my understanding is correct.

---

Notation:

• $V$ is the universal class $\{x:x=x\}$.
• $\text{Ord}$ is the class of Ordinals.
• $\text{Suc}$ is the class of successor ordinals.
• $\text{Lim}$ is the class of limit ordinals.
• If $\beta$ is the successor ordinal of $\alpha$, then $\beta = \alpha + 1$ and $\alpha = \beta - 1$.
• If $\kappa$ is a cardinal, then the smallest cardinal greater than $\kappa$ is written $\kappa^+$.

---

From Jech's Set Theory:

Theorem 2.15 (Transfinite Recursion). Let $G$ be a function (on $V$ ), then there is a unique function $F$ on $\text{Ord}$ such that $$F(α) = G(F\upharpoonrightα)$$ for each $α\in\text{Ord}$. In other words, if we let $a_α = F(α)$, then for each $\alpha$ $$a_α = G\left(\langle a_ξ : ξ<α\rangle\right).$$

---

First question: is the following result true?

Theorem(?) Suppose we are given

1. Any set $x_0$.
2. A function $s$ on $\text{Suc}$.

Then, there exists a function $F$ on $\text{Ord}$ such that

$$F:\alpha \mapsto \begin{cases} x_0 & \text{ if } \alpha = 0\\ s\circ F(\alpha-1) & \text{ if } \alpha\in\text{Suc}\\ \lim_{\xi\to\alpha}F(\xi) & \text{ if } \alpha\in\text{Lim}\\ \end{cases}$$

Proof: let $G$ be a function on $V$ defined by

$$G:x \mapsto \begin{cases} 0 & \text{ if } x\text{ is not a function of ordinals}\\ x_0 & \text{ if } x = 0\\ s(a_{\alpha-1}) & \text{ if } x = \langle a_\xi : \xi<\alpha\in\text{Suc}\rangle\\ \lim_{\xi\to\alpha}a_\xi & \text{ if } x = \langle a_\xi : \xi<\alpha\in\text{Lim}\rangle\\ \end{cases}$$

by Trasfinite Recursion, there is a function $F$ on $\text{Ord}$ such that $\alpha\mapsto G(F\upharpoonright \alpha)$. We show all three conditions are met:

• $0\mapsto 0$ trivially.
• If $\alpha\in\text{Suc}$, then $F(\alpha) = G(F \upharpoonright \alpha) = G(\langle F(\xi) : \xi < \alpha\in\text{Suc}\rangle) = s\circ F(\alpha-1)$, as wanted.
• If $\alpha\in\text{Lim}$, then $F(\alpha) = G(F \upharpoonright \alpha) = G(\langle F(\xi) : \xi < \alpha\in\text{Lim}\rangle) = \lim_{\xi\to\alpha}F(\xi)$, as wanted. $$\square$$

---

Assuming the first question was answered in the affirmative:

Second question: is the theorem above the implicit intermediate step between Transfinite Recursion and defining ordinal addition, multiplication, exponentiation, the Aleph function, etc?

As an example, ordinal addition is often defined by applying, though it's not explain exactly how, Transfinite Recursion to the three conditions below:

1. $\alpha + 0 = \alpha$.
2. $\alpha + \beta = \left[\alpha + (\beta-1)\right] + 1$ if $\beta\in\text{Suc}$.
3. $\alpha + \beta = \lim_{\xi\to\beta}(\alpha + \beta)$ if $\beta\in\text{Lim}$.

As I see it Theorem(?) is being applied with $x_0 = 0$ and $s : \beta\mapsto \beta + 1$ to define ordinal addition. Ordinal multiplication (on the right, by $\alpha$) is defined by setting $x_0 = 0$ and $s:\beta\mapsto\beta+\alpha$, while ordinal exponentiation (base $\alpha$) sets $x_0 = 1$ and $s:\beta\mapsto\beta\cdot\alpha$.

As a last example, the Aleph function is defined using Theorem(?) with $x_0 = \omega$ and $s:\kappa\mapsto\kappa^+$ where $\kappa^+$ denotes the smallest cardinal greater than $\kappa$.