 Power set in a generic extension

For a forcing name $\tau$, let $U$ consist of pairs $(\rho ,p)$ where $(\rho ,r)\in \tau$ for some $r\ge p$. Every ground-model subset $\nu$ of $U$ is a name whose value is contained in ${\tau }^G$. Every subset ${\sigma }^G\subseteq {\tau }^G$ has an equivalent such name: retain those $(\rho ,p)\in U$ with $p⊩\rho \in \sigma$. The atomic membership truth lemma for forcing proves equality of values. Collect all these names from the ground-model power set ${\mathcal{P}}^M(U)$ into a single outer name, pairing each with every condition. Its value is the full internal power set, without presupposing that power set in the extension.