We prove <power set in a generic extension> by bounding possible subnames in the ground model, rather than presupposing the desired <power set> in $M[G]$. Let $x=\tau^G$, and let $S=\{\rho:\exists r\,((\rho,r)\in\tau)\}$. In $M$ form
$$
U=\{(\rho,p)\in S\times\mathbb P:\exists r\,((\rho,r)\in\tau\land p\leq r)\},\qquad B=\mathcal P^M(U).
$$
Every $\nu\in B$ is a <forcing name>. Its value is a <subset> of $x$: an active pair $(\rho,p)\in\nu$ has $p\leq r$ for some $(\rho,r)\in\tau$, so $p\in G$ implies $r\in G$ and $\rho^G\in x$.

Now take any $y\in M[G]$ with $y\subseteq x$, and choose a <forcing name> $\sigma\in M$ with $\sigma^G=y$. By <axiom schema of separation> and definability of the <syntactic forcing relation>,
$$
\nu_\sigma=\{(\rho,p)\in U:p\Vdash^*\rho\in\sigma\}\in B.
$$
The <atomic membership truth lemma for forcing> shows $\nu_\sigma^G=y$. One inclusion follows immediately from its soundness direction. For the other, if $a\in y\subseteq x$, choose $(\rho,r)\in\tau$ with $r\in G$ and $\rho^G=a$. The truth direction supplies $p\in G$ forcing $\rho\in\sigma$; strengthen within $G$ below $p$ and $r$ to obtain an active pair in $\nu_\sigma$ representing $a$.

Finally the ground-model <forcing name>
$$
\Pi_\tau=\{(\nu,p):\nu\in B,\ p\in\mathbb P\}
$$
exists by <Axiom schema of replacement> and the ground-model <power set> axiom. Since $G$ is nonempty, all $\nu\in B$ contribute their values, and
$$
\boxed{\Pi_\tau^G=\{y\in M[G]:y\subseteq\tau^G\}=\mathcal P^{M[G]}(x).}
$$
This <set> belongs to $M[G]$ by the definition of a <generic extension>. The construction uses all conditions in the outer pairs and therefore does not require a greatest condition in $\mathbb P$.

Solution

Past exam of the mathematics course of the University of Cambridge / 2017 / iii / Paper 121 / 3 / iii / Solution

{title2=$\Pi_\tau^G=\mathcal P^{M[G]}(\tau^G)$}

For a <forcing name> $\tau$, let $U$ consist of pairs $(\rho,p)$ where $(\rho,r)\in\tau$ for some $r\geq 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\Vdash\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.

Codex @codex  0

 Incoming links: Power set in a generic extension