Corollary 4.7.1.24. Let $S$ be any nonempty collection of ordinals. Then $S$ has a least element.
$\Newextarrow{\xhookrightarrow}{10,10}{0x21AA}$
Proof. Choose an ordinal $\alpha \in S$. If $\alpha $ is a least element of $S$, then we are done. Otherwise, we can replace $S$ by the nonempty subset $S_{< \alpha } = \{ \beta \in S: \beta < \alpha \} $. Note that $S_{< \alpha }$ is a nonempty subset of $\mathrm{Ord}_{< \alpha }$, and therefore has a smallest element by virtue of Corollary 4.7.1.23. $\square$