# Ordinal is Finite iff Natural Number

## Theorem

Let $x$ be an ordinal.

Then $x$ is a finite set if and only if $x$ is an element of the minimally inductive 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 minimally inductive set.

$\blacksquare$