Finite von Neumann ordinal (source code)

= Finite von Neumann ordinal
{c}
{title2=$n=\{0,\ldots,n-1\}$}

A finite von Neumann ordinal is obtained from $0=\varnothing$ by finitely many applications of the successor operation $S(x)=x\cup\{x\}$. Equivalently, it is an ordinal every nonempty subset of which has a greatest element. This characterization defines the individual natural numbers without quantifying over all inductive sets.