I'd like to know if my proof is correct or incorrect in the following.
Given definition of Axiom of Choice (AoC): The direct product of a family of non-empty sets indexed by a non-empty set is non-empty.
Show that the Axiom of Choice is equivalent to the statement that every set has a choice function.
(Choice Function => AoC):
Suppose every set has a choice function.
Let S be a set, and fix a natural number n.
Let $$
I = \{1,2,….,n\}
$$
and let $\mathbf A$ be a family of non-empty subsets of S sets indexed over I.
$$
\mathbf A = \{A_1, A_2, … , A_n\}
$$
The task is to show that the direct product over sets in $\mathbf{A}$ is non-empty. This will be shown if an element of this set can be produced.
Let
$$
D = A_1 \times A_2 \times … \times A_n
$$
By supposition, this set has a choice function $f$ defined over non-empty subsets $X$ of $D$ with the following:
$f: X \to D$ such that $f(X)∈X$ for all subsets $X$.
So, $f(X) ∈ X$ $\Rightarrow$ $f(X) ∈ D$.
So, $D$ is non-empty.
(Show AoC => Choice Function):
Suppose the Axiom of Choice, let S be a set, and fix a natural number n.
Let
$$
I = \{1,2,….,n\}
$$
and let
$$
\mathbf{A} = \{A_1,A_2,….,A_n \}
$$
be a family of non-empty subsets of S indexed over I.
Let
$$
D = A_1 \times A_2 \times … \times A_n
$$
By the Axiom of choice, $D$ is non-empty.
Let $y ∈ D$ and define a function $f: D \to D$ by $f(x) = y$ for all elements $x ∈ D$.
(So, every element of D is mapped to this fixed element $y$.)
So, $f(x)∈D$ for all $x∈ D$.
In other words, $f$ defines a choice function on $D$.
So, assuming the Axiom of Choice implies that $S$ has a choice function defined on its non-empty subsets.
Best Answer
You are working only with finite products, and this hold in general. In the Choice Function $\Rightarrow$ AoC direction you don't know if $D$ is nonempty, that is what you are trying to pare working only with finite products, and this hold in general. In the AoC $\Rightarrow$ Choce Function direction you need a choice function on $\mathcal{A},$ not in $D.$ Moreover, I think we need to clarify some definitions.
First one definition
Definition: Let $\mathcal{A}$ be a nonempty collection os sets. A surjective function $f$ from some set $J$ to $\mathcal{A}$ is called an indexing function for $\mathcal{A}.$ $J$ is called the index set. The collection $\mathcal{A},$ together with $f,$ is called an indexed family of sets.
I'll use your definition of axiom of choice.
Axiom of choice: For any indexed family $\{ A_\alpha \}_{\alpha \in J}$ of nonempty sets, with $J \neq 0,$ the cartesian product $$ \prod_{\alpha \in J} A_\alpha$$ is not empty. Recall that the cartesian product is the set of all functions $$ \mathbf{x}:J \to \bigcup_{\alpha \in J}A_\alpha$$ such that $\mathbf{x}(\alpha) \in A_\alpha$ for all $\alpha \in J.$
Now,
Existence of a choice function: Given a collection $\mathcal{A}$ of nonempty sets, there exists a function $$ c: \mathcal{A} \to \bigcup_{A \in \mathcal{A}}A$$ such that $c(A)$ is an element of $A: c(A)\in A$ for each $A \in \mathcal{A}.$
Axiom of choice $\Rightarrow$ Existence of choice function.
We are assuming that for any indexed family $\{ A_\alpha \}_{\alpha \in J}$ of nonempty sets, with $J \neq 0,$ the cartesian product $ \prod_{\alpha \in J} A_\alpha$ is not empty. Let $\mathcal{A}$ be a collection of nonempty sets. We have to prove that there exists a function $ c: \mathcal{A} \to \bigcup_{A \in \mathcal{A}}A$ such that $c(A) \in A$ for each $A \in \mathcal{A}.$ We first index $\mathcal{A}$: let $J=\mathcal{A}$ and $f:\mathcal{A} \to \mathcal{A}$ given by $f(A)=A.$ Then $\{A\}_{A \in \mathcal{A}}$ is an indexed family of sets, so we can consider its cartesian product $\prod_{A \in \mathcal{A}}A.$ By hypothesis, this product is nonempty, so there exists a function $$ \mathbf{x}: \mathcal{A} \to \bigcup_{A \in \mathcal{A}}A$$ such that $\mathbf{x}(A) \in A$ for each $A \in \mathcal{A}.$ Then $c=\mathbf{x}$ is the function we were looking for.
Existence of choice function $\Rightarrow$ Axiom of choice
Now we are assuming that the existence of choice function, and let $\{A_\alpha \}_{\alpha \in J}$ be an indexed family of nonempty sets, with $J \neq 0.$ This means that there is a nonempty collection of sets $\mathcal{A}$ and there is an indexing (i.e. surjective) function $f:J \to \mathcal{A}$ such that $f(\alpha)=A_\alpha \in \mathcal{A}$ for each $\alpha \in J.$ By the existence of choice function, there is a function $c:\mathcal{A} \to \bigcup_{A \in \mathcal{A}}A$ such that $c(A) \in A$ for each $A \in \mathcal{A}.$ Thus the function $$ \mathbf{x}:= c \circ f : J \to \mathcal{A} = \bigcup_{\alpha \in J}A_\alpha$$ satisfies $\mathbf{x}(\alpha)=c(f(\alpha))=c(A_\alpha) \in A_\alpha$ for each $\alpha \in J,$ so the product $\prod_{\alpha \in J}A_\alpha$ is nonempty.