Well-ordered Cartesian product in ZF Can it be proved in ZF that the product $\prod_{\alpha < \kappa} S_\alpha$ is nonempty given$\{ S_\alpha \}_{\alpha < \kappa}$ a family of nonempty set and $\kappa > 0$ is an ordinal?

It seems possible with transfinite induction, yet I cannot seems to show the limit case holds for the predicate $\varphi(\alpha) := \exists f (f \text{ is a choice function for} \{ S_\beta \}_{\beta < \alpha})$
 A: No, of course not. Not even in the case that $\kappa=\omega$, as that would be exactly countable choice which is known to be unprovable.
Moreover, even if you assume that for any ordinal $\kappa$ the product of $\kappa$ non-empty sets is non-empty, you still cannot prove the axiom of choice in general. In fact, you cannot even prove that every uncountable cardinal is comparable with $\aleph_1$.
A: The transfinite induction you're probably imagining fails at every limit ordinal.
I suppose you're thinking "then take the union of the functions we have so far", but which of them? Since there are many sequences for each shorter length, in order for "take the union" to work you need to be able to point to just one of each length in a way that fits together -- but that is exactly what $\alpha$-choice which you're just trying to prove is for. So this argument actually begs the question.
Even though we think of the induction as a process that happens in sequence, that's not how it works formally. In the induction step for $\alpha$ all the induction hypothesis lets you assume is that there exist one or more sequences of every length shorter than $\alpha$ -- you don't have a particular selection of them already singled out as "the ones we chose in previous steps". There are no "previous steps", because the induction step in transfinite induction must be proved just once but for an arbitrary $\alpha$.
This may be easier to wrap your mind around if you remember how to prove transfinite induction from the fact that ordinals are well-ordered. In this proof you're not actually doing anything step by step -- it's an indirect proof where we say, once and for all, something like this:

Suppose the desired property fails for at least one ordinal. Then bla bla well-ordered bla bla, and therefore there is a smallest $\alpha$ that the property fails for. Then apply the induction step just once, for that $\alpha$, and conclude that the property doesn't actually fail there after all -- a contradiction.

This proof never applies the induction step to all the ordinals before the supposed first point where the property fails. So we shouldn't assume when we apply it that it "has already run", so to say, for the smaller ordinals. We just know that its conclusion is, somehow, true for each of them independently.
