Prikry sequence is countable

Question

I am reading the chapter on Prikry forcing of Handbook of Set Theory. On page 1353:

1.4 Lemma Let $G\subseteq \mathcal P$ be generic for $\langle \mathcal P, \le \rangle$. Then $\bigcup\{p\mid \exists(\langle p, A\rangle \in G)\}$ is an $\omega$-sequence cofinal in $\kappa$.

The proof below perfectly explains why $G$ is cofinal: Let $$D_\alpha=\{\langle p, A\rangle\in \mathcal P \mid \langle p, A\rangle > \langle q, B\rangle\text{ and } \max(p)>\alpha\}\text.$$ Then $D_\alpha$ is dense, so $G\cap D_\alpha\ne\varnothing$ implies $G$ contains $\langle p, A\rangle$ where $\max(p)$ is very large.

However, that $G$ is countable doesn't look particularly clear to me.

Answer 1

Lemma. Suppose that $(p,A)$ and $(q,B)$ are compatible conditions, then $p$ is an initial segment of $q$ or vice versa.

Proof. Let $(r,C)$ be a common extension. Then $r$ is an end-extension of both $q$ and $p$. Therefore the conclusion must hold. $\square$

Corollary. If $G$ is a $V$-generic filter, then $\{p\mid\exists A,(p,A)\in G\}$ is a chain of subsets.

Proof. Think. $\square$

Corollary. If $s$ is a Prikry sequence, then $s$ is of order type $\omega$.

Proof. As $s$ is the union of a chain of finite sets. Since clearly $s$ is not finite, it must have order type $\omega$. $\square$