Finite predecessor closures are sets

Given: Work in ZF unless the statement explicitly weakens or supplements it; fix the objects and hypotheses of the statement.

Let $X$ be a definable class and $R$ a definable binary relation on $X$, with fixed set parameters. Write ${\mathrm{pred}}_R(x)=\{y\in X:yRx\}$. The relation is setlike if this predecessor collection is a set for every $x\in X$. It is well-founded if every nonempty set $A\subseteq X$ has an $R$-minimal member $x$, meaning ${\mathrm{pred}}_R(x)\cap A=\mathrm{\varnothing }$. These are schemes in first-order set theory: a class is notation for a defining formula. No transitivity or totality of $R$ is required. Every relation on a set is setlike. An ordinal carries a well-founded membership relation by its definition; ambient Foundation does not make every arbitrary relation well-founded. All results concerning a supplied well-founded setlike relation are valid in ZF without Foundation unless stated otherwise. Conventions and prerequisites: def-ordinal. (Well-founded and setlike relations)

Let $(W,<)$ be a well-order (def-well-order) and let $G$ be a class function: a rule, given by a formula in the language of set theory, that assigns a set $G(h)$ to every function $h$ whose domain is a proper initial segment of $W$ (def-initial-segment). Then there is exactly one function $F$ with domain $W$ such that $F(a)=G(F\upharpoonright W_{<a})\text{for every }a\in W\mathrm{.}$ Here $F\upharpoonright W_{<a}$ is the restriction of $F$ to the initial segment determined by $a$, so the value of $F$ at $a$ is prescribed in terms of all its earlier values at once. Because $G$ is a class function rather than a set, this is a theorem schema of ZF: one theorem for each formula defining $G$. It uses Replacement, and it uses no form of the Axiom of Choice. (Transfinite recursion)