Assuming countable choice: every at most countable subset of $\omega_1$ is bounded below $\omega_1$, so no at most countable subset of $\omega_1$ is cofinal in it, and a supremum of at most countably many at most countable ordinals is at most countable

Assume the Axiom of Countable Choice $\mathrm{AC}_\omega$ (The Axiom of Countable Choice ($\mathrm{AC}_\omega$)). Let $\omega_1$ be the first uncountable ordinal (The first uncountable ordinal $\omega_1 := \aleph(\omega)$). Then:

(a) Boundedness. Every at most countable (Finite, countably infinite, countable, uncountable) subset $A \subseteq \omega_1$ is bounded below $\omega_1$: the ordinal $\sup A = \bigcup A$ lies in $\omega_1$ and satisfies $\alpha \le \sup A$ for every $\alpha \in A$.

(b) No small cofinal set. No at most countable subset of $\omega_1$ is cofinal in $\omega_1$ (Cofinal subset of an ordinal).

(c) Suprema stay countable. If $A$ is an at most countable set of at most countable ordinals, then $\sup A = \bigcup A$ is an at most countable ordinal.

The hypothesis is not decoration. $\mathrm{AC}_\omega$ is spent at exactly one step, step 1.2 below, and it is spent there only through Countable unions of at most countable sets, assuming $\mathrm{AC}_\omega$, whose own statement carries the same hypothesis. Everything else on this page, including the existence of $\omega_1$ and all of $\omega_1$ is uncountable, every ordinal below it is at most countable, it is a cardinal and a limit ordinal, and its existence is a theorem of ZF, is a theorem of ZF. The ledger is the choice-ledger remark at the end of this page.

Where exactly the choice is spent, and why it cannot be avoided here. Step 1.2 hands an $\mathbb{N}$-indexed family of at most countable sets to Countable unions of at most countable sets, assuming $\mathrm{AC}_\omega$, and that theorem selects one enumeration of each member at once. Each ordinal $\alpha < \omega_1$ has enumerations by $\mathbb{N}$, in general many, and countability alone gives no rule for singling one out. Note that the family $(A_n)$ itself is produced without choice: it is $n \mapsto s(n)$ for a surjection $s$ that A nonempty set is at most countable iff it is a surjective image of $\mathbb{N}$ hands over, and that lemma is choice free.

The hypothesis is genuinely needed, not merely convenient. Without a choice principle the conclusion can fail outright: it is consistent with ZF, granted the consistency of ZF, that $\omega_1$ is the supremum of an $\omega$-sequence of at most countable ordinals. That is the Feferman-Levy model, recorded in Choice ledger for this page: $\omega_1$ exists in ZF, and the boundedness theorem does not with the external citation. So the boundedness proved here is not a fact about $\omega_1$ alone; it is a fact about $\omega_1$ plus $\mathrm{AC}_\omega$.

What the statement deliberately avoids at this point in the reading order. The usual formulation is "$\omega_1$ is a regular cardinal", using the cofinality function $\operatorname{cf}$. That vocabulary is introduced later in Cofinality $\operatorname{cf}(\alpha)$, and regular and singular cardinals ↗, so the present theorem states the conclusion in the subset form available here: no at most countable subset is cofinal. That is exactly the form the applications need, for instance the non-normality of the deleted Tychonoff plank, where the countably many ordinals produced by a covering argument must be capped below $\omega_1$.

Claim (c) restated. A supremum of at most countably many at most countable ordinals is at most countable. This is the same fact viewed without reference to $\omega_1$, and it is the form used when the ambient ordinal is not $\omega_1$ but some countable limit; see the worked increasing-sequence example on the companion examples page.