Proving dependent choice with initial value from dependent choice without

Question

A precise statement of the Axiom of Dependent Choice (DC1) is as follows:

$$\forall A,F\big[\big(A\ne\emptyset\wedge [F\!:A\to{\cal P}(A)-\{\emptyset\}]\big)\to\exists g\big([g\!:\omega\to A]\wedge(\forall n\in\omega)[g(n+1)\in F(g(n))]\big)\big]$$

In words, this says that for any set $A$, and any function $F$ from $A$ to nonempty subsets of $A$, there exists a sequence $g(n)$ such that $g(n+1)$ is a member of $F(g(n))$ for every $n$. (Note that this can be proven for a sequence of any given finite length by induction without needing any new axioms.)

I would like to prove, from this statement of the axiom, the following generalization (which I'll call DC2):

$$\begin{align} \forall x,A,F\big[\big(\!\!&x\in A\wedge [F\!:A\to{\cal P}(A)-\{\emptyset\}]\big)\to \\ &\quad\exists g\big([g\!:\omega\to A]\wedge g(0)=x\wedge(\forall n\in\omega)[g(n+1)\in F(g(n))]\big)\big] \end{align}$$

The obvious difference is that now the initial value is specified, where previously it was completely unrestricted (except that $g(0)\in A$). My question is how to reconstruct DC2 from DC1. Obviously going the other way is trivial, but if we were after a certain sequence starting from $x$, say ($x,x_1,x_2,\dots$), then in particular any sequence $x_n,x_{n+1},x_{n+2},\dots$ starting in the middle of the sequence is also a possible "solution to the equation" provided by the $g$ of DC1, since $F$ is "memoryless" and the initial value could be any point in the domain. Now this is alright, because if we actually coincide with a possible solution to the problem with $x$ as initial value (that is, there is some sequence of choices starting at $x$ and containing $x_n$), we can use finite induction to patch the sequence back together. But in general, this is not the case, and there seems to be no way to construct $F$ to restrict the values of $g$ at the beginning, since the initial value is completely unpredictable and the same $F$ is used for all $n$.

I understand that (DC1) is a statement of the axiom in some (many?) textbooks, so this problem must be surmountable. How would one deal with it?

Answer 1

Suppose you have $x,A,F$ as in the hypothesis of DC2. Let $S$ be the set of finite sequences of elements of $A$ whose first element is $x$ and whose successive terms are related by $F$, i.e., $s(n+1)\in F(s(n))$. So the elements of $S$ are finite partial approximations to the sort of infinite sequence demanded in DC2. For any $s\in S$, let $G(s)$ be the set of those $s'\in S$ obtainable by appending one additional element to the end of $s$. Now apply DC1 to $S$ and $G$ to get an infinite sequence of finite sequences, each extending the previous one by a single term. The union of all those finite sequences will be as required in DC2.