No Infinitely Descending Membership Chains

From ProofWiki
Jump to navigation Jump to search

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$


Sources