Let us assume that we have only statement of transfinite induction. (And maybe some other well-know axioms)
My question: "Is it possible to derive from it a regularity axiom as a theorem?".
Some of my thoughts:
Definition 1:
$S(x):=(\exists a.a\in x)\rightarrow (\exists y\in x . \neg \exists z\in y.z\in x)$
Main theorem: $\forall x. S(x)$.
Proof: Firstly, apply transfinite induction. Now we need to show that $\forall x. \big((\forall z\in x.S(z))\rightarrow S(x)\big)$.
In order to prove it, let's start a proof by contradiction.
Assume that there exists M such that $(\forall z\in M.S(z))\land \neg S(M)$. Now we need to prove a false. … (I got stuck here.)
It may be useful to prove lemma like $z\in M \land S(M) \rightarrow S(z)$. (That's because we would immediately get a desired contradiction.)
But I don't know whether it is true. Any comments are welcome.
Edited:
I am currently verifying this theorem in coq-contrib/zfc library and obtain the next situation. (I think I properly followed Andreas' instructions.)
Now we have $z\in u$, $z\in x$, $x\in u$, $(\mbox{hyp} : \forall y \in x .P (y))$. We also have proved $P[z/x]$, where $P$ is your LaTeX formula.(by IndHyp). Our aim is to prove False from this context. What are the next steps?
Edited 2:
Self-contained code of the unfinished(!) theorem may be found here:
https://gist.github.com/georgydunaev/f24883f05ebaadb8c658cf53858646da
Edited 3 (final):
I've wrote a full solution here:
https://github.com/georgydunaev/zfc/blob/master/3_Regularity.v
Best Answer
Prove, by $\in$-induction on $x$, that all sets $x$ have the following property. $$ \forall u\,\big(x\in u\implies (\exists y\in u)(\forall z\in u)\,z\notin y)\big). $$ That is, every set $u$ that contains $x$ also contains an $\in$-minimal member. The idea of the proof is that, if $x$ is not $\in$-minimal in $u$, then the counterexample to minimality is a member of $x$ and therefore subject to the induction hypothesis.