[proofplan]
We prove the two implications separately. For the first, full choice selects one $R$-successor from each point of a serial relation, and ordinary recursion on $\mathbb{N}$ turns this successor map into an infinite $R$-chain. For the second, given countably many nonempty sets, we form the set of finite partial choice functions and use Dependent Choice on the relation "extend by one coordinate." The resulting infinite chain of finite approximations determines a genuine countable choice function.
[/proofplan]
[step:Use full choice to select a successor for each point of a serial relation]
Assume the [Axiom of Choice](/page/Axiom%20of%20Choice). Let $X$ be a nonempty set, and let $R \subset X \times X$ be serial.
For each $x \in X$, define the successor set
\begin{align*}
S_x := \{y \in X : (x,y) \in R\}.
\end{align*}
Seriality of $R$ says exactly that $S_x \neq \varnothing$ for every $x \in X$. Applying the Axiom of Choice to the family $(S_x)_{x \in X}$, we obtain a function
\begin{align*}
g: X &\to X
\end{align*}
such that $g(x) \in S_x$ for every $x \in X$. Hence
\begin{align*}
(x,g(x)) \in R
\end{align*}
for every $x \in X$.
[guided]
Assume the Axiom of Choice. We want to prove Dependent Choice, so we begin with the data appearing in Dependent Choice: a nonempty set $X$ and a serial relation $R \subset X \times X$.
The word "serial" means that every point has at least one successor. To package those successors into a family of nonempty sets, define, for each $x \in X$,
\begin{align*}
S_x := \{y \in X : (x,y) \in R\}.
\end{align*}
Because $R$ is serial, each $S_x$ is nonempty. The Axiom of Choice applies to the family $(S_x)_{x \in X}$ and gives a function
\begin{align*}
g: X &\to X
\end{align*}
such that $g(x) \in S_x$ for every $x \in X$.
Unpacking the definition of $S_x$, the membership $g(x) \in S_x$ means exactly that
\begin{align*}
(x,g(x)) \in R
\end{align*}
for every $x \in X$. Thus full choice has converted the multivalued relation $R$ into a single-valued successor map $g$ whose values still follow the relation $R$.
[/guided]
[/step]
[step:Build an infinite dependent sequence by recursion]
Since $X$ is nonempty, choose an element $x_1 \in X$. By recursion on $\mathbb{N}$, there exists a unique function
\begin{align*}
f: \mathbb{N} &\to X
\end{align*}
such that
\begin{align*}
f(1) &= x_1,\\
f(n+1) &= g(f(n)) \quad \text{for every } n \in \mathbb{N}.
\end{align*}
For every $n \in \mathbb{N}$, the defining property of $g$ gives
\begin{align*}
(f(n), f(n+1)) = (f(n), g(f(n))) \in R.
\end{align*}
Thus $f$ is an $R$-chain indexed by $\mathbb{N}$, proving Dependent Choice.
[guided]
We now turn the successor map $g$ into an infinite sequence. Since $X$ is nonempty, there exists an element $x_1 \in X$. The recursion principle for $\mathbb{N}$ gives a unique function
\begin{align*}
f: \mathbb{N} &\to X
\end{align*}
satisfying
\begin{align*}
f(1) &= x_1,\\
f(n+1) &= g(f(n)) \quad \text{for every } n \in \mathbb{N}.
\end{align*}
The point of defining $f$ recursively in this way is that every next term is produced by the selected successor map $g$. Therefore, for each $n \in \mathbb{N}$,
\begin{align*}
(f(n), f(n+1)) = (f(n), g(f(n))).
\end{align*}
From the previous step, $(x,g(x)) \in R$ for every $x \in X$. Applying this with $x = f(n)$ gives
\begin{align*}
(f(n), f(n+1)) \in R.
\end{align*}
So $f: \mathbb{N} \to X$ is an infinite sequence whose consecutive terms are related by $R$. This is precisely the conclusion of Dependent Choice.
[/guided]
[/step]
[step:Encode countable choice as dependent extension of finite choice functions]
Assume Dependent Choice. Let $(X_n)_{n \in \mathbb{N}}$ be a sequence of nonempty sets.
Let $\mathbb{N}_0 := \mathbb{N} \cup \{0\}$. Define $Y$ to be the set of all finite partial choice functions with initial-segment domain:
\begin{align*}
Y := \{s : \{1,\dots,m\} \to \bigcup_{n \in \mathbb{N}} X_n \mid m \in \mathbb{N}_0 \text{ and } s(i) \in X_i \text{ for every } i \in \{1,\dots,m\}\}.
\end{align*}
For $m=0$, the domain $\{1,\dots,m\}$ is $\varnothing$, so the empty function belongs to $Y$. Hence $Y \neq \varnothing$.
Define a binary relation $E \subset Y \times Y$ by declaring $(s,t) \in E$ exactly when there exists $m \in \mathbb{N}_0$ such that
\begin{align*}
\operatorname{dom}(s) &= \{1,\dots,m\},\\
\operatorname{dom}(t) &= \{1,\dots,m+1\},\\
t|_{\{1,\dots,m\}} &= s,\\
t(m+1) &\in X_{m+1}.
\end{align*}
The relation $E$ is serial on $Y$: if $s \in Y$ has domain $\{1,\dots,m\}$, then $X_{m+1}$ is nonempty, so choose $a \in X_{m+1}$ and define
\begin{align*}
t: \{1,\dots,m+1\} &\to \bigcup_{n \in \mathbb{N}} X_n
\end{align*}
by
\begin{align*}
t(i) &=
\begin{cases}
s(i), & 1 \leq i \leq m,\\
a, & i = m+1.
\end{cases}
\end{align*}
Then $t \in Y$ and $(s,t) \in E$.
[guided]
Assume Dependent Choice. We must prove Countable Choice, so take a sequence $(X_n)_{n \in \mathbb{N}}$ of nonempty sets.
The idea is to choose elements one at a time. Instead of trying to choose all elements simultaneously, we consider finite partial choices. Let $\mathbb{N}_0 := \mathbb{N} \cup \{0\}$, and define $Y$ by
\begin{align*}
Y := \{s : \{1,\dots,m\} \to \bigcup_{n \in \mathbb{N}} X_n \mid m \in \mathbb{N}_0 \text{ and } s(i) \in X_i \text{ for every } i \in \{1,\dots,m\}\}.
\end{align*}
Thus an element of $Y$ is a finite choice function whose domain is an initial segment of $\mathbb{N}$. When $m=0$, this initial segment is empty, and the empty function is an element of $Y$. Therefore $Y$ is nonempty, as required for Dependent Choice.
Next define the relation $E \subset Y \times Y$ by one-step extension. For $s,t \in Y$, we put $(s,t) \in E$ exactly when there exists $m \in \mathbb{N}_0$ such that
\begin{align*}
\operatorname{dom}(s) &= \{1,\dots,m\},\\
\operatorname{dom}(t) &= \{1,\dots,m+1\},\\
t|_{\{1,\dots,m\}} &= s,\\
t(m+1) &\in X_{m+1}.
\end{align*}
So $t$ agrees with $s$ on all previously chosen coordinates and adds one new choice from the next set.
We verify seriality of $E$. Let $s \in Y$, and suppose $\operatorname{dom}(s)=\{1,\dots,m\}$ for some $m \in \mathbb{N}_0$. Since $X_{m+1}$ is nonempty, there exists $a \in X_{m+1}$. Define
\begin{align*}
t: \{1,\dots,m+1\} &\to \bigcup_{n \in \mathbb{N}} X_n
\end{align*}
by
\begin{align*}
t(i) &=
\begin{cases}
s(i), & 1 \leq i \leq m,\\
a, & i = m+1.
\end{cases}
\end{align*}
Then $t(i) \in X_i$ for every $i \in \{1,\dots,m+1\}$: this follows from $s \in Y$ for $i \leq m$, and from $a \in X_{m+1}$ for the final coordinate. Hence $t \in Y$, and by construction $(s,t) \in E$. Thus $E$ is serial on $Y$.
[/guided]
[/step]
[step:Apply Dependent Choice to obtain an infinite chain of finite choices]
By Dependent Choice applied to the nonempty set $Y$ and the serial relation $E \subset Y \times Y$, there exists a sequence
\begin{align*}
u: \mathbb{N} &\to Y
\end{align*}
such that
\begin{align*}
(u(k),u(k+1)) \in E
\end{align*}
for every $k \in \mathbb{N}$.
Let $\ell: Y \to \mathbb{N}_0$ denote the length map, defined by the condition
\begin{align*}
\operatorname{dom}(s)=\{1,\dots,\ell(s)\}
\end{align*}
for each $s \in Y$. Since $(u(k),u(k+1)) \in E$, we have
\begin{align*}
\ell(u(k+1)) = \ell(u(k)) + 1
\end{align*}
for every $k \in \mathbb{N}$. By induction on $k$, for every $k \in \mathbb{N}$,
\begin{align*}
\ell(u(k)) = \ell(u(1)) + k - 1.
\end{align*}
In particular, for every $n \in \mathbb{N}$, there exists $k \in \mathbb{N}$ such that $n \leq \ell(u(k))$; for example, take $k=n+1$ if $\ell(u(1)) \geq 0$.
[guided]
Now the hypotheses of Dependent Choice have been verified: $Y$ is nonempty and $E$ is serial on $Y$. Therefore Dependent Choice gives a sequence
\begin{align*}
u: \mathbb{N} &\to Y
\end{align*}
such that
\begin{align*}
(u(k),u(k+1)) \in E
\end{align*}
for every $k \in \mathbb{N}$.
Each $u(k)$ is a finite partial choice function. To track how long these finite functions are, define the length map
\begin{align*}
\ell: Y &\to \mathbb{N}_0
\end{align*}
by requiring
\begin{align*}
\operatorname{dom}(s)=\{1,\dots,\ell(s)\}
\end{align*}
for each $s \in Y$. This is well-defined because every element of $Y$ has a unique initial-segment domain.
The relation $E$ means "extend by exactly one coordinate." Hence, from $(u(k),u(k+1)) \in E$, we get
\begin{align*}
\ell(u(k+1)) = \ell(u(k)) + 1
\end{align*}
for every $k \in \mathbb{N}$. An induction on $k$ gives
\begin{align*}
\ell(u(k)) = \ell(u(1)) + k - 1
\end{align*}
for every $k \in \mathbb{N}$. Therefore the lengths of the finite choices grow without bound. In particular, for every coordinate $n \in \mathbb{N}$, some $u(k)$ has length at least $n$; taking $k=n+1$ suffices because $\ell(u(1)) \in \mathbb{N}_0$.
[/guided]
[/step]
[step:Extract a countable choice function from the coherent chain]
Define
\begin{align*}
c: \mathbb{N} &\to \bigcup_{n \in \mathbb{N}} X_n
\end{align*}
as follows. For each $n \in \mathbb{N}$, choose any $k \in \mathbb{N}$ such that $n \leq \ell(u(k))$, and set
\begin{align*}
c(n) := u(k)(n).
\end{align*}
This definition is independent of the choice of $k$. Indeed, if $k \leq j$ and $n \leq \ell(u(k))$, then repeated use of the extension condition in $E$ gives
\begin{align*}
u(j)|_{\{1,\dots,\ell(u(k))\}} = u(k),
\end{align*}
so $u(j)(n)=u(k)(n)$. The same argument applies after interchanging two indices by comparing both with their maximum.
Since $u(k) \in Y$ and $n \in \operatorname{dom}(u(k))$, the definition of $Y$ gives
\begin{align*}
c(n)=u(k)(n) \in X_n.
\end{align*}
Thus $c$ is a choice function for $(X_n)_{n \in \mathbb{N}}$. This proves Countable Choice, and hence Dependent Choice implies Countable Choice.
[guided]
We now convert the infinite chain of finite choices into one function on all of $\mathbb{N}$. For every $n \in \mathbb{N}$, the previous step showed that there exists $k \in \mathbb{N}$ with $n \leq \ell(u(k))$. This means $n$ lies in the domain of the finite function $u(k)$.
Define
\begin{align*}
c: \mathbb{N} &\to \bigcup_{n \in \mathbb{N}} X_n
\end{align*}
by choosing such a $k$ and setting
\begin{align*}
c(n) := u(k)(n).
\end{align*}
We must check that this is well-defined, because there may be many indices $k$ for which $n \leq \ell(u(k))$.
Suppose $k \leq j$ and $n \leq \ell(u(k))$. Since each transition $(u(r),u(r+1)) \in E$ extends the previous finite function without changing its old values, repeated application of the extension condition gives
\begin{align*}
u(j)|_{\{1,\dots,\ell(u(k))\}} = u(k).
\end{align*}
Therefore
\begin{align*}
u(j)(n)=u(k)(n).
\end{align*}
If two admissible indices are not ordered in the desired direction, compare both with their maximum. This proves that $c(n)$ is independent of all choices made in defining it.
Finally, since $u(k) \in Y$ and $n \in \operatorname{dom}(u(k))$, the defining property of $Y$ gives
\begin{align*}
c(n)=u(k)(n) \in X_n.
\end{align*}
Thus $c$ selects one element from each $X_n$. Since the original sequence $(X_n)_{n \in \mathbb{N}}$ was arbitrary, Countable Choice follows from Dependent Choice.
[/guided]
[/step]
