It is often tempting to think that all our existential instantiations happen "in advance", a sort of proof theoretic "mise en place" if you will.

But it's not, and it doesn't have to be. For a given $a$, we pick some $H$ and $H_i$'s, and so on. At each step, we only need to instantiate finitely many quantifiers.

Now, you may still wonder, how do we choose an element from a proper class? Well, the axiom of choice has absolutely nothing to do with that. As we know, a class is really a formula, i.e. $C$ is a class when there's some $\varphi(x)$ which defines it (we allow parameters, but I'm omitting them as they are fixed through this discussion anyway). To say that $C$ is not empty is exactly to say that $\exists x\,\varphi(x)$ holds. Now apply existential instantiation and we're done.

Even if you want to choose infinitely many elements from a class, which the above reasoning doesn't allow you, we can easily prove in $\sf ZF$ that no class is finite, and so that every class must contain an infinite set: simply look at $C\cap V_\alpha$, where $V_\alpha$ is the $\alpha$th step of the von Neumann hierarchy. Since we must add new elements unboundedly often, there is some $\alpha$ such that $C\cap V_\alpha$ is infinite. If we also assume choice, then we can even argue that we surpass every possible cardinality.