# Axiom of Choice iff Every set has a choice function

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.

• Your choice function -> AoC argument looks wrong to me. 'By supposition, this set has a choice function defined over non-empty subsets', but you haven't shown that there are any non-empty subsets of D! That is, after all, the thing you're trying to prove. Jul 19, 2017 at 0:18
• Also, you index over 'finite' products $A_1\ldots A_n$, but that doesn't take AC; the non-emptyness of a finite product can be proven in ZF. Choice is only relevant for infinite products. Jul 19, 2017 at 0:20
• For some basic information about writing math at this site see e.g. here, here, here and here. Sep 4, 2017 at 6:04
• The set-theoretic def'n of $\prod_{j\in J}A_j$ is the set of functions from $J$ into $\cup \{A_j:j\in J\}$ that satisfy $\forall j\in J\;(f(j)\in A_j).$ Sep 4, 2017 at 8:28

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.

• Thank you for the feedback; I appreciate it! Btw, this is just for my own interest; not for a class or anything... Jul 19, 2017 at 14:13
• A member of $P=\prod_{a\in A}A_a$ is a choice-function for $\{A_a:a\in A\}$ by the def'n of $P$ and the def'n of a choice-function. So the proposition is essentially a tautology. Jul 19, 2017 at 16:35
• Your answer is clear, full of relevant definitions, and concise! Feb 23, 2018 at 7:42