No Infinitely Descending Membership Chains

Theorem

Let $\omega$ denote the minimal infinite successor set.

Let $F$ be a function whose domain is $\omega$.

Then:

$\exists n \in \omega: F \left({n^+}\right) \notin F \left({n}\right)$

Corollary

There cannot exist a sequence $\left\langle{x_n}\right\rangle$ whose domain is $\N_{\gt 0}$ such that:

$\forall n \in \N_{\gt 0}: x_{n+1} \in x_n$

Proof

Let $F$ be a function whose domain is $\omega$.

By the axiom of replacement, the range of $F$ is a set.

Let the range of $F$ be denoted $\mathcal W \left({F}\right)$.

Then:

 $\displaystyle$  $\displaystyle \exists x \in \mathcal W \left({F}\right): \left({\mathcal W \left({F}\right) \cap x}\right) = \varnothing$ Axiom of Foundation $\displaystyle$ $\implies$ $\displaystyle \exists x: \left({\left({\mathcal W \left({F}\right) \cap x}\right) = \varnothing \land \exists n \in \omega: x = F \left({n}\right)}\right)$ as $x \in \mathcal W \left({F}\right)$, $x = F \left({n}\right)$ for some $n \in \omega$ $\displaystyle$ $\implies$ $\displaystyle \exists n \in \omega: \left({\mathcal W \left({F}\right) \cap F \left({n}\right)}\right) = \varnothing$ Logical manipulation eliminating $x$

But:

$F \left({n^+}\right) \in \mathcal W \left({F}\right)$

So:

$F \left({n^+}\right) \not \in F \left({n}\right)$

$\blacksquare$