A Universe of Sorts

Let $(J, <)$ be a well-ordered set.
Denote by $[0, \alpha)$ the set $\{ j \in J : j < \alpha \}$ as suggestive notation. Similarly $[0, \alpha]$ is the set $\{ j \in J: j \leq \alpha \}$ .
Let $r: (\forall \alpha \in J, [0, \alpha) \rightarrow O) \rightarrow O$ be a recursion formula, which when given a function $f: [0, \alpha) \rightarrow O$ which is well defined on $J$ upto $\alpha$ , produce a value $r(\alpha) \in O$ that extends $f$ to be well defined at $\alpha$ .
We wish to find a function $f(j)$ such that for all $j \in J$ , $f(j) = r([0, j))$ . So this function $f$ is deterined by the recursion principle $r$ . We construct such a function by transfinite induction.
Let $J_0 \subseteq J$ be the set of $j \in J$ such that there exists a function $f_j: [0, j] \rightarrow O$ (see the closed interval!), which obeys the recursion formula upto $j$ . That is, for all other $k \leq j$ , we have that $f_j(k) = r(f_j|[0, k))$ . Choose $k \leq j$ so that we check that $f_j(j) = r(f_j|[0, j))$ .
Claim: the set $J_0$ is inductive.
Let $[0, j) \subseteq J_0$ . Thus, for all $k < j$ , there is a function $f_k: [0, k] \rightarrow O$ such that $f_k(l) = r(f_k|[0, l))$ .
We must show that $j \in J_0$ . So we must construct a function $f_j: [0, j] \rightarrow O$ such that ... (reader: fill in the blanks).
Handwavy: note that the set of functions $\{ f_k : k \in [0, j) \}$ all agree on their outputs since their outputs are determined by the recursion formula (Foraal: we can first prove that any function that satisfies the recursion scheme is uniquely defined).
Thus, we can build the function $g_j: [0, j) \rightarrow O$ given by $g_j \equiv \cup_{k \in [0, j)} f_j$ . That is, we literally take the "set union" of the functions as ordered pairs, as the functions are all compatible. This gives us a function defined upto $j$ .
The value of $f_j$ at $j$ must be $r(g_j)$ . So we finally define $f_j \equiv g_j \cup \{ (j, r(g_j) \}$ . This is a uniquely defined function as $r$ is a function: $r: [0, j) \rightarrow O$ thus produces a unique output for a unique input $g(j)$ .
We have a function $f_j$ that obeys the recursion schema: (1) at $j$ , it is defined to obey the recursion schema; At $k < j$ , it is written as union of prior $f_k$ which obey recursion schema by transfinite induction hypothesis.
Thus, we have $j \in J_0$ , witnessed by $f_j$ .
We have fulfilled the induction hypothesis. So $J_0 = J$ , and we have a set of function $\{ f_j : j \in J \}$ , all of which are compatible with each other and obey the recursion schema. We take their unions and define $f \equiv \cup_j f_j$ and we are done!

§ Transfinite Recursion: Proof