Axiom of Dependent Choice implies Axiom of Countable Choice [Proof Verification]

Question

I have searched over the forum but not found any similar question, so I post it here.

1. 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}$.

2. 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!

Answer 1

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.