= Power set in a generic extension
{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.
Back to article page
