Does the principle of schematic dependent choice follow from ZFCU?

Let ZFCU be ZFC modified in the usual way to allow for urelements but without an axiom stating that there is a set of all urelements. Let the principle of Schematic Dependent Choice (SDC) be:

$\forall x\exists y\phi(x, y) \to \forall x\exists f(\mbox{dom}(f) = \omega \wedge f(0) = x \wedge \forall n\in\omega: \phi(f(n), f(n+1)))$

Question: does SDC follow from ZFCU?

The answer is, as Noah suggests, negative.

Suppose that $\frak M$ is a model of $\sf ZFCU$ where $U$ is not a set. Consider the model generated by taking all the permutations of $U$ which are sets (namely, permutations of a subset of $U$, and therefore the identity elsewhere). And consider $\cal F$ to be the filter generated by $\langle\operatorname{fix}(E)\mid E\text{ finite set of atoms}\rangle$, where $\operatorname{fix}(X)$ is the pointwise stabilizer of a set. Let $\frak N$ be the permutation model defined from these, and I claim that:

1. $\frak N\models\sf ZFCU$.
2. $\frak N\not\models\sf SDC$.

To see (1) holds, first prove that every set of atoms in $\frak N$ is finite; that every transitive set in $\frak N$ contains only finitely many atoms; by induction on the rank of a set show that if $x$ is a transitive set and $E=x\cap U$, then $\operatorname{fix}(E)=\operatorname{fix}(x)$. In particular a classical theorem about permutation models is that if the pointwise stabilizer of a set is in the filter, then the set can be well-ordered.

To see that (2) holds, or rather that $\sf SDC$ fails, consider the statement $\phi(x,y)$ to be "If $x$ is a set of atoms, then $y$ is a set of atoms and $x\subsetneq y$". Of course every set of atoms can be extended to a larger set of atoms; but if $f$ exists as in the schema, then $\bigcup f(n)$ exists by replacement and union, but it has to be an infinite set of atoms.

Here is a tentative (better) example. I don't have time to work out all the details yet.

Start with a model of $\sf ZFCU$ where $U$ is not a set, and there is a bijection between $U$ and the ordinals. Let $F$ denote a definable class function from $U$ onto $\omega$ such that every fiber is a proper class. This is doable from the bijection with the ordinals, for example (which is really the only reason to require that bijection).

Now consider all the set permutations of $U$ which preserve $F$. Namely $\pi\colon U\to U$, which is the identity outside some set $d$, and $F(a)=F(\pi(a))$ for all $a\in d$.

Let $\cal F$ be the filter generated by $\{\operatorname{fix}(E)\mid E\text{ is any set of urelements and }F[E]\text{ is bounded in }\omega\}$. Let $\frak N$ be the permutation model.

1. $\frak N\models\sf ZFCU$.
2. $F$ is definable in $\frak N$.
3. There is no $f\colon\omega\to U$ such that $F(f(n))=n$.

Now consider the formula $\phi(x,y)$ to be "If $x$ is a finite partial inverse of $F$ [read: $F(x(n))=n$ for $n\in\operatorname{dom}(x)$], then so is $y$, and $x\subsetneq y$". This is an obvious counterexample to $\sf SDC$ as in the previous case.

If I understand ZFCU correctly, then the answer should be "no": there seems to be nothing ruling out a model $M$ of ZFCU in which the atoms do not form a set, there is a linear order $L$ on the class of atoms with no $L$-greatest element, and there is no infinite set of atoms. In such a case, SDC would fail for the formula $\phi(x, y)\equiv$"$x$ is not an atom or $y>_Lx$."

In fact, here's an outline of how to build such a model. Start with a countable model of ZFCU in which the atoms form a proper class which is linearly ordered by some definable relation $L$, of (external) order type $\mathbb{Q}$ - so $L$ is externally homogeneous. Now let $G$ be the group of $L$-automorphisms of the class of atoms, and let $\mathcal{F}$ be the filter of finite supports as usual; the permutation model constructed from $M$ via $G, \mathcal{F}$ should have the desired properties.

Note that if the atoms form a set, then (1) we would have to have an infinite set of atoms, of course, and (2) if we demanded instead "no injection from $\omega$ to atoms," this would violate choice. But since the atoms don't form a set, neither objection applies.