How does $\mathsf{ZF}$ prove the countability of ordinals coming out of functions such as the ordinal collapse function?

Question

I am reading about fast growing hierarchies and the ordinal functions that are used in the indices, which allow us to categorise fast growing functions by selecting fundamental sequences for these large countable ordinals. For instance the Veblen functions, or the ordinal collapsing function $\psi$. The countability of all of these ordinals is obvious if we use $\mathsf{AC}_{\omega}$ ($\Rightarrow$ a countable of union of countable sets is countable). My question is, how does one prove the same statements in $\mathsf{ZF}?$ (for instance, for large countable ordinals arising from these functions)

Answer 1

The countability result is often proven differently depending on the definition, although unfortunately I'm not sure the proofs given in the original published literature are choiceless. When the definition of the ordinal collapsing function is simply based on the minimum excludant from one of the closure sets (like in Buchholz's "A new system of proof-theoretic ordinal functions", where $\psi_\nu(\alpha)=\textrm{min}\{\beta\mid\beta\notin C_\nu(\alpha)\}$) often a cardinality argument is used - for example Buchholz uses the fact that $C_0(\alpha)$'s cardinality is less than $\Omega$ to show that there must exist $\beta<\Omega$ where $\beta\notin C_0(\alpha)$, so $\psi_0(\alpha)<\Omega$.

Otherwise, for definitions not just based on the minimum excludant, at least for definitions appearing in literature there seems to be another common general form of them, similar to this sketch on Buchholz's "A simplified version of local predicativity" (full definition of $\psi_\pi(\alpha)$ for $\pi\in\textrm{Reg}\cap I$ on p.140):

We have a binary $C(\alpha,\beta)\supseteq\beta$, and $\psi_\Omega(\alpha)$ is the least $\beta$ where $C(\alpha,\beta)\cap\Omega\subseteq\beta$. Buchholz proves each $\psi_\Omega(\alpha)$ is countable, by showing that setting $$\beta=\textrm{sup}\{C(\alpha,0),\,C(\alpha,C(\alpha,0)),\,C(\alpha,C(\alpha,C(\alpha,0))),\,\ldots\}$$ gives us the necessary $C(\alpha,\beta)\cap\Omega\subseteq\beta$ condition, so $\psi_\Omega(\alpha)\leq\beta$. Unfortunately I'm not sure whether the demonstration that this supremum is countable makes use of the assumption "a countable union of countable sets is countable", so I'm not sure if this proof is choiceless.