[proofplan]
We prove both implications. Assuming the [Axiom of Choice](/page/Axiom%20of%20Choice), we first replace each set $X_i$ by its tagged copy $\{i\} \times X_i$ so that distinct indices give distinct sets even when some $X_i$ are equal. A choice function on the set of tagged copies selects a pair $(i,x_i)$ for each index $i$, and the second coordinate gives an element of the product. Conversely, applying the product principle to the family indexed by a set $A$ of nonempty sets, with the $a$-th factor equal to $a$, produces exactly a choice function on $A$.
[/proofplan]
[step:Use tagged copies to turn an indexed family into a set of distinct nonempty sets]
Assume the Axiom of Choice. Let $I$ be a set, and let $(X_i)_{i \in I}$ be an indexed family of nonempty sets. Define, for each $i \in I$, the tagged set
\begin{align*}
Y_i := \{i\} \times X_i.
\end{align*}
Each $Y_i$ is nonempty because $X_i$ is nonempty. If $i,j \in I$ and $Y_i = Y_j$, then choosing any $(i,x) \in Y_i$ gives $(i,x) \in Y_j = \{j\} \times X_j$, hence $i=j$ by equality of ordered pairs. Thus the map
\begin{align*}
Y: I &\to \{Y_i : i \in I\} \\
i &\mapsto Y_i
\end{align*}
is injective, and every member of
\begin{align*}
B := \{Y_i : i \in I\}
\end{align*}
is a nonempty set.
[guided]
The reason for introducing tags is that the original family may repeat the same set: it can happen that $X_i = X_j$ with $i \neq j$. A choice function on the set $\{X_i : i \in I\}$ would then choose only once from that repeated set, while an element of the product must choose once for every index. To preserve the index, define
\begin{align*}
Y_i := \{i\} \times X_i
\end{align*}
for each $i \in I$. Since $X_i$ is nonempty, there exists $x \in X_i$, and then $(i,x) \in Y_i$, so $Y_i$ is nonempty.
We also need the tagged sets to be distinguishable by their indices. Suppose $Y_i = Y_j$. Since $Y_i$ is nonempty, choose $(i,x) \in Y_i$. Then $(i,x) \in Y_j = \{j\} \times X_j$, so $(i,x) = (j,y)$ for some $y \in X_j$. Equality of ordered pairs gives $i=j$. Therefore distinct indices give distinct tagged sets. Hence
\begin{align*}
B := \{Y_i : i \in I\}
\end{align*}
is a set of nonempty sets whose elements still remember the indices from which they came.
[/guided]
[/step]
[step:Apply the Axiom of Choice to the tagged family and extract an element of the product]
By the Axiom of Choice applied to $B$, there exists a function
\begin{align*}
c: B \to \bigcup B
\end{align*}
such that $c(Y_i) \in Y_i$ for every $i \in I$. Since $c(Y_i) \in \{i\} \times X_i$, there is a unique element $x_i \in X_i$ such that
\begin{align*}
c(Y_i) = (i,x_i).
\end{align*}
Define
\begin{align*}
f: I &\to \bigcup_{i \in I} X_i \\
i &\mapsto x_i.
\end{align*}
Then $f(i)=x_i \in X_i$ for every $i \in I$, so
\begin{align*}
f \in \prod_{i \in I} X_i.
\end{align*}
Therefore
\begin{align*}
\prod_{i \in I} X_i \neq \varnothing.
\end{align*}
[guided]
Now $B$ is exactly the kind of object to which the Axiom of Choice applies: it is a set, and every element of it is nonempty. Therefore there exists a function
\begin{align*}
c: B \to \bigcup B
\end{align*}
such that $c(Y) \in Y$ for every $Y \in B$. In particular, for every $i \in I$,
\begin{align*}
c(Y_i) \in Y_i = \{i\} \times X_i.
\end{align*}
Membership in this Cartesian product means that there is some $x_i \in X_i$ with
\begin{align*}
c(Y_i) = (i,x_i).
\end{align*}
The element $x_i$ is unique because ordered pairs have unique coordinates.
We now define a function by taking these second coordinates:
\begin{align*}
f: I &\to \bigcup_{i \in I} X_i \\
i &\mapsto x_i.
\end{align*}
For each $i \in I$, the construction gives $x_i \in X_i$, so $f(i) \in X_i$. This is precisely the defining condition for membership in the Cartesian product:
\begin{align*}
f \in \prod_{i \in I} X_i.
\end{align*}
Thus the product is nonempty.
[/guided]
[/step]
[step:Recover a choice function from the product principle]
Assume the Product Form. Let $A$ be a set whose elements are nonempty sets. Consider the indexed family $(X_a)_{a \in A}$ defined by
\begin{align*}
X_a := a
\end{align*}
for every $a \in A$. By the Product Form,
\begin{align*}
\prod_{a \in A} X_a \neq \varnothing.
\end{align*}
Choose
\begin{align*}
f \in \prod_{a \in A} X_a.
\end{align*}
Then $f$ is a function with domain $A$ and satisfies $f(a) \in X_a = a$ for every $a \in A$. Hence
\begin{align*}
f: A \to \bigcup A
\end{align*}
is a choice function on $A$. Since $A$ was arbitrary, the Axiom of Choice follows.
[guided]
To prove the converse, we start with an arbitrary set $A$ whose elements are nonempty sets. Our goal is to construct a function choosing one element from each $a \in A$.
Use $A$ itself as the index set. Define the indexed family $(X_a)_{a \in A}$ by
\begin{align*}
X_a := a
\end{align*}
for every $a \in A$. Each factor $X_a$ is nonempty because each element $a$ of $A$ is nonempty. Therefore the Product Form applies and gives
\begin{align*}
\prod_{a \in A} X_a \neq \varnothing.
\end{align*}
Choose an element
\begin{align*}
f \in \prod_{a \in A} X_a.
\end{align*}
By the definition of the product, $f$ is a function with domain $A$ and satisfies
\begin{align*}
f(a) \in X_a
\end{align*}
for every $a \in A$. Since $X_a=a$, this becomes
\begin{align*}
f(a) \in a
\end{align*}
for every $a \in A$. Also $f(a) \in a \subset \bigcup A$, so $f$ has codomain contained in $\bigcup A$, and we may view it as a function
\begin{align*}
f: A \to \bigcup A.
\end{align*}
Thus $f$ is a choice function on $A$. Because $A$ was arbitrary, the Axiom of Choice holds.
[/guided]
[/step]
[step:Conclude the equivalence]
The first two steps show that the Axiom of Choice implies the Product Form. The third step shows that the Product Form implies the Axiom of Choice. Therefore, over ZF, the Axiom of Choice is equivalent to the assertion that every indexed family of nonempty sets has nonempty Cartesian product.
[/step]
