Ordinal is Finite iff Natural Number

From ProofWiki
Jump to navigation Jump to search

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 iff $x$ is an element of the minimal infinite successor set.


Proof

$x$ is finite iff $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 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$


Sources