While working on a project in operator algebras with a collaborator (and fellow MO user), we are able to successfully complete a transfinite induction assuming that the following has an affirmative answer.
Question: Let $\delta$ be a cardinal, considered as an initial ordinal, so that it is equal to the set of all ordinals of cardinality strictly less than $\delta$. Does there exist a nondecreasing function $\phi \colon \delta \to \delta$ such that, for all ordinals $1 \leq \lambda < \delta$, there exists $\gamma < \lambda$ such that $\phi(\gamma) \geq \lambda$?
If it happens to matter, we are only concerned with the case where $\delta$ is a limit cardinal. Any reasonably (transfinitely) constructive approach to writing down such $\phi$ seems to quickly run into issues of ordinal notation that are beyond our expertise. If an abstract existence argument is available, we will certainly still be happy. On the other hand, we fear that this may somehow depend on large cardinal issues.