A transfinite sequence is a function whose domain is an ordinal $\alpha$. Let $C$ denote the class of all transfinite sequences of ordinals, and let $\text{On}$ denote the class of ordinals.
Use the transfinite recursion theorem to define a class function $\sum: C \to \text{On}$ such that
- $\sum_{i \in 0} x_i = 0$
- $\sum_{i \in \alpha+1} x_i = \left(\sum_{i \in \alpha} x_i \right) + x_\alpha$ for all ordinals $\alpha$
- $\sum_{i \in \alpha} x_i = \sup_{\beta \in \alpha} \sum_{i \in \beta} x_i$ for all nonzero limit ordinals $\alpha$
My attempt:
Let $G(x,y)$ be the operation defined by
$$G(x,y)= \begin{cases} 0 \text{ if } x=0 \\ x(\alpha)+y(\alpha) \text{ if } x,y \in C, \text{dom}(x) =\alpha+1, \text{ and } \alpha \in \text{dom} (y) \\ \cup \text{ran}(x) \text{ if } x\in C \text{ and } \text{dom}(x) \text{ is a nonzero limit ordinal} \\ 0 \text{ otherwise} \end{cases}$$
We interpret $G$ as a class function with parameter $y$. The transfinite recursion theorem yields an operation $F(x,y)$ satisfying $F(\alpha,y)=G(F_y \restriction \alpha,y)$ for all ordinals $\alpha$ and all sets $y$.
Lemma. If $\alpha$ is an ordinal and $y\in C$ with $\alpha\leq \text{dom}(y)$, then
$F(\alpha,y)$ is an ordinal
$F(\alpha,y)=F(\alpha,y\restriction \alpha)$
Proof. Both claims can be shown by transfinite induction on $\alpha$.
Now define $\sum: C \to \text{On}$ by $\sum(y)=F(\alpha,y)$, where $\alpha=\text{dom}(y)$. Then, using 1 and 2 above we can check that $\Sigma$ has the desired porperties.
Is this correct? Is there a simpler way to proceed?