I have formalized Noah Schweber's idea to prove that Axiom of Dependent Choice implies Axiom of Countable Choice, but I'm not sure if my below proof is correct or not. Please have a look and check! Thank you for your help!
- Axiom of Dependent Choice
Let $T \neq\varnothing$ and $\mathcal{R} \subseteq T^2$ such that $\forall a \in T, \exists b \in T: a\mathcal{R}b$. Then there exists $(x_n \mid n \in \mathbb N)$ such that $x_n \mathcal{R} x_{n+1}$.
- Axiom of Countable Choice
Let $(A_n \mid n \in \mathbb N)$ be a sequence of non-empty sets and $X=\bigcup_{n \in \mathbb N} A_n$. Then there exists a mapping $f: \mathbb N \to X$ such that $f(n) \in A_n$.
Here is my take:
Let $\mathcal{R}=\{(x,y) \in X^2 \mid \exists n \in \mathbb N \text{ such that } x \in A_n \text{ and } y \in A_{n+1} \}$.
Clearly, $\mathcal{R}$ satisfies the requirement of DC. Hence there is a sequence $(x_i \mid i \in \mathbb N)$ where for some $n,x_i \in A_{i+n}$ $\forall i \in \mathbb N$.
Let $f: \mathbb N \to X$ in which $f(i) \in A_i$ $\forall i<n$ and $f(i)=x_{i−n}$ $ \forall i \geqslant n$.
Defining $f$ in this way, we have the desired function.