Axiom of Dependent Choice implies Axiom of Countable Choice [Proof Verification] I have searched over the forum but not found any similar question, so I post it here.


*

*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$.

My proof that Axiom of Dependent Choice implies Axiom of Countable Choice:

Let $T=\{s: n \to X \mid n \in \mathbb N \text{ and } \forall k < n:s(k) \in A(k)\}$ and $\mathcal{R}=\{(u,v) \in T^2 \mid u \subsetneq v\}$.
Assume $s: n\to X$ such that $s\in T$. Let $s': n+1\to X$ such that $s'(x)=s(x)$ for all $x<n$ and $s'(n)\in A(n)$. Then $s'\in T$ and $s\subsetneq s'$. That is for all $s \in T$, there exists $s' \in T$ such that $s \mathcal{R} s'$. As a result, $\mathcal{R}$  satisfies the requirement of DC. Hence there is a sequence $(s_n \mid n \in \mathbb N)$ through $T$ such that for all $m \le n \in \mathbb N \colon s_m \subseteq s_n$. Let $f=\bigcup_{n \in \mathbb N} s_n$. Now we prove $f$ is the desired function. 1. f is a function Let $(k,a),(k,b) \in f$. Then $\exists u, v \in (s_n \mid n \in \mathbb N)$ such that $ (k,a) \in u, (k,b) \in v$. Assume $u \subsetneq v$. This implies $(k,a) \in v$. $(k,a),(k,b) \in v \implies a=b$. Thus $f$ is a function.2. $\mathrm{dom}(f)=\mathbb N$ $\forall s \in T: 0 \in \mathrm{dom}(s) \implies 0 \in \mathrm{dom}(f)$. Assume $n \in \mathrm{dom}(f)$. This implies $\exists s_{t} \in (s_n \mid n \in \mathbb N): n \in \mathrm{dom}(s_{t})$. On the other hand, $s_{t} \subsetneq s_{t+1} \implies n+1 \in \mathrm{dom}(s_{t+1}) \implies n+1 \in \mathrm{dom}(f)$. Thus $\mathrm{dom}(f)=\mathbb N$.3. Condition $f(n) \in A_n$ Let $(n,f(n)) \in f$. Then $\exists s_{t} \in (s_n \mid n \in \mathbb N): (n,f(n)) \in s_{t}$. $s_{t}(n) \in A_n \implies f(n) \in A_n$.

Please check if my above proof is correct. Many thanks for your help!
 A: The proof you give is correct.
A stylistic comment, but I think an important one: your use of "$\implies$" is odd. "$\implies$" connects statements. "Let $foo$ be blah" isn't really a statement; "foo is blah" is a statement. So 

"foo is blah $\implies$ foo is bleen"

is fine, but

"Let foo be blah $\implies$ foo is bleen"

would be better written as 

"Let foo be blah. Then foo is bleen."

or similarly.

Incidentally, there is another approach which will also work. First, we assume WLOG that the $A(i)$s are disjoint (if they're not, just replace $A(i)$ with $B(i):=A(i)\times \{i\}$ for each $i$, run the argument below, and then strip away the added right coordinates at the end). Now consider the relation $R(x, y)$ on $\bigcup_{n\in\mathbb{N}}A(n)$ which holds exactly when for some $n$ we have $x\in A(n)$ and $y\in A(n+1)$. Applying dependent choice we get a sequence $(x_i)_{i\in\mathbb{N}}$ where for some $n$, $x_i\in A(i+n)$ (basically, we might not "start at $0$"). This doesn't quite get us what we want, but there's only finitely much "error," so we can fix it without choice. Your approach is much better, in my opinion, I just think it's worth mentioning this one too.
