Zermelo set theory and Zorn's lemma I have a specific question and a more vague web of questions (that are, however, the motivation for the specific question).
Specific: Can Zorn's lemma be proved in Zermelo set theory (with choice, but without the axiom of regularity)?
Motivation: I know that the axiom of replacement is needed to do some serious set theory, for example to discuss ordinal numbers. So Zermelo set theory doesn't suffice for that purpose. But it certainly suffices for most of the set theory mathematicians use in practice (I know the relationship to topos theory). But I wonder how many applications of set theory to "normal" mathematics can be proved within Zermelo set theory. Zorn's lemma is the first such application of real set theory that normal mathematics uses that came to my mind. How tragic is the lack of the axiom of regularity: is it used in any real application of set theory to mathematics? (By that I don't mean appealing concepts like the cumulative hierarchy, that is definitely important for pure set theoretical purposes.)
 A: Replacement is needed for constructing the von Neumann ordinals. But we can still consider well-ordered sets even when they don't have corresponding von Neumann ordinals.
We can still prove the necessary theorems for transfinite recursions, only that now it's not a global schema that takes a class function and returns a class function. Now it's a theorem about sets. So given a well-ordered set, we can still do recursion over that set.
We can still define what are ordered pairs by the Kuratowski encoding, and we can therefore encode functions and all that other things.
But most importantly, Zermelo's set theory still have power sets. Now let $P$ be a partial order where every chain has an upper bound.

*

*Fix a choice function from non-empty sets of $P$, which we can do since we have power set and choice.


*Fix a well-order which does not inject into $P$ (as a set, but we can relax this to mean order embedding if we really want). That's the "tricky" bit, but just recall that the original proof of Hartogs' theorem didn't use von Neumann ordinals. Indeed, it simply shows that every set has a well-ordered set which does not inject into it.


*Recurse over the well-order you've fixed, using the choice function you've fixed, and construct a chain that is either unbounded or has a maximal element (in $P$). That is, repeat the usual proof of Zorn's lemma.
We need neither Replacement nor Regularity for either of these things. We do need Power Set and Separation (and obviously Choice). But Zermelo got us covered on these.
