Fdtxjr

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 $mathbfA$ 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

$$
mathbfA = 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.

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 $mathcalA,$ not in $D.$ Moreover, I think we need to clarify some definitions.

First one definition

Definition: Let $mathcalA$ be a nonempty collection os sets. A surjective function $f$ from some set $J$ to $mathcalA$ is called an indexing function for $mathcalA.$ $J$ is called the index set. The collection $mathcalA,$ 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
$$ mathbfx:J to bigcup_alpha in JA_alpha$$
such that $mathbfx(alpha) in A_alpha$ for all $alpha in J.$

Now,

Existence of a choice function: Given a collection $mathcalA$ of nonempty sets, there exists a function
$$ c: mathcalA to bigcup_A in mathcalAA$$
such that $c(A)$ is an element of $A: c(A)in A$ for each $A in mathcalA.$

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 $mathcalA$ be a collection of nonempty sets. We have to prove that there exists a function $ c: mathcalA to bigcup_A in mathcalAA$ such that $c(A) in A$ for each $A in mathcalA.$ We first index $mathcalA$: let $J=mathcalA$ and $f:mathcalA to mathcalA$ given by $f(A)=A.$ Then $A_A in mathcalA$ is an indexed family of sets, so we can consider its cartesian product $prod_A in mathcalAA.$ By hypothesis, this product is nonempty, so there exists a function
$$ mathbfx: mathcalA to bigcup_A in mathcalAA$$
such that $mathbfx(A) in A$ for each $A in mathcalA.$ Then $c=mathbfx$ 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 $mathcalA$ and there is an indexing (i.e. surjective) function $f:J to mathcalA$ such that $f(alpha)=A_alpha in mathcalA$ for each $alpha in J.$ By the existence of choice function, there is a function $c:mathcalA to bigcup_A in mathcalAA$ such that $c(A) in A$ for each $A in mathcalA.$ Thus
the function
$$ mathbfx:= c circ f : J to mathcalA = bigcup_alpha in JA_alpha$$
satisfies $mathbfx(alpha)=c(f(alpha))=c(A_alpha) in A_alpha$ for each $alpha in J,$ so the product $prod_alpha in JA_alpha$ is nonempty.