"No infinite descending membership chains", Peano Axioms, Axiom of Regularity I use ZFC with the axiom of Regularity.


*

*At page 62 of my notes I prove that "There is no infinite descending membership chains" (because of well-ordering of $\mathbb{N}_0$), 

*The Lemma "No infinite descending membership chains" is connected with the Axiom of Regulatity (see for example here)

*In my notes I used the axiom of Regulatity only to prove that $x\notin x$ (special case of "No infinite descending membership chains").



My question is: If I had a pretty standard derivation of the natural numbers (with Peano axioms) at which point I could have applied (I mean: is applied in the standard derivation) the axiom of Regularity? I must have done some derivation using it but unknowingly.

EDIT Other formulation of my question.
I prove that "There is no infinite descending membership chains" (because of well-ordering of $\mathbb{N}_0$), without using directly the axiom of Regularity. But, since the "no infinite descending membership chains" is connected to the Axiom of Regularity, I must have applied it somewhere on the way, unknowingly. Q: At which point is applied the Axiom of Regularity in a standard derivation (using Peano) of the claim  "There is no infinite descending membership chains"?
EDIT Draw of the derivation
The construction of $\mathbb{N}_0$ is perhaps after all not that standard: see ch. 3.


*

*Ch. 1: Axioms of ZFC as in Wikipedia or Ciesielski1997 (there are some minor differences), nothing exotic. Consequences of the axioms (e.g $x\notin x$, aso). Set operations with their properties.

*Ch. 2: Relations and Functions

*Ch. 3: 3.1)  Natural Numbers: Set-theoretic definition: A natural number is a set that belongs to every inductive
set ($\varnothing \in x$ and $y\in x\to S(y)\in x$, where $S(x)=x\cup \{x\}$). 3.2) Peano System defined as $(X,i,f)$ (properties $f$ injective, $i\notin\textrm{ran}(f)$, $(X,i,f)$ has no proper subsystem). Properties of a Peano system. Proof that $\mathbb{N}_0$ (as defined in 3.1) is a Peano system. 3.3 recursion and isomorphism 3.4 operations on $\mathbb{N}_0$.

*Ch. 4: 4.1 Well-ordering 4.2 Ordering on $\mathbb{N}_0$


Note: I use $f$ for generic Peano system and $S$ for $\mathbb{N}_0$.
At this point I have the following Lemmas:
Lemma $(\mathbb{N}_0,\le)$ is a well-ordering.
Proof
Suppose that $X\subseteq\mathbb{N}_0$ and that $X$ does not have a minimum. Define $Y:=\{y\in\mathbb{N}_0:\neg \exists x(x\in X\land x<y)\}$, that is "there is no member of $X$ smaller than $y$". We show that $Y$ is inductive. (1) $0\in Y$, since no natural number is smaller than $0$. (2) Suppose $y\in Y$, then $\neg \exists x(x\in X\land x<y)$ ans thus, since $y<S(y)$, $\neg \exists x(x\in X\land x<S(y))$ or $S(y)\in Y$. Thus $Y$ is inductive and $Y=\mathbb{N}_0$, therefore $X=\varnothing$, the only subset of $\mathbb{N}_0$ without a minimum.
(Actually not really relevant for this Question) Lemma, Infinite Descent 
Given a statement $P(x)$ with $x\in\mathbb{N}_0$, then $P(x)\to \exists y(y<x\land P(y))$ implies $\forall x\neg P(x)$, or $X=\{x\in\mathbb{N}_0:P(x)\}=\varnothing$.
Proof
The consequence of the hypothesis is that $X$ has no minimum, and being $\mathbb{N}_0$ well-ordered it follows that $X=\varnothing$.
Lemma
There are no infinite descending membership chains. Or: There is no infinite $\in$-decreasing sequence in $\mathbb{N}_0$, that is, there is no sequence $\{x_n:n\in\mathbb{N}_0\}$ such that $x_{n+1}\in x_n$ for all $n\in\mathbb{N}_0$.
Proof
Otherwise the set $\{x_n:n\in\mathbb{N}_0\}$ would have no $\in$-minimal element (which is not the case since $\mathbb{N}_0$ is well-ordered).
 A: You need to distinguish carefully between what you're saying and proving. As stated, you're not quite precise about what you mean by either "there are no" and "infinite descending membership chain".
In regular ZF(C), what you can prove using the Axiom of Regularity is

  
*
  
*There is no function $f: \mathbb N \to X$ such that $\forall n\in\mathbb N: f(n+1)\in f(n)$, no matter which set you allow $X$ to be.
  

On the other hand, what you can prove without regularity is


  
*There is no function $f: \mathbb N \to \omega$ such that $\forall n\in\mathbb N: f(n+1)\in f(n)$.
  

Of these, (2) is a weaker claim because the class of possible things it says cannot exist is smaller. Therefore it should be unsurprising that it is easier to prove and doesn't need the specific axiom that tells you (1).
(It's like the difference between claiming "unicorns don't exist" and "there are no unicorns in my living room").

Independently of this, be aware that if you have a model of ZFC, it may well be that you, looking at the model from the outside, can find a sequence of elements such that each has the next as an element -- even though both of claims (1) and (2) above are true inside the model.
That will be because the sequence you can see from the outside is not represented as a function $f:\mathbb N\to V$ that is itself an element of the model. So formulas in the first-order language of set theory cannot even speak about whether or not it exists.
(And there must exist such models if ZFC is consistent at all, as a standard compactness argument shows. In fact, every model has an elementary extension that has a descending chain of naturals).
A: I don't see how you could possibly prove that there are no infinite descending membership chains just "because of well-ordering of $\aleph_0$."  In models of ZFC minus regularity plus (as Asaf Karagila pointed out in a comment) the negation of regularity, there are infinite descending membership chains, yet $\aleph_0$ is well-ordered. In order to prove "there are no infinite descending membership chains" you need to use (some version of) the axiom of regularity, not just the well-ordering of $\aleph_0$.
A: There is no inherent connection. The Peano axioms (the second order one) imply that the order on the natural numbers is a well order. It has nothing to do with the axiom of regularity, and it holds in situations where the axiom of regularity fails, just as well.
Similarly you can prove that an ordered field is densely ordered. Why does this not contradict the axiom of regularity? Well. Because these are two different things.
The axiom of regularity simply states that $\in$ is well founded, which is the non-linear generalization of well ordered.
You could argue that you are talking about the von Neumann ordinals with $\in$ as the order relation, on which case you also don't need regularity since the ordinals are well ordered by definition (or, you might want to prove that from some other definition, but again regularity at most simplifies the proof, it is not necessary). 
A: If you are working in ZFC without the axiom of regularity, you are working in a model that has all the "standard sets" -- i.e., a model of full ZFC -- plus possibly some other non-well-founded sets. These "standard sets" are just the cumulative hierarchy, and you can define it by a formula. In particular that means that you do not need the axiom of regularity to prove the existence of something like the natural numbers: they are present without it anyway, and you can construct them just the same. 
For natural numbers (and ordinals in general) you can prove that $\alpha \notin \alpha$ directly -- that doesn't require the axiom, although it does of course make it easier.
