Why is the axiom of foundation not presented in terms of its, arguably more intuitive, negation? Informally, the axiom of foundation states that every non-empty set $x$ contains an element $y$ with which it is disjoint.
Formally the axiom appears as
$$
\forall x (x\not= \emptyset \implies \exists y (y\in x \land \lnot \exists z (z \in y \land z \in x)))
$$
It seems to me the most important consequence of the axiom of foundation is that there are no infinite descending chains of set membership e.g.:
$$
x_0 \ni x_1 \ni x_2\ni \ldots
$$
However, it's not immediately obvious to me why the absence of a disjoint member precludes the existence of such an infinite $\in$-chain.
There is a proof on Wikipedia that no infinite sequences of descending sets exist, but to even define an infinite sequence we require $\mathbb{N}$ and the axiom of infinity. I was curious if there is a way to state and prove there are no infinite descending sets without the axiom of infinity.
Then I did a few manipulations and realized the axiom of foundation states the desired result directly if you just manipulate it a little.
$$
\forall x (x\not= \emptyset \implies \exists y (y\in x \land \lnot \exists z (z \in y \land z \in x)))
$$
Apply $\forall x \phi \iff \lnot \exists x (\lnot\phi)$ along with $\lnot(\phi \implies \pi) \iff \phi \land \lnot \pi$ to get
$$
\lnot \exists x(x\not=\emptyset \land \lnot\exists y(y\in x \land \lnot \exists z(z\in y \land z \in x)))
$$
Now applying $\lnot \exists x\phi \iff \forall x \lnot \phi$ along with $\lnot(\phi \land \lnot \pi) \iff \phi \implies \pi$ we get
$$
\lnot \exists x(x\not=\phi \land \forall y(y\in x\implies \exists z(z\in y \land z\in x)))
$$
The negation of this would be the statement that there exists a non-empty $x$ which has the property that for every non-empty element $y\in x$ there is another element $z\in x$ satisfying $z\in y$. In other words, for every element $y\in x$ there is another element $z\in x$ with $z\in y$ so that $z$ is "one-step down the $\in$-chain" than $y$. In yet other words, the set $x$ would be a collection of all of the sets in the hypothetical $\in$ chain, and the axiom of foundation says that no such set exists.
My questions are as follows:
(1) Is all of what I've said above correct?
(2) If so, why can't I find this approach in the literature? I realize the answer is blah blah historical/social etc., but nonetheless, intuitive approaches should at least be mentioned and adopted somewhat.. Alternative, could someone point me to a reference that explains the axiom using this approach? Perhaps one reason the axiom is given in the form at the top is that it is a statement that $\in$ is a well-founded relation on every non-empty set?
(3) Finally a related but more technical question. As stated above, the axiom states that there is no collection of sets where each element contains another element in the set. What I can't wrap my head around is, if it could be possible (with or without the axiom of foundation) the have the existence of such a $\in$-chain while not having a collection of all the sets in the chain. I.e. $x_0 \ni x_1 \ni x_2 \ni \ldots$ but there is no set $\{x_0, x_1, x_2, \ldots\}$.
Perhaps some of the other axioms could always construct the set $\{x_0, x_1, x_2, \ldots\}$ given the $\in$-chain.
Could the collection set always be established even without the axiom of infinity?
 A: I frankly don't see much of a conceptual difference between your suggested phrasing and the usual version which says every nonempty set has an $\in$-minimal element. The intuition for picking out an infinite descending chain is right there in that formulation: let $x_0\in A$ be arbitrary. $x_0$ is not $\in$-minimal, so take $x_1\in x_0\cap A,$ and so on. Note that the role of the axiom of infinity is really just to make the sequence a set, so it is inessential in that sense. But on a side note, the construction does make essential use of the axiom of dependent choice.
Your third question could be reformulated somewhat to ask if it is true that every non-empty class has an $\in$-minimal element. In ZF, the answer is yes: If $C\ne 0$ is a class, let $x\in C.$ If $x$ is $\in$-minimal in $C$, great. Otherwise, $\operatorname{trcl}(x)\cap C$ is a nonempty set and thus has an $\in$-minimal element, which is necessarily $\in$-minimal in $C.$
The class version is quite important, since it is equivalent to the $\in$-induction scheme $$ \forall x\;( \forall y \in x\;\varphi(y)\to \varphi(x) ) \to \forall x \; \varphi(x).$$ But note the proof that  the class version follows from the set version relies on the existence of transitive closures, so it doesn't always hold in weak set theories. In particular, it doesn't necessarily hold in the absence of the axiom of infinity.
There is a simple model (necessarily only of a weak set theory without transitive closures) that satisfies set foundation but not class foundation. Start off in an ill-founded set theory with a sequence $a_0=\{a_1\},$ $a_1=\{a_2\}, \ldots,$ then recursively define $M_0=\{a_i: i\in\omega\},$ and $M_{n+1}$ be the set of all finite subsets of $M_n,$ and let $M=\bigcup_n M_n.$ Since the $a_i$ don't have any membership cycles and all the sets are finite, set-foundation holds, but clearly the $a_i$ are an infinite $\in$-descending class-sequence.
