# How does one prove without the axiom of choice that the product of a collection of nonempty well-ordered sets is nonempty?

Suppose $$\{X_{\alpha}\}_{\alpha\in\mathcal A}$$ is an indexed family of nonempty well-ordered sets, where $$X_{\alpha}=(E_{\alpha},\le_{\alpha})$$ for each $$\alpha$$. It seems intuitively obvious that we can prove, without the axiom of choice, that the product $$\prod_{\alpha\in\mathcal A}E_{\alpha}$$ is nonempty. The proof that immediately comes to mind is to define the function $$f:\mathcal A\to\bigcup_{\alpha\in\mathcal A}E_{\alpha}$$ by $$f(\alpha)=\min X_{\alpha}$$, where $$\min X_{\alpha}$$ denotes the minimum of $$X_{\alpha}$$ with respect to the order $$\le_{\alpha}$$. However, I'm not sure exactly which axioms from $$\mathsf{ZF}$$ allow us to define the function $$f$$. That is, I'm not sure how to prove, using the axioms of $$\mathsf{ZF}$$ alone, that there exists a function $$f:\mathcal A\to\bigcup_{\alpha\in\mathcal A}E_{\alpha}$$ such that for all $$\alpha\in\mathcal A$$ and $$y\in\bigcup_{\alpha\in\mathcal A}E_{\alpha}$$, $$(\alpha,y)\in f\implies (y\in E_{\alpha})\land(\forall z\in E_{\alpha}(y\le_{\alpha}z)) \, .$$ How would one do this? I suppose one could try applying the comprehension schema to the product $$\mathcal A\times\bigcup_{\alpha\in\mathcal A}E_{\alpha}$$ in some way, but I'm not clear on the details.

• I assume you mean "an indexed family of nonempty well-ordered sets"? Commented May 22 at 11:33
• I am not sure why you need to define such a function. The element $\langle \min X_\alpha \rangle_{\alpha\in \mathcal A}$ is an element of the product. Therefore the product is nonempty. Commented May 22 at 11:55
• @MikhailKatz: The Cartesian product of an indexed family of sets is defined as a certain collection of functions from the index set. The element which you speak of is the function $f$ in my post, at least under the usual set-theoretic definitions.
– Joe
Commented May 22 at 12:00
• If you think of a function as a set via its graph, then the fact that you can pass from a formula to the underlying set is the Axiom of Separation. You don't seem to be using much else. Commented May 22 at 12:50
• Yes, this is just comprehension/separation. Take $f$ to be the set of all $(\alpha,x)\in \mathcal A\times \bigcup_{\alpha\in \mathcal A}E_\alpha$ such that $x$ is the $<_\alpha$-least element of $E_\alpha.$ Commented May 22 at 19:58