How can one prove the axiom of collection in ZFC without using the axiom of foundation?

Say I want to prove the axiom(s) of collection from the axiom(s) of replacement. If you have the axiom of foundation, then you can use Scott's trick to do this.

But suppose I'm working in a context without the axiom of foundation. How can I prove it then? It certainly seems like it ought to be possible using the axiom of choice instead. In particular, if you allow the axiom of global choice, it's quite easy. And if it's possible with global choice, it certainly ought to be possible with ordinary local choice! And yet so far I have not been able to make it work (again, without using the axiom of foundation).

How can you prove collection from replacement, without using foundation, and just using ordinary, local choice?

Thanks all!


The answer is that you can't.

Instead of omitting foundation, I'll add atoms. You can replace them by Quine atoms and have the same results without foundations to your liking.

We construct the same permutation model as in this answer: start with a proper class of atoms and global choice, and make the class of atoms have only finite subsets while preserving local choice.

Now consider the predicate $\varphi(x,y)$ stating that $x<\omega$ and $y$ is a set of atoms which is equinumerous with $x$. Since $\omega$ is still a set, and we have finite sets of atoms in every finite size, $\forall x\in\omega\exists y(\varphi(x,y))$.

However, if there is some $B$ such that $B$ is a set and for every $x\in\omega$ there is some $y\in B$ such that $\varphi(x,y)$ then $\bigcup B$ is an infinite set of atoms. Contradiction.