Kerodon

$\Newextarrow{\xRightarrow}{5,5}{0x21D2}$ $\newcommand\empty{}$
$\Newextarrow{\xhookrightarrow}{10,10}{0x21AA}$

Proposition 4.7.1.14. Let $(S, \leq )$ and $(T, \leq )$ be linearly ordered sets, and let $f,f': S \hookrightarrow T$ be strictly increasing functions. Suppose that $S$ is well-ordered and that $f$ is an initial segment embedding. Then, for each $s \in S$, we have $f(s) \leq f'(s)$.

Proof. Set $S_0 = \{ s \in S: f'(s) < f(s) \} $. We wish to show that $S_0$ is empty. Assume otherwise. Since $S$ is well-ordered, there is a least element $s \in S_0$. Since $f$ is an initial segment embedding, the inequality $f'(s) < f(s)$ implies that we can write $f'(s) = f(t)$ for some $t < s$. Then $t \notin S_0$, so we must have $f(t) \leq f'(t)$. It follows that $f'(s) \leq f'(t)$, contradicting our assumption that the function $f'$ is strictly increasing. $\square$