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.
$\begingroup$
$\endgroup$
6
-
$\begingroup$ I assume you mean "an indexed family of nonempty well-ordered sets"? $\endgroup$– Naïm FavierCommented May 22 at 11:33
-
2$\begingroup$ 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. $\endgroup$– Mikhail KatzCommented May 22 at 11:55
-
1$\begingroup$ @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. $\endgroup$– JoeCommented May 22 at 12:00
-
1$\begingroup$ 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. $\endgroup$– Mikhail KatzCommented May 22 at 12:50
-
3$\begingroup$ 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.$ $\endgroup$– spaceisdarkgreenCommented May 22 at 19:58
|
Show 1 more comment