Proposition 4.7.1.22. Let $(S, \leq )$ be a well-ordered set, and let $\alpha $ denote its order type. Then there is a unique order-preserving bijection $S \rightarrow \mathrm{Ord}_{< \alpha }$, which carries each element $s \in S$ to the order type of the well-ordered set $S_{< s} = \{ s' \in S: s' < s \} $.
$\Newextarrow{\xhookrightarrow}{10,10}{0x21AA}$
Proof. We will prove existence; uniqueness then follows from Corollary 4.7.1.16. For each $s \in S$, let $\alpha _{s}$ denote the order type of the set $S_{< s}$ (which is well-ordered, by virtue of Remark 4.7.1.5). Note that, since there is an initial segment embedding $S_{< s} \hookrightarrow S$ which is not bijective, we must have $\alpha _{s} < \alpha $ (Remark 4.7.1.18). Consequently, the construction $s \mapsto \alpha _{s}$ determines a function $S \rightarrow \mathrm{Ord}_{< \alpha }$. If $s < t$ in $S$, then there is an initial segment embedding from $S_{< s}$ to $S_{< t}$ which is not bijective, so that $\alpha _{s} < \alpha _{t}$ (again by Remark 4.7.1.18). To complete the proof, it will suffice to show that the function $s \mapsto \alpha _{s}$ is surjective. Let $\beta $ be an ordinal which is strictly smaller than $\alpha $. Then $\beta $ is the order type of some initial segment $S_0 \subsetneq S$. Since $S$ is well-ordered, the set $S \setminus S_0$ has a smallest element $s$. It follows that $S_0 = S_{< s}$, so that $\beta = \alpha _{s}$. $\square$