Bounded successor characterization of finite ordinals ($x\in \omega ⟺\mathrm{Ord}(x)\wedge {\mathrm{Succ}}_0(x)\wedge \forall y\in x{\mathrm{Succ}}_0(y)$)

A Von Neumann ordinal $x$ is finite exactly when $x$ and every member of $x$ are either zero or successor ordinals. Every finite ordinal has that property. Conversely, an infinite ordinal is either $\omega$, which is a nonzero limit, or is greater than $\omega$ and contains that nonzero limit ordinal. The test can be expressed by a bounded first-order formula: ordinality uses transitivity and membership comparability, and a nonempty ordinal is a successor exactly when it has a greatest member. This defines the class of natural numbers without quantifying over arbitrary infinite inductive sets.