Does iterating any definable in ZFC functional relation give a $\mathbb N$-indexed family of sets? Consider an extension of ZFC (the first-order theory with signature $\in$ and the usual axioms) by a constant $x$, and a binary relation $N$ that is functional, i.e., we have the additional axiom


*

*$\forall x\exists!y\,N(x,y)$


and a constant $x_0$.
My question is whether there is a proof from the axioms that there exists a set $S$ and a set-function $f\colon\mathbb N\to S$ so that $n\in\mathbb N\rightarrow N(f(n),f(n+1))$ and $f(0)=x_0$?
There is also an equivalent way of phrasing the question since the existence of such an $f$ implies that the two-variable formula $\phi(n,x)$ given by $\phi(n,x)\equiv f(n)=x$ satisfies:


*

*$\exists! x\,\phi(0,x)$

*$\phi(0,x_0)$

*$\forall n\left(n\in\mathbb N\rightarrow \forall y\left(\left(\exists x\left(\phi(n,x)\wedge N(x,y)\right)\right)\leftrightarrow\phi(n+1,y)\right)\right)$


and conversely, given such a formula $\phi$, since ZFC implies the induction principle of $\mathbb N$, we can derive from those properties that $\phi$ is functional ($\forall n\left(n\in\mathbb N\rightarrow\exists!x\,\phi(n,x)\right)$), by the axiom schema of replacement we obtain the existence of our desired set $S$ and the function $f$.
Hence my question is equivalent to asking whether there exists such a formula in the language of this extension. 

My question is ill-posed and its answer depends on whether I intend on extending the axiom schemes of replacement and comprehension to formulas involving the functional $N$.
If the axiom schemes are not extended, then the answer is clearly no as we can see by taking a countable model of ZFC, $x_0=$the zeroeth element uneder an enumeration, and $N$ the increment of that enumeration (which is what the accepted answer says).
If the axiom schemes are extended, then the answer is yes, and the formula $\phi$ given by the the usual argument establishing that transfinite recursion works. 
Specifically, (and with shorthands) $\phi(n+1,x)$ is given by "$x=g(n+1)$ where $g$ is any function $g\colon\{0,\dots,n+1\}\to T$ to a set $T$ such that $g(0)=x_0$ and $g(n+1)=T(g(n))$". 
 A: Let M be a countable transitive model of ZFC and let N be the graph of a function on M whose orbit starting at x is all of M. Then there is no f, S of the type you seek. But if you allow the use of N in the replacement scheme then such f, S exist. In particular if N is definable, this is true.
A: A few thoughts:


*

*The axiom scheme $$(\forall x)(\exists y)\phi(x,y) \to (\forall x)(\exists \langle z_i : i \in \omega\rangle)(\forall i \in \omega)[z_0 = x \land \phi(z_i,z_{i+1})]$$
is a form of the principle of dependent choice that is provable in ZFC. 

*If you extend the axiom schemes (comprehension and replacement) in ZFC to the new larger class of formulas (including $N$), then dependent choice for this larger language will also be provable. That will give an affirmative answer to the question. Similarly, if we make a extension by definitions that defines $N$, then dependent choice for the larger class of formulas will be provable.  

*If you extend the language but don't extend the axiom schemes to match, there is no reason to suspect you can prove things about $N$. For example, if $A$ is infinite, you can't even form $\{N(x) : x \in A\}$. 
