Prikry forcing adds no bounded subsets of kappa

For each pair $(r,\xi )$ with $r{\le }^{\ast }p$ and $\xi <\gamma$, F1 makes the set of direct extensions of $r$ deciding ``$\check{\xi }\in \dot{x}$'' nonempty. By F4 choose one such extension for every pair. This fixed selector, rather than an unstated sequence of arbitrary choices, will drive the recursion.

Write $p=(s,A_0)$. By transfinite recursion on $\xi <\gamma$, keep the stem $s$: at a successor use the selector from step 1.1 to obtain $p_{\xi +1}{\le }^{\ast }{p}_{\xi }$ deciding ``$\check{\xi }\in \dot{x}$'', and at a nonzero limit $\delta <\gamma$ take upper part ${\bigcap }_{\xi <\delta }{A}_{\xi }$. The latter is in the measure because $\delta <\gamma <\kappa$. Hence every $p_{\xi }$ is a condition and the sequence is direct-extension decreasing.

Intersect all upper parts used in the recursion, including the original one, to obtain $B\in U$, and put $q=(s,B)$. This also covers $\gamma =0$, when the intersection has just the original factor. Define in the ground model $x=\{\xi <\gamma :p_{\xi +1}⊩\check{\xi }\in \dot{x}\}$. For every $\xi <\gamma$, $q\le p_{\xi +1}$, so $q$ forces the positive membership statement exactly when $\xi \in x$, and otherwise forces its negation.

Let $G$ be any generic filter containing $q$. Since $q\le p$, the hypothesis gives ${\dot{x}}_G\subseteq \gamma$; step 3.1 says for every $\xi <\gamma$ that $\xi \in {\dot{x}}_G$ exactly when $\xi \in x$. Extensionality yields ${\dot{x}}_G=x$. By the semantic equivalence in F3, $q⊩\dot{x}=\check{x}$. The case $\gamma =0$ says simply that every subset of zero is empty, and was already included in step 3.1. [F3, step 3.1] $\mathrm{\square }$