The Prikry generic sequence changes cofinality to omega

Any two conditions in $G$ have a common stronger condition because $G$ is a filter. Their stems are therefore both initial segments of the common stem and hence are comparable by end-extension. Thus $g=\bigcup \{s_p:p\in G\}$ is a function whose domain is an initial segment of $\omega$, and F1 makes it strictly increasing.

For each $n<\omega$, let $D_n$ consist of conditions whose stems have length at least $n$. It is dense: from $(s,A)$ add finitely many increasing points from the nonempty successive measure-one tails of $A$. The definition of $D_n$ and this density proof are in $M$. By F3, $G$ meets $D_n$ for every ground-model natural number $n$; transitivity makes these all actual natural numbers. Hence $\mathrm{dom}(g)=\omega$.

A measure-one set is unbounded in $\kappa$. Otherwise it would be contained in some $\alpha <\kappa$, while $\kappa \setminus \alpha$ belongs to $U$ because it is the intersection of fewer than $\kappa$ complements of singleton sets; this contradicts properness. For each $\alpha <\kappa$, the set $E_{\alpha }$ of conditions with a nonempty stem whose last entry exceeds $\alpha$ is consequently dense: extend once using a point of the upper part above $\alpha$. Since $E_{\alpha }\in M$, F3 gives $p\in G\cap E_{\alpha }$, and an entry of $g$ exceeds $\alpha$. Thus $g$ is cofinal in $\kappa$.

The canonical name for the union of generic stems evaluates to $g$, and the truth lemma places the preceding statements in $M[G]$. By F5, $g:\omega \to \kappa$ cofinal gives $\mathrm{cf}(\kappa )\le \omega$. No finite sequence is cofinal in the infinite limit ordinal $\kappa$, since its finite range has a maximum below $\kappa$; therefore $\mathrm{cf}(\kappa )$ is not finite and equals $\omega$. [F4, F5, step 2.1, step 2.2] $\mathrm{\square }$