The Lévy collapse localizes countable ordinal data

By F2 every $\alpha <\kappa$ is countable after forcing, whereas the $\kappa$-chain condition preserves $\kappa$ and its uncountability. Hence $\kappa ={\omega }_1^{V[G]}$.

First justify the ordinal decisions. Fix a name $\dot{\gamma }$ forced to be an ordinal and let $\rho$ exceed its name rank. By the rank bound and ordinal preservation in F3, every possible value is some ground ordinal below $\rho$. In the Boolean completion, the join of the set of truth values $\parallel \dot{\gamma }=\check{\alpha }\parallel$ for $\alpha <\rho$ is $1$: otherwise a nonzero remainder would force that $\dot{\gamma }$ is an ordinal below $\rho$ unequal to every such $\alpha$, contradicting the forcing clauses and density closure. A maximal antichain refining these truth values therefore decides $\dot{\gamma }$ as a check ordinal. This proves the needed ordinal-name decision lemma; binary decision density alone was not substituted for it.

Apply step 1.2 to $\dot{f}(n)$ for each $n$. Ambient AC selects a sequence $(A_n{)}_{n<\omega }$ of deciding maximal antichains. The $\kappa$-cc makes every $A_n$ have size below $\kappa$. Each condition has finite support, so regularity in F4 bounds ${\bigcup }_{n<\omega }{\bigcup }_{p\in A_n}\mathrm{supp}(p)$ below some $\xi <\kappa$. Every $A_n\subseteq P_{\xi }$, and replacing each coefficient by its restriction gives a $P_{\xi }$-name whose $G_{\xi }$-value is ${\dot{f}}_G$. A real is the special case of an ordinal-valued omega-sequence.

In $V$, the collection of nice $P_{\xi }$-names for reals has cardinal below $\kappa$: each is coded by countably many antichains in the set $P_{\xi }$, and inaccessibility supplies the required bound. The tail collapse makes that ground set countable. Evaluating an ambient enumeration of its codes gives a surjection from $\omega$ onto ${\mathbb{R}}^{V[G_{\xi }]}$ in $V[G]$. Empty names and the zero real are included; no uniform choice is made inside an inner model.