[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*}[/step]

[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: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]