# Ordinal is Finite iff Natural Number

 This article is not under active maintenance. While the contents of this page could be useful, they are currently not being maintained. The correctness, lay-out and usefulness of the article may be compromised, so use whatever you get from here with caution.

## Theorem

Let $x$ be an ordinal.

Then $x$ is a finite set if and only if $x$ is an element of the minimal infinite successor set.

## Proof

$x$ is finite if and only if $x \sim \N_n$ for some $n \in \N$, by definition.

But $x$ is an ordinal, and by definition, it is equal to its initial segment.

By definition of the von Neumann construction of natural numbers, it follows that $x \sim n$ for some $n$.

By Finite Ordinal is equal to Natural Number, it follows that $x$ is equal to $n$.

Thus, $x$ is an element of the minimal infinite successor set.

$\blacksquare$