Non-Empty Bounded Subset of Natural Numbers has Greatest Element

Theorem

Let $\omega$ be the set of natural numbers defined as the von Neumann construction.

Then every non-empty bounded subset of $\omega$ has a greatest element.

Proof

From Von Neumann Construction of Natural Numbers is Minimally Inductive, $\omega$ is minimally inductive class under the successor mapping.

From Successor Mapping on Natural Numbers is Progressing, this successor mapping is a progressing mapping.

The result is a direct application of Non-Empty Bounded Subset of Minimally Inductive Class under Progressing Mapping has Greatest Element.

$\blacksquare$

Sources

• 2010: Raymond M. Smullyan and Melvin Fitting: Set Theory and the Continuum Problem (revised ed.) ... (previous) ... (next): Chapter $3$: The Natural Numbers: $\S 5$ Applications to natural numbers: Theorem $5.4$