I'm currently working through some set theory texts, and I am having some trouble with using the transfinite recursion theorem to create functions in the language of set theory. I am trying to sort out the use of the process where we write some formula of the form $$\phi = \text{'$f$ is a function' }\land \text{'dom($f$)}=\alpha\space\land\text{}...$$
to define a function. I'd like to get more practice with problems like this, so I would really appreciate if someone could point me in the direction of where to find examples or perhaps give an example. I appreciate any help.
These are examples in $\sf ZFC$, and they utilize a choice function.
You can use transfinite recursion to prove there is a bijection between $X$ and an ordinal. Fix a choice function from non-empty subsets of $X$ and use it for the recursive definition.
You can use transfinite recursion to prove that every vector space has a basis.
You can use transfinite recursion to prove that given a partial order, there is a maximal element, or an unbounded chain which is well-ordered.
You can use transfinite recursion to prove that every countable ordinal can be embedded into the rational numbers (this can be done without transfinite recursion, in a simpler way, but this is an example).
You can use transfinite recursion to define ordinal addition, multiplication and exponentiation (for bonus points: use transfinite induction to prove associativity, and other properties).