This question was asked on math.stackexchange and didn't receive an answer. But I think it's interesting, and I at least would love to know the answer.


Let ${\sf ZFCU}$ be the axioms of ${\sf ZFC}$ modified to allow for urelements in the usual way. We do not assume that the urelements form a set.


The question is whether ${\sf ZFCU}$ plus the axiom schema of collection---i.e.:


(Collection) $\forall x\exists y \phi(x, y) \to \forall z\exists w\forall x\in z\exists y\in w \phi(x, y)$


implies schematic dependent choice---i.e.:


(SDC) $\forall x\exists y\phi(x, y) \to \forall z\exists f(f(0) = z \wedge \forall n\phi(f(n), f(n+1)))$



Does the axiom schema of collection imply schematic dependent choice in ZFCU?
(Remark: Sam Roberts pointed out to me an error in the first version of the proof I posted earlier -- there was no reason that the desired automorphisms exist, as there was no specification of them on the atoms outside of the sets of atoms under consideration. The following is a significantly modified version, and I think this time it works. One should also compare with [Emil Jeřábek's](https://mathoverflow.net/questions/387424/does-the-axiom-schema-of-collection-imply-schematic-dependent-choice-in-zfcu#comment988246_387471) and [Sam Roberts'](https://mathoverflow.net/questions/387424/does-the-axiom-schema-of-collection-imply-schematic-dependent-choice-in-zfcu#comment988238_387471) comments regarding DC$\_{\omega\_1}$ in the original question and below this answer.)


Assuming foundation is included (in the sense that for every non-empty set $x$ with no atomic elements, there is $y\in x$ such that $y\cap x=\emptyset$), SDC follows:


Write $U$ for the entire universe (of all sets and atoms).


If there is only a set $A$ of atoms, then $U=V(A)$, i.e. $U$ is the union of the cumulative hierarchy $\left<V\_\beta(A)\right>\_{\beta\in\mathrm{Ord}}$ above $V\_0(A)=A$. In this case there's an easy argument by recursively collecting witnesses according to rank. That is, let $\beta\_0$ be the least ordinal $\beta$ such that there is $y\in V\_\beta(A)$ with $\varphi(z,y)$ (where $z$ was the given parameter). Then by collection, we can take $\beta\_1$ least such that for all $x\in V\_{\beta\_0}(A)$ there is $y\in V\_{\beta\_1}(A)$ such that $\varphi(x,y)$. Etc, producing $\left<\beta\_n\right>\_{n<\omega}$. From this information we can build a set relation and apply DC to it to get the DC-branch $f$, i.e. such that $f(0)=z$ and $\varphi(f(n),f(n+1))$ for each $n<\omega$.


So suppose $A$ is a proper class. We will adapt the argument just mentioned.


Remark: I use parametrized collection in the proof, but this follows from the axioms in a routine way, by folding parameters into the ``$x$'' in unparametrized collection and modifying $\phi$ appropriately.


Lemma 1: For every set $x$, the transitive closure of $x$ exists.


Proof: Just the usual thing, taking the union of $\bigcup^nx$ over all $n<\omega$.


Given a set of atoms $a$ and ordinal $\beta$, let $V\_\beta(a)$ be the cumulative hierarchy built above $V\_0(a)=a$.


Lemma 2: For every set $x$, there is a set $a$ of atoms and ordinal $\beta$ with $x\in V\_\beta(a)$.


Proof: Let $t$ be the transitive closure of $\{x\}$ and $a=t\cap A$. So it suffices to see $t\subseteq V(a)$. If not let $t'=t\backslash V(a)$, so $t'\neq\emptyset$ and $t'$ is not an atom, and note that $t'$ contains no atoms. By foundation there is (a set) $y\in t'$ such that $y\cap t'=\emptyset$. So since $y\subseteq t$, we have $y\subseteq V(a)$. But then by collection there is $\beta$ with $y\subseteq V\_\beta(a)$, but then $y\in V\_{\beta+1}(a)$, so $y\in V(a)$, a contradiction.


We now split into cases.


Case 1: For all cardinals $\kappa$ there is a set of atoms of cardinality $\kappa$.


Claim 1.1: Let $a,a'$ be sets of atoms of the same cardinality and $\pi:a\to a'$ a bijection, and $\pi^+:V(a)\to V(a')$ the resulting isomorphism. Then for all formulas $\varphi$ and all $x\in V(a)$, we have $\varphi(x)\Leftrightarrow\varphi(\pi^+(x))$ (with truth of $\varphi$ evaluated in $U$).


Proof: By (meta-)induction on formula complexity. If $\varphi$ is $\Sigma\_0$ then it is just absoluteness of $\Sigma\_0$ between $V(a)$ and $U$ and since $\pi^+$ is an isomorphism (the language can include a predicate interpreted as $A$, which is equivalent to the sets $a/a'$ when interpreted over $V(a)/V(a')$). Suppose it holds for $\Sigma\_n$ formulas, let $\varphi$ be $\Sigma\_n$, let $x\in V(a)$, and suppose there is $y\in U$ such that $\varphi(x,y)$. Let $b$ be some set of atoms which is disjoint from $a$ and such that there is such a $y\in V(a\cup b)$. Let $b'$ be a set of atoms of the same cardinality as $b$, which is disjoint from $a'$. This exists by Case 1 hypothesis. Then $a'\cup b'$ has the same cardinality as $a\cup b$. Let $\sigma:a\cup b\to a'\cup b'$ be a bijection extending $\pi$ (which bijected $a$ with $a'$ already). Let $\sigma^+:V(a\cup b)\to V(a'\cup b')$ be the resulting isomorphism. Then $\pi^+\subseteq\sigma^+$, and by induction, since $\varphi(x,y)$ is true, so is $\varphi(\sigma^+(x),\sigma^+(y))$, which suffices, proving Claim 1.1.


Now suppose that for all $x$ there is $y$ such that $\varphi(x,y)$, and let $z$ be given. Let $t\_z$ be the transitive closure of $\{z\}$ and $a\_z=A\cap t\_z$. Let $(\kappa\_0,\beta\_0)$ be the lexicographically least pair $(\kappa,\beta)$ of ordinals such that for some set $a$ of atoms of cardinality $\kappa$, with $a$ disjoint from $a\_z$, there is $y\in V\_\beta(a\_z\cup a)$ such that $\varphi(z,y)$.


Now suppose we have defined $(\kappa\_0,\beta\_0),\ldots,(\kappa\_n,\beta\_n)$.
Let $(\kappa\_{n+1},\beta\_{n+1})$ be the lex least pair $(\kappa,\beta)$ of ordinals such that for all sets $a\_0,a\_1,\ldots,a\_n$ of atoms, if $a\_z,a\_0,\ldots,a\_n$ are pairwise disjoint and each $a\_i$ has cardinality $\kappa\_i$, then there is a set $a'$ of atoms of cardinality $\kappa$ such that $a'$ is disjoint from $a\_z\cup a\_0\cup\ldots\cup a\_n$, and for all $x\in V\_{\beta\_n}(a\_z\cup a\_0\cup\ldots\cup a\_n)$, there is $y\in V\_{\beta}(a\_z\cup a\_0\cup\ldots\cup a\_n\cup a')$ such that $\varphi(x,y)$.


(Note that we allow $\kappa\_n=0$.)


(Such a pair $(\kappa,\beta)$ exists. For let $(a\_0,\ldots,a\_n)$ and $(a'\_0,\ldots,a'\_n)$ satisfy these conditions.
Using collection, there is a set $Y$ such that for all $x\in W=V\_{\beta\_n}(a\_z\cup a\_0\cup\ldots\cup a\_n)$, there is $y\in Y$ such that $\varphi(x,y)$. From $Y$ we can compute a $(\kappa,\beta)$ which works for $W$. But then the same $(\kappa,\beta)$ works for $W'=V\_{\beta\_n}(a\_z\cup a'\_0\cup\ldots\cup a'\_n)$, by Claim 1.1 and since by case hypothesis, we can always find a disjoint set of atoms of a given cardinality.)


Now fix a sequence $\left<a\_n\right>\_{n<\omega}$ of pairwise disjoint sets of atoms, disjoint from $a\_z$, with each $a\_i$ of cardinality $\kappa\_i$. (Exists by case hypothesis.) Note that there is $y\in V\_{\beta\_0}(a\_z\cup a\_0)$ such that $\varphi(z,y)$ and for each $n<\omega$, for each $x\in V\_{\beta\_n}(a\_z\cup a\_0\cup\ldots\cup a\_n)$ there is $y\in V\_{\beta\_{n+1}}(a\_z\cup a\_0\cup\ldots\cup a\_{n+1})$ such that $\varphi(x,y)$. So we have reduced the whole issue down to set-size, so applying choice, we get our DC-branch $f$, as desired.


Case 2: Otherwise. (There is some cardinal $\kappa$ such that there is no set of atoms of cardinality $\kappa$.)


Note that there are infinite sets of atoms, because for each $n<\omega$ there is a set of atoms of cardinality $n$, and applying collection. And given any set $a$ of atoms, there is an infinite set $b$ of atoms which is disjoint from $a$, for similar reasons and because $A$ is not a set.


Claim 2.1: There is a largest cardinal $\kappa$ such that there is a set of atoms of size $\kappa$.


Proof: Let $\kappa$ be the sup of all $\kappa'$ such that there is a set of atoms of size $\kappa'$. So $\kappa\geq\omega$. By collection, we can find a set $Y$ which contains a set of atoms of size $\kappa'$, for each $\kappa'<\kappa$. Let $\kappa$ be the cardinality the set of atoms in the transitive closure of $Y$. Then $\kappa$ works.


Let $\kappa\_0=$ this largest $\kappa$.


Subcase 2.1: For every set $c$ of atoms of cardinality $\kappa\_0$, there is a set $b$ of atoms of cardinality $\kappa\_0$ which is disjoint from $c$.


This subcase is just a simplification of the subcase below.


Subcase 2.2: Otherwise. (There is a set $c$ of atoms of cardinality $\kappa\_0$ such that there is no set $b$ of atoms of cardinality $\kappa\_0$ with $c\cap b=\emptyset$.)


Let $c$ be a set as in Subcase 2.2 hypothesis. Then define $\mu\_c$ as the largest cardinality of a set of atoms $b$ which is disjoint from $c$. This largest cardinality exists like in the proof of Claim 2.1. Now let $\mu\_0$ be the least value of $\mu\_c$, ranging over all such $c$.
Let $c\_0$ witness this choice. Note that $\mu\_0\geq\omega$, since $A$ is not a set.


Claim 2.2: For every set $c$ of atoms disjoint from $c\_0$, there is a set $b$ of atoms disjoint from $c\cup c\_0$, such that $b$ has cardinality $\mu\_0$.


Proof: If not, let $c'=c\cup c\_0$ and observe that $\mu\_{c'}<\mu\_0$, a contradiction.


From here we can run a simple variant of the proof from Case 1, but starting with $c\_0\cup a\_z$ as our base set of atoms. That is:


Claim 2.3: Let $a,a'$ be sets of atoms of the same cardinality, which are disjoint from $c\_0$. Let $\pi:a\to a'$ a bijection, and $\sigma:V(c\_0\cup a)\to V(c\_0\cup a')$ the resulting isomorphism. Then for all formulas $\varphi$ and all $x\in V(c\_0\cup a)$, we have $\varphi(x)\Leftrightarrow\varphi(\sigma(x))$ (with truth evaluated in the entire universe).


Proof: This is now proved like its version in Case 1, but using Claims 2.2 and 2.3 (the properties of $c\_0$ and $\mu\_0$) to see that we can find appropriate disjoint sets of atoms (of cardinality at most $\mu\_0$).


The rest of the proof is like before; given a sequence $a\_0,\ldots,a\_n$ of sets of atoms disjoint from $c\_0\cup a\_z$, they each have cardinality $\leq\mu\_0$, and we can always find another set $a$ of atoms of cardinality $\mu\_0$ disjoint from the rest. (So in fact, since $\mu\_0\geq\omega$, one could just fix a sequence $\left<a\_i\right>\_{n<\omega}$ of sets $a\_i$ of atoms, each of cardinality $\mu\_0$, disjoint from $c\_0\cup a\_z$ and pairwise disjoint, and then argue that given an ordinal $\beta$, there is an ordinal $\beta'$ such that for every $x\in V\_{\beta}(c\_0\cup a\_z\cup a\_0\cup\ldots\cup a\_n)$ there is $y\in V\_{\beta'}(c\_0\cup a\_z\cup a\_0\cup\ldots\cup a\_n\cup a\_{n+1})$ such that $\varphi(x,y)$. Then we can define a resulting sequence $\left<\beta\_n\right>\_{n<\omega}$, and apply DC to sets as before.)


Remark: Considering @SamRoberts' and @EmilJeřábekand's comments below, we might have $\kappa\_0=\mu\_0=\omega$, hence no $\omega\_1$-sequence of atoms. In this case the proof wouldn't work to give DC$\_{\omega\_1}$, since it would rely on having a sequence $\left<a\_\beta\right>\_{\beta<\omega\_1}$ of pairwise disjoint (presumably non-empty) sets of atoms. We got a sequence like this above because we had the set of cardinality $\mu\_0$ of atoms to work with, and since (in the argument) $\mu\_0\geq\omega$, we can actually partition it as desired. But if $\mu\_0=\omega$, this clearly breaks when we want an $\omega\_1$-sequence.


