Proposition 4.7.1.33. Let $(T, \leq )$ be a linearly ordered set. Then the cofinality $\mathrm{cf}(T)$ is the smallest ordinal $\alpha $ with the following property:
There exists a well-ordered set $(S, \leq )$ of order type $\alpha $ and a function $f: S \rightarrow T$ which is unbounded (that is, every element $t \in T$ satisfies $t \leq f(s)$ for some $s \in S$). Here we do not require $f$ to be nondecreasing.
Proof. It is clear that the cofinality $\mathrm{cf}(T)$ satisfies condition $(\ast )$. For the converse, assume that $(S, \leq )$ is a well-ordered set of order type $\alpha $ and that $f: S \rightarrow T$ is an unbounded function. Let us say that an element $s \in S$ is good if, for every element $s' < s$ of $S$, we have $f(s') < f(s)$. Let $S_0$ be the collection of good elements of $S$, and set $f_0 = f|_{ S_0 }$. By construction, the function $f_0$ is strictly increasing. Moreover, the order type of $S_0$ is $\leq \alpha $ (Remark 4.7.1.21). To complete the proof, it will suffice to show that $f_0: S_0 \hookrightarrow T$ is cofinal. Fix an element $t \in T$, and set $S_{\geq t} = \{ s \in S: t \leq f(s) \} $. We wish to show that the intersection $S_{\geq t} \cap S_0$ is nonempty. We first observe that $S_{\geq t}$ is nonempty (by virtue of our assumption that $f$ is unbounded). Since $(S, \leq )$ is well-ordered, the set $S_{\geq t}$ contains a least element $s$. We claim that $s$ belongs to $S_0$. Assume otherwise: then there exists some $s' < s$ satisfying $f(s') \geq f(s)$. It follows that $s'$ belongs to $S_{\geq t}$, contradicting the minimality of $s$. $\square$