Is Foundation equivalent to $\forall_x (x \in V)$ in ZF-Foundation?

Question

Is Foundation equivalent to $\forall_x \exists_\alpha x \in V_\alpha$ (every set has a rank) in ZF-Foundation?

The Wikipedia article on Foundation makes this claim with no reference:

In ZF it can be proven that the class $V$, called the von Neumann universe, is equal to the class of all sets. This statement is even equivalent to the axiom of regularity (if we work in ZF with this axiom omitted). From any model which does not satisfy axiom of regularity, a model which satisfies it can be constructed by taking only sets in $V$.

I think I see how this works in one direction: if the rank is a total class function mapping sets to ordinals, then by Specification and Replacement every non-empty set has a non-empty subset containing the elements of smallest rank, and it's disjoint from every element of this subset, implying Foundation. I believe I did not use Choice here.

In the other direction, suppose $\{x: x \notin V\}$ is a class with a subclass $S = \{a, b, c, \dots\}$ satisfying $a \ni b \ni c \ni \dots$. More formally, $(S \neq \emptyset) \land (S \cap V = \emptyset) \land \forall_x(x \in S \rightarrow x \subset S)$. If $S$ were a set its existence would contradict Foundation because it's not disjoint from any of its elements. We could define a Foundation-violating set by transfinite recursion starting with $a$, if we had a class function sending every set to one of its elements — but that's equivalent to Choice!

Another way I was trying to look at it is, pick an $x \notin V$, and form its transitive closure. That set would not be disjoint from any of its elements. But I understand the transitive closure is defined by Specification from the rank of $x$ and we're assuming $x \notin V$ so it has no rank.

I'm probably missing something simple. How to prove this equivalence without Choice?

Answer 1

The key fact is:

If $a\not\in V$, then there is some $b\in a$ with $b\not\in V$.

Now choice may tempt us into trying to build - from a single $a\not\in V$ - an $\in$-decreasing sequence of sets not in $V$, by the above rule. Of course, this won't work without choice.

We can get around this as follows. By Replacement, the transitive closure $tcl(a)$ exists; now consider $x=$ "$tcl(a)\setminus V$," that is the set of elements of $tcl(a)$ not in $V$ (which exists by separation - $V$ is definable!). By the highlighted point above, for any $y\in x$ there is some $z\in y$ with $z\not\in V$; but then this $z$ is an element of an element of $tcl(a)$, and since $tcl(a)$ is transitive this tells us $z\in tcl(a)$. But then $z\in x$ since $z\not\in V$, and so we have $y\cap x\ni z$. So $x$ constitutes a failure of foundation.

Answer 2

If $x\in V$, then $\operatorname{tcl}(x)$ is well-founded. To see this: we prove two things:

1. If $x\in V_\alpha$, then $\operatorname{tcl}(x)\in V_\alpha$ as well.
2. If $x\subseteq y$ are two transitive sets and $y$ is well-founded, then $x$ is well-founded.

The former is easy by induction on $\alpha$. The latter is easy since if $z\in x$ is such that $\{u\in x\mid u\in z\}$ has no minimal element, then $z\in y$ is also a counterexample of well-foundedness there.