How does Axiom of Dependent Choice imply this weaker variant?

Question

Here is the excerpt from the textbook A Course in Mathematical Analysis by Prof D. J. H. Garling.

So I have the Theorem 1:

Given a set $A\neq\varnothing$, a mapping $\varphi:A\to P(A )\setminus \{\varnothing\}$, and $\bar{a}\in A$. Then there exists a sequence $$(a_{n})_{n\in \mathbb{N}}$$ such that $a_{0}=\bar{a}$ and $a_{n+1}\in \varphi(a_{n})$ for all $n\in \mathbb{N}$

Axiom of Choice:

Given a collection $A$ of nonempty sets, there exists a function $$c: A \to \bigcup_{A_{i} \in A}A_{i}$$ such that $c(A_{i})\in A_{i}$ for all $A_{i} \in A$.

Axiom of Dependent Choice:

Given a nonempty set $A$ and a binary relation $\mathcal{R}$ on $A$ such that for all $a\in A$, there exists $b\in A$ such that $a\mathcal{R}b$. There exists a sequence $$(a_{n})_{n\in \mathbb{N}}$$ such that $a_{n}\mathcal{R}a_{n+1}$ for all $n \in \mathbb{N}$.

The author states that The axiom of dependent choice states that this [Theorem 1] is always possible. But I can only infer Theorem 1 from Axiom of Choice, not from Axiom of Dependent Choice. Below is how I did it.

Using Axiom of Choice for the collection $P(A)\setminus \{\varnothing\}$ of nonempty sets, then there exists a choice function $$\varphi':P(A)\setminus \{\varnothing\} \to A$$ such that $\varphi'(X)\in X$ for all $X\in P(A)\setminus \{\varnothing\}$.

Let $\bar{\varphi}=\varphi'\circ \varphi:A\to A\implies\bar{\varphi}(a)=\varphi'(\varphi(a))\in \varphi(\bar{a})$ for all $a\in A$

To sum up, we have $\bar{\varphi}:A\to A$ and $\bar{a}\in A$. Applying Recursion Theorem, we get a sequence $$(a_{n})_{n\in \mathbb{N}}$$ such that $a_{0}=\bar{a}$ and $a_{n+1}=\bar{\varphi}(a_{n})\in\varphi(a_{n})$ for all $n\in \mathbb{N}$. So this $(a_{n})_{n\in \mathbb{N}}$ is the required sequence.

I would like you to check my above proof and check whether it is possible for Axiom of Dependent Choice to imply Theorem 1.

Many thanks for your help!

Answer 1

Here is how I would think about the problem:

Let $T$ be the set of all finite functions $$ s \colon n \to A $$ such that $n \in \mathbb N$, $s(0) = \bar{a}$ and, for all $i +1 < n$, $$ s(i+1) \in \phi(s(i)). $$ Let $R \subseteq T \times T$ be given by $$ R = \{(s,t) \in T^2 \mid t \text{ is a proper end-extension of } s \} = \{ (s,t) \in T^2 \mid s \subsetneq t \} $$

$R$ satisfies the requirement of DC (since $\phi(a) \neq \emptyset$ for all $a \in A$). Hence there is an infinite sequence (branch) $(s_n \mid n \in \mathbb N)$ through $T$ such that for all $m < n \in \mathbb N \colon s_m \subsetneq s_n$. Let $s := \bigcup_{n \in \mathbb N} s_n$. For each $k \in \mathbb N$ let $a_k := s(k)$. Then $(a_k \mid n \in \mathbb N)$ is as desired.

Answer 2

Let $\mathcal R =\{ (a,b) \in A \times A \mid a,b \in A \text{ and } b \in \phi(a) \}$, then $\mathcal R$ satisfies DC's requirement. Hence there is an infinite sequence (branch) $(a_n \mid n \in \mathbb N)$ through $A$ such that $a_{n+1} \in \phi(a_n)$ for all $n \in \mathbb N$.