[proofplan]
We argue by contradiction: if forcing with $P$ collapsed $\omega_1^V$, then some condition would force the existence of a countable cofinal map from $\omega$ into $\omega_1^V$. We place the relevant objects inside a countable elementary submodel $M \prec H_\theta$ and use properness to strengthen the condition to an $(M,P)$-generic master condition. The master condition ensures that every possible value of the name is already decided by a condition in $M$, hence lies below $\delta = M \cap \omega_1$. This bounds the range of the alleged cofinal map below $\omega_1^V$, giving the contradiction.
[/proofplan]
[step:Assume a condition forces a countable cofinal map into $\omega_1^V$]
Suppose, toward a contradiction, that $P$ does not preserve $\omega_1^V$. Then there are a condition $p \in P$ and a $P$-name $\dot{f}$ such that
\begin{align*}
p \Vdash \dot{f}: \omega \to \check{\omega}_1^V \text{ is cofinal}.
\end{align*}
Here the order on $P$ is written so that $q \leq p$ means that $q$ is stronger than $p$.
[/step]
[step:Choose a countable elementary submodel and an $(M,P)$-generic strengthening]
Let $H_\theta$ denote the set of all sets whose transitive closures have cardinality less than the regular cardinal $\theta$. Choose $\theta$ large enough that $P$, $p$, $\dot{f}$, $\omega_1$, and the relevant forcing relation for $P$ restricted to names in $H_\theta$ belong to, or are definable over, $H_\theta$. Choose a countable elementary submodel
\begin{align*}
M \prec H_\theta
\end{align*}
such that $P,p,\dot{f} \in M$. Define
\begin{align*}
\delta := M \cap \omega_1.
\end{align*}
Since $M$ is countable in $V$, $\delta$ is a countable ordinal, hence $\delta < \omega_1^V$.
By the definition of properness, since $P$ is proper and $p \in P \cap M$, there exists a condition $q \leq p$ such that $q$ is $(M,P)$-generic. We use the standard dense-set form of $(M,P)$-genericity: for every dense set $D \subset P$ with $D \in M$, the set $D \cap M$ is predense below $q$. Equivalently, whenever $s \leq q$, there is some $r \in D \cap M$ compatible with $s$.
[/step]
[step:Build dense sets that either avoid $p$ or decide each value of the name]
For each $n \in \omega$, define the deciding set below $p$ by
\begin{align*}
D_n := \{r \in P : \text{there exists } \alpha < \omega_1^V \text{ such that } r \Vdash \dot{f}(\check{n}) = \check{\alpha}\}.
\end{align*}
Define the full dense set
\begin{align*}
E_n := \{r \in P : r \text{ is incompatible with } p\} \cup D_n.
\end{align*}
The set $E_n$ is dense in $P$. Indeed, let $a \in P$. If $a$ is incompatible with $p$, then $a \in E_n$. If $a$ is compatible with $p$, choose a common extension $c \leq a,p$. Since $c \leq p$ and
\begin{align*}
p \Vdash \dot{f}: \omega \to \check{\omega}_1^V,
\end{align*}
the condition $c$ forces that $\dot{f}(\check{n})$ is an ordinal below $\check{\omega}_1^V$. By the [forcing theorem](/theorems/6531), in its decision form for ordinal-valued names, there are a condition $b \leq c$ and an ordinal $\alpha < \omega_1^V$ such that
\begin{align*}
b \Vdash \dot{f}(\check{n}) = \check{\alpha}.
\end{align*}
Then $b \leq a$ and $b \in D_n \subset E_n$.
Also $E_n \in M$, because the definition of $E_n$ is first-order over $H_\theta$ from the parameters $P$, $p$, $\dot{f}$, $n$, $\omega_1$, and the forcing relation for $P$ on the relevant names. These parameters and definable predicates are available in $H_\theta$ by the choice of $\theta$, and $P$, $p$, $\dot{f}$, and $n$ belong to $M$.
[/step]
[step:Show every value forced below the master condition lies below $\delta$]
Fix $n \in \omega$. We prove that
\begin{align*}
q \Vdash \dot{f}(\check{n}) < \check{\delta}.
\end{align*}
Let $s \leq q$ be arbitrary. Since $s \leq q \leq p$, the condition $s$ is compatible with $p$. By density of $E_n$, choose $t \leq s$ with $t \in E_n$. Since $t \leq s \leq p$, the condition $t$ is compatible with $p$, so $t$ is not in the incompatible-with-$p$ part of $E_n$. Hence $t \in D_n$, and there is an ordinal $\alpha < \omega_1^V$ such that
\begin{align*}
t \Vdash \dot{f}(\check{n}) = \check{\alpha}.
\end{align*}
Since $q$ is $(M,P)$-generic and $E_n \in M$ is dense, there exists $r \in E_n \cap M$ compatible with $t$.
The compatibility of $r$ with $t \leq p$ implies that $r$ is compatible with $p$. Therefore $r$ is not in the incompatible-with-$p$ part of $E_n$, so $r \in D_n \cap M$. The assertion “there exists $\beta < \omega_1$ such that $r \Vdash \dot{f}(\check{n}) = \check{\beta}$” is witnessed in $H_\theta$, and elementarity gives some $\beta \in M \cap \omega_1$ such that
\begin{align*}
r \Vdash \dot{f}(\check{n}) = \check{\beta}.
\end{align*}
Thus $\beta < \delta$.
Choose a common extension $u \leq t,r$. Then $u$ forces both
\begin{align*}
\dot{f}(\check{n}) = \check{\alpha}
\end{align*}
and
\begin{align*}
\dot{f}(\check{n}) = \check{\beta}.
\end{align*}
Forcing preserves equality of check names for ground-model ordinals, so $\alpha=\beta$. Therefore $\alpha < \delta$. By the density characterization of forcing, since every $s \leq q$ has a stronger condition $t \leq s$ forcing $\dot{f}(\check{n}) < \check{\delta}$, we have
\begin{align*}
q \Vdash \dot{f}(\check{n}) < \check{\delta}.
\end{align*}
[guided]
Fix a natural number $n \in \omega$. The goal is to prove that below the master condition $q$, the $n$th value of $\dot{f}$ cannot reach $\delta = M \cap \omega_1$.
Start with an arbitrary condition $s \leq q$. We cannot use the set $D_n$ as a [dense subset](/page/Dense%20Subset) of all of $P$, because the original condition $p$ only controls extensions below $p$. Instead we use the dense set $E_n$, whose conditions either are incompatible with $p$ or decide the value of $\dot{f}(\check{n})$. Since $s \leq q \leq p$, the condition $s$ is compatible with $p$. Density of $E_n$ gives a strengthening $t \leq s$ with $t \in E_n$. Because $t \leq s \leq p$, the condition $t$ is compatible with $p$, so $t$ cannot belong to the incompatible-with-$p$ part of $E_n$. Therefore $t \in D_n$, and by the definition of $D_n$ there is an ordinal $\alpha < \omega_1^V$ such that
\begin{align*}
t \Vdash \dot{f}(\check{n}) = \check{\alpha}.
\end{align*}
Now we use properness through the master condition. Since $E_n \in M$ is dense in $P$ and $q$ is $(M,P)$-generic, the set $E_n \cap M$ is predense below $q$. Because $t \leq q$, there is a condition $r \in E_n \cap M$ compatible with $t$.
The compatibility with $t$ forces $r$ to be a deciding condition rather than an incompatible condition. Indeed, $t \leq p$, so any common extension of $r$ and $t$ is also a common extension of $r$ and $p$. Thus $r$ is compatible with $p$, and hence $r$ is not in the incompatible-with-$p$ part of $E_n$. Therefore $r \in D_n \cap M$. Since $r \in D_n$, in $H_\theta$ there exists an ordinal $\beta < \omega_1$ such that
\begin{align*}
r \Vdash \dot{f}(\check{n}) = \check{\beta}.
\end{align*}
The parameters $r$, $P$, $\dot{f}$, and $n$ all belong to $M$, so elementarity of $M \prec H_\theta$ gives such a witness $\beta$ inside $M$. Therefore $\beta \in M \cap \omega_1 = \delta$, so $\beta < \delta$.
Because $r$ and $t$ are compatible, choose a common extension $u \leq r,t$. Then $u$ extends $t$, so
\begin{align*}
u \Vdash \dot{f}(\check{n}) = \check{\alpha}.
\end{align*}
Also $u$ extends $r$, so
\begin{align*}
u \Vdash \dot{f}(\check{n}) = \check{\beta}.
\end{align*}
A condition cannot force the same name for an ordinal to be two distinct ground-model ordinals. Hence $\alpha=\beta$, and therefore $\alpha < \delta$.
We have shown that every condition $s \leq q$ has a stronger condition forcing $\dot{f}(\check{n}) < \check{\delta}$. By the density characterization of forcing, this is exactly the forcing assertion
\begin{align*}
q \Vdash \dot{f}(\check{n}) < \check{\delta}.
\end{align*}
[/guided]
[/step]
[step:Contradict cofinality of the forced map]
Since the preceding step holds for every $n \in \omega$, the condition $q$ forces
\begin{align*}
\operatorname{Range}(\dot{f}) \subset \check{\delta}.
\end{align*}
Because $\delta < \omega_1^V$, this implies
\begin{align*}
q \Vdash \dot{f} \text{ is not cofinal in } \check{\omega}_1^V.
\end{align*}
But $q \leq p$, and $p$ was assumed to force that $\dot{f}: \omega \to \check{\omega}_1^V$ is cofinal. This contradiction shows that no such $p$ and $\dot{f}$ exist. Therefore forcing with $P$ preserves $\omega_1^V$, equivalently
\begin{align*}
P \Vdash \check{\omega}_1^V = \omega_1.
\end{align*}
[/step]