Infinite decreasing sequence for class relation without minimal elements

Question

Let us assume $<$ is some class relation without minimal elements, meaning $\forall a, \exists b, b< a$. This means that for every $n\in\omega$, one can build a decreasing function $f$ with domain $n+1$, meaning that $f(k+1)<f(k)$ for every $k\in n$. This is a very simple inductive argument.

My question is, how can we show the existence of a decreasing function whose domain is all $\omega$?

If I had access to a global choice function $\tau$, I could do the following. For every $n\in\omega$, inductively show the existence of functions with domain $n+1$ such that $f(0)=\varnothing$ and $$f(k+1)=\tau\{x\in V_\alpha|x<f(k)\}$$ for $k\in n$, where $\alpha$ is the least ordinal such that $V_\alpha$ contains some set less than $f(k)$, as in Scott's trick. Then I could simply use replacement and union over all of these to get the desired set.

Since ZFC with global choice is a conservative extension of ZFC, I understand that there should be some way to prove this result without invoking global choice, at least for a fixed class relation $<$. But how?

Answer 1

Why do you need a global choice function, though? Yes, it's neater, but unnecessary.

Define, for each $x\in V_\alpha$ an ordinal $\alpha_x$ such that it is the minimal for which $V_{\alpha_x}$ contains witnesses that $x$ is not minimal in $<$. Now let $\alpha_0$ be defined for witnesses that $\varnothing$ is not minimal; then $\alpha_{n+1}=\sup\{\alpha_x\mid x\in V_{\alpha_n}\}$. Finally, $\alpha=\sup\alpha_n$.

Now all you need is to have a choice function for $V_\alpha$. This can be modified, of course, to start with any set, not just $\varnothing$.

Alternatively, use Reflection to find some $V_\alpha$ such that $(V_\alpha,<\restriction V_\alpha)$ reflects the "no minimal elements", which is essentially what we did before, and then work with a choice function for that specific $V_\alpha$.