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