[proofplan]
For each natural number $n$, we choose a maximal antichain below $p$ whose elements decide the ordinal value of $\dot f(n)$. The countable chain condition makes each such antichain countable, and hence the set of all ordinals decided by all these antichains is a countable ground-model subset of $\alpha$. Maximality then ensures that every condition below $p$ is compatible with a condition deciding $\dot f(n)$ to lie in this set, so $p$ forces every value of $\dot f$ to lie in the same [countable set](/page/Countable%20Set).
[/proofplan]
[step:Choose countable maximal antichains deciding each coordinate]
For each $n \in \omega$, define the cone below $p$ by
\begin{align*}
\mathbb{P}_{\leq p} := \{r \in \mathbb{P} : r \leq p\}.
\end{align*}
Since $p \Vdash_{\mathbb{P}} \dot f: \omega \to \alpha$, every condition $r \leq p$ forces $\dot f(n)$ to be an element of $\alpha$. By the definition of forcing for ordinal-valued names, for every $r \leq p$ there is a condition $s \leq r$ and an ordinal $\beta \in \alpha$ such that
\begin{align*}
s \Vdash_{\mathbb{P}} \dot f(n) = \beta.
\end{align*}
Thus the set of conditions below $p$ that decide $\dot f(n)$ is dense in $\mathbb{P}_{\leq p}$. Choose a maximal antichain $B_n \subset \mathbb{P}_{\leq p}$ consisting only of conditions that decide $\dot f(n)$. Since $B_n$ is an antichain in $\mathbb{P}$ and $\mathbb{P}$ satisfies the countable chain condition, $B_n$ is countable.
For each $b \in B_n$, let $\beta_{n,b} \in \alpha$ be the unique ordinal satisfying
\begin{align*}
b \Vdash_{\mathbb{P}} \dot f(n) = \beta_{n,b}.
\end{align*}
Uniqueness follows because no condition can force two distinct ordinal values for the same name.
[guided]
Fix $n \in \omega$. We want to control the possible values of the single name $\dot f(n)$. Since $p$ forces $\dot f$ to be a function from $\omega$ into $\alpha$, every stronger condition $r \leq p$ forces that $\dot f(n)$ is an ordinal below $\alpha$.
The forcing relation for ordinal-valued names has the following decision property: below any condition forcing membership in an ordinal, there is a stronger condition deciding the exact ordinal value. Therefore, for every $r \leq p$, we can find $s \leq r$ and some $\beta \in \alpha$ such that
\begin{align*}
s \Vdash_{\mathbb{P}} \dot f(n) = \beta.
\end{align*}
This means that the deciding conditions are dense in the cone
\begin{align*}
\mathbb{P}_{\leq p} := \{r \in \mathbb{P} : r \leq p\}.
\end{align*}
Inside this dense set, choose a maximal antichain $B_n$. Every element of $B_n$ lies below $p$ and decides $\dot f(n)$.
Now the countable chain condition enters. An antichain in the cone below $p$ is still an antichain in the whole poset $\mathbb{P}$, because incompatibility is computed in $\mathbb{P}$. Since $\mathbb{P}$ is ccc, every antichain in $\mathbb{P}$ is countable. Hence $B_n$ is countable.
Finally, for each $b \in B_n$, define $\beta_{n,b}$ to be the ordinal decided by $b$:
\begin{align*}
b \Vdash_{\mathbb{P}} \dot f(n) = \beta_{n,b}.
\end{align*}
This ordinal lies in $\alpha$ because $b \leq p$ and $p$ forces $\dot f(n) \in \alpha$.
[/guided]
[/step]
[step:Collect all ordinal values decided by the antichains]
Define
\begin{align*}
A := \{\beta_{n,b} : n \in \omega \text{ and } b \in B_n\}.
\end{align*}
For each $n \in \omega$, the set $B_n$ is countable, and $\omega$ is countable. Hence $A$ is a [countable union of countable sets](/theorems/755), so $A$ is countable. Since each $\beta_{n,b}$ belongs to $\alpha$, we have $A \subset \alpha$. The construction used only ground-model objects, so $A$ belongs to the ground model.
[/step]
[step:Show that $p$ forces every coordinate of $\dot f$ into $A$]
Fix $n \in \omega$. We prove
\begin{align*}
p \Vdash_{\mathbb{P}} \dot f(n) \in A.
\end{align*}
Let $r \leq p$ be arbitrary. Since $B_n$ is maximal as an antichain below $p$, there exists $b \in B_n$ compatible with $r$. Choose a common strengthening $t \in \mathbb{P}$ with
\begin{align*}
t \leq r
\end{align*}
and
\begin{align*}
t \leq b.
\end{align*}
Because $b \Vdash_{\mathbb{P}} \dot f(n) = \beta_{n,b}$ and forcing is downward persistent, we have
\begin{align*}
t \Vdash_{\mathbb{P}} \dot f(n) = \beta_{n,b}.
\end{align*}
Since $\beta_{n,b} \in A$, this gives
\begin{align*}
t \Vdash_{\mathbb{P}} \dot f(n) \in A.
\end{align*}
Thus below every $r \leq p$ there is a stronger condition forcing $\dot f(n) \in A$. Therefore $p \Vdash_{\mathbb{P}} \dot f(n) \in A$.
Since $n \in \omega$ was arbitrary, $p$ forces that every value of $\dot f$ lies in $A$:
\begin{align*}
p \Vdash_{\mathbb{P}} \operatorname{Range}(\dot f) \subset A.
\end{align*}
Taking $q := p$ gives $q \leq p$ and the required conclusion.
[/step]
