Successor Mapping on Ordinals is Strictly Progressing

From ProofWiki
Jump to navigation Jump to search


Let $\On$ denote the class of all ordinals.

Let $s$ denote the successor mapping on $\On$:

$\forall \alpha \in \On: \map s \alpha := \alpha \cup \set \alpha$

where $\alpha$ is an ordinal.

Then $s$ is a strictly progressing mapping.


From Ordinal is Proper Subset of Successor:

$\alpha \subsetneqq \alpha^+$

where $\alpha^+$ is identified as $\map s \alpha$.

The result follows by definition of strictly progressing mapping.