I am trying to prove the following: In Zf, dependent choice (DC) and recursive construction (RCW) are equivalent where
and
(RCW):
Can you tell me if my proof in one direction is correct and help me with the other? Thank you.
(RCW) $\rightarrow$ (DC): Assume RCW and let $R$ be a binary relation on $X$ such that $\forall x \exists y : \langle x, y \rangle \in R$. Pick $x_0 \in X$ and define $G^\ast $ as $\langle f,0 \rangle \mapsto \{x_0\}$ and $\langle f,n \rangle \mapsto \{ x \mid \langle f(k), f(k+1) \rangle \in R \text{ for } 0 \le k \le n-2 \land \langle f(n-1), x\rangle \in R \}$. Then $f(n) \in G^\ast (F\mid I(n), n)$ is the desired sequence.
(DC) $\rightarrow$ (RCW): Assume DC and let $X,Z,W$ and $G^\ast$ be as in RCW. Now we want to define a binary relation $R$ on $X$ such that for every $x$ there is a $y$ such that $\langle x,y\rangle \in R$ and such that the set of the $x_n$ we obtain defines a function $F$ as in $R^\ast$ somehow.
The problem is, I don't see how we can turn our countable sequence into something defining a function defined on a possibly uncountable set. How to prove this direction?