Function $f: \omega \to A$ with $f(0)=a$ and $f(i)Rf(i+1)$ in ZF Let $\mathcal{L}$ be a language containing a binary relation symbol $P$. Let $A$ be a set such that, for any $\mathcal{L}$-structure $\mathcal{A}$ having domain $A$ and any $a \in A$, there exists a countable $\mathcal{B}_a \preceq \mathcal{A}$ such that $a \in \mathcal{B}_a$.
Let $R \subseteq A \times A$ satisfy $(\forall x \in A) (\exists y \in A)xRy$.
Fix $a \in A$.

I want to show that there is a function $f: \omega \to A$ such that $f(0)=a$ and $f(i) R f(i+1)$ for every $i \in \omega$.

For the purposes of this question we are in ZF.
 A: Fix such an $A$ and $R$, and consider the $\mathcal{L}$-structure $\mathcal{A}$ with domain $A$ and interpretation $P^\mathcal{A}=R$. Fixing $a\in A$, let $\mathcal{B}_a$ be a countable elementary substructure of $\mathcal{A}$ containing $a$.
Since $\mathcal{B}_a$ is countable (in fact all we actually need is that it is well-orderable), we can enumerate its elements as $(b_i)_{i\in \omega}$. Now by elementarity and hypothesis on $R$, we have $\mathcal{B}_a\models\forall x\exists y(xPy)$. We can now just go along and pick elements using the enumeration above: set $$a_0=a,\quad a_{i+1}=b_{\min\{j: a_iPb_j\}}.$$ Note that at no point have we gone beyond $\mathsf{ZF}$: we only ever needed to make two "ad hoc" choices (the choice of $\mathcal{B}_a$ and the choice of enumeration of $\mathcal{B}_a$'s elements), and each of these was just an application of existential instantiation. The construction from this data of the sequence $(a_i)_{i\in\omega}$ is entirely deterministic: recursive constructions like this do not rely on choice (if anything it's replacement which plays a nontrivial role).
