[proofplan] Choose an $M$-name $\tau$ with $\tau_G = a$ and isolate the set $S$ of names that can appear as potential members of $\tau$. Every subset $x \subseteq a$ in $M[G]$ can be represented by a nice name whose first coordinates all lie in $S$, obtained by choosing in $M$ a family of maximal antichains that decide membership for each $\sigma \in S$. Since all such nice names are subsets of $S \times \mathbb P$, their ranks are uniformly bounded in $M$. We then form, inside $M$, a single name whose possible members are exactly the bounded-rank names forced to be subsets of $\tau$, and use the [Truth Lemma](/theorems/4291) and the soundness direction of the [Forcing Theorem](/theorems/4290) to show that its interpretation is precisely $\mathcal{P}(a)^{M[G]}$. [/proofplan]

[step:Choose a name for $a$ and bound the ranks of all relevant nice names]Since $a \in M[G]$, choose an $M$-name $\tau \in M$ such that $\tau_G = a$. Define the set of potential member names of $\tau$ by \begin{align*} S := \{\sigma \in M : \exists p \in \mathbb P \text{ such that } (\sigma,p) \in \tau\}. \end{align*} Because $\tau \in M$ is a set of ordered pairs and $M \models \mathrm{ZFC}$, the set $S$ belongs to $M$ by Separation and Replacement inside $M$. Let $\operatorname{rank}^M$ denote the rank function computed in $M$. Define \begin{align*} \beta := \operatorname{rank}^M(S \cup \mathbb P). \end{align*} Choose an ordinal $\alpha \in \operatorname{Ord}^M$ such that every subset of $S \times \mathbb P$ that belongs to $M$ is an element of $V_\alpha^M$. For example, with the Kuratowski ordered-pair convention, one may take $\alpha := \beta + 6$. Thus, if $\nu \in M$ and $\nu \subseteq S \times \mathbb P$, then $\nu \in V_\alpha^M$.[/step]

[guided]The point of this step is to find one fixed set in $M$ that contains every name we will later need. We begin with an $M$-name $\tau \in M$ satisfying $\tau_G = a$. Such a name exists by the definition of the generic extension $M[G]$. The only names that can ever appear as members of $a = \tau_G$ are the first coordinates of pairs in $\tau$. We therefore define \begin{align*} S := \{\sigma \in M : \exists p \in \mathbb P \text{ such that } (\sigma,p) \in \tau\}. \end{align*} This is a set in $M$: since $\tau$ is a set in $M$, the operation of taking first coordinates from the ordered pairs in $\tau$ is available in $M$ by the axioms of Separation and Replacement. We now need a uniform rank bound. Let $\operatorname{rank}^M$ be the rank function of $M$, and put \begin{align*} \beta := \operatorname{rank}^M(S \cup \mathbb P). \end{align*} Every element of $S$ and every condition in $\mathbb P$ has $M$-rank less than $\beta$. With the Kuratowski convention $(\sigma,p) = \{\{\sigma\},\{\sigma,p\}\}$, the ordered pair $(\sigma,p)$ has rank bounded by a fixed finite amount above the ranks of $\sigma$ and $p$. Hence every element of $S \times \mathbb P$ lies in some $V_{\beta+k}^M$ for a fixed finite $k$. Taking one more rank level contains all subsets of $S \times \mathbb P$ that belong to $M$. Thus there is an ordinal $\alpha \in \operatorname{Ord}^M$, for instance $\alpha := \beta + 6$, such that \begin{align*} \nu \subseteq S \times \mathbb P \text{ and } \nu \in M \quad \Longrightarrow \quad \nu \in V_\alpha^M. \end{align*} This bound is what later lets $M$ collect all relevant names into a single set.[/guided]

[step:Replace every subset of $a$ by a bounded nice name]Let $x \in M[G]$ satisfy $x \subseteq a$. Choose an $M$-name $\mu \in M$ with $\mu_G = x$. We write $p \Vdash \varphi(\theta_1,\dots,\theta_n)$ for the forcing relation over the poset $\mathbb P$ computed in $M$, where $p \in \mathbb P$ and $\theta_1, \dots, \theta_n$ are $\mathbb P$-names in $M$. For each $\sigma \in S$, define in $M$ the set \begin{align*} D_\sigma := \{p \in \mathbb P : p \Vdash \sigma \in \mu \text{ or } p \Vdash \sigma \notin \mu\}. \end{align*} The forcing relation for the formula $\sigma \in \mu$ is definable over $M$ by the definability part of the [Forcing Theorem](/theorems/4290), so $D_\sigma \in M$ by Separation in $M$. The set $D_\sigma$ is dense by the decision argument for forcing: for every $q \in \mathbb P$, either some extension $r \leq q$ forces $\sigma \in \mu$, or, by the definition of forcing negation, some extension $r \leq q$ forces $\sigma \notin \mu$. Since $M \models \mathrm{ZFC}$, [Zorn's lemma](/theorems/1226) in $M$ gives, for each $\sigma \in S$, a maximal antichain $A_\sigma \in M$ with $A_\sigma \subseteq D_\sigma$; the [axiom of choice](/page/Axiom%20of%20Choice) in $M$ then gives a function $\sigma \mapsto A_\sigma$ with domain $S$ selecting such antichains. Define \begin{align*} A_\sigma^+ := \{p \in A_\sigma : p \Vdash \sigma \in \mu\}. \end{align*} By definability of the forcing relation and Separation in $M$, each $A_\sigma^+$ belongs to $M$, and Replacement in $M$ collects the family $\langle A_\sigma^+ : \sigma \in S\rangle$ as a set in $M$. Now define the nice name \begin{align*} \nu := \{(\sigma,p) : \sigma \in S \text{ and } p \in A_\sigma^+\}. \end{align*} Then $\nu \in M$, $\nu \subseteq S \times \mathbb P$, and hence $\nu \in V_\alpha^M$. We claim that $\nu_G = \mu_G = x$. If $y \in \nu_G$, then $y = \sigma_G$ for some $\sigma \in S$ and some $p \in G \cap A_\sigma^+$. Since $p \Vdash \sigma \in \mu$ and $p \in G$, the soundness direction of the [Forcing Theorem](/theorems/4290) gives $\sigma_G \in \mu_G$, so $y \in x$. Conversely, let $y \in x = \mu_G$. Since $x \subseteq a = \tau_G$, we have $y \in \tau_G$. Hence there are $\sigma \in S$ and $r \in G$ such that $(\sigma,r) \in \tau$ and $y = \sigma_G$. Since $A_\sigma$ is a maximal antichain in $M$, define \begin{align*} E_\sigma := \{q \in \mathbb P : \exists b \in A_\sigma \text{ such that } q \leq b\}. \end{align*} The set $E_\sigma$ belongs to $M$ and is dense in $\mathbb P$: for any $q \in \mathbb P$, maximality of $A_\sigma$ gives $b \in A_\sigma$ compatible with $q$, and any common extension of $q$ and $b$ lies in $E_\sigma$. By $M$-genericity, choose $q \in G \cap E_\sigma$, and then choose $p \in A_\sigma$ with $q \leq p$. Since $G$ is upward closed, $p \in G \cap A_\sigma$. Because $p \in D_\sigma$, the condition $p$ decides whether $\sigma \in \mu$. If $p \Vdash \sigma \notin \mu$, then the soundness direction of the [Forcing Theorem](/theorems/4290) and $p \in G$ would give $\sigma_G \notin \mu_G$, contradicting $\sigma_G = y \in \mu_G$. Therefore $p \Vdash \sigma \in \mu$, so $p \in A_\sigma^+$, and consequently $\sigma_G = y \in \nu_G$. Thus $\nu_G = x$.[/step]

[guided]We want to replace the arbitrary name $\mu$ for $x$ by a name whose support is uniformly controlled by the set $S$ from the first step. The forcing order convention is that $q \leq p$ means $q$ is stronger than $p$, so if $q \in G$ and $q \leq p$, then $p \in G$ because a generic filter is upward closed toward weaker conditions. For each $\sigma \in S$, define \begin{align*} D_\sigma := \{p \in \mathbb P : p \Vdash \sigma \in \mu \text{ or } p \Vdash \sigma \notin \mu\}. \end{align*} The parameters $\sigma$ and $\mu$ are $\mathbb P$-names in $M$, so the definability part of the [Forcing Theorem](/theorems/4290) applies to the formula $\sigma \in \mu$. Hence $D_\sigma \in M$ by Separation in $M$. The decision argument for forcing gives density: for every $q \in \mathbb P$, either some stronger condition $r \leq q$ forces $\sigma \in \mu$, or, by the definition of forcing negation, some stronger condition $r \leq q$ forces $\sigma \notin \mu$. Inside $M$, Zorn's lemma applies to the poset of antichains contained in $D_\sigma$, ordered by inclusion, because $M \models \mathrm{ZFC}$. Thus for each $\sigma \in S$ there is a maximal antichain $A_\sigma \in M$ with $A_\sigma \subseteq D_\sigma$, and the axiom of choice in $M$ lets us select the family $\langle A_\sigma : \sigma \in S\rangle$. Define \begin{align*} A_\sigma^+ := \{p \in A_\sigma : p \Vdash \sigma \in \mu\}. \end{align*} Again, definability of the forcing relation and Separation in $M$ imply $A_\sigma^+ \in M$, and Replacement in $M$ collects the family indexed by $S$. Define the nice name \begin{align*} \nu := \{(\sigma,p) : \sigma \in S \text{ and } p \in A_\sigma^+\}. \end{align*} Then $\nu \in M$ and $\nu \subseteq S \times \mathbb P$, so the rank bound from the first step gives $\nu \in V_\alpha^M$. We now compare evaluations. If $y \in \nu_G$, then $y = \sigma_G$ for some $\sigma \in S$ and some $p \in G \cap A_\sigma^+$. Since $p \Vdash \sigma \in \mu$, the soundness direction of the [Forcing Theorem](/theorems/4290) gives $\sigma_G \in \mu_G$, so $y \in x$. Conversely, suppose $y \in x = \mu_G$. Since $x \subseteq a = \tau_G$, we also have $y \in \tau_G$. Therefore $y = \sigma_G$ for some $\sigma \in S$ and some $r \in G$ with $(\sigma,r) \in \tau$. The maximal antichain $A_\sigma$ must be met by $G$: indeed, the set of conditions extending some member of $A_\sigma$ is dense, and $G$ meets every [dense subset](/page/Dense%20Subset) of $\mathbb P$ that belongs to $M$. Choose $p \in G \cap A_\sigma$. Since $p \in D_\sigma$, it decides whether $\sigma \in \mu$. If $p \Vdash \sigma \notin \mu$, soundness would imply $\sigma_G \notin \mu_G$, contradicting $\sigma_G = y \in \mu_G$. Hence $p \Vdash \sigma \in \mu$, so $p \in A_\sigma^+$ and $y = \sigma_G \in \nu_G$. Thus $\nu_G = x$.[/guided]

[step:Form in $M$ the name for all forced subsets of $\tau$]Define the set of bounded names in $M$ by \begin{align*} N_\alpha := \{\nu \in V_\alpha^M : M \models ``\nu \text{ is a } \mathbb P\text{-name}''\}. \end{align*} The predicate "$\nu$ is a $\mathbb P$-name" is first-order over $M$ with parameter $\mathbb P$, so $N_\alpha \in M$ by Separation in $M$. Now define \begin{align*} \rho := \{(\nu,p) \in N_\alpha \times \mathbb P : p \Vdash \nu \subseteq \tau\}. \end{align*} For every $\nu \in N_\alpha$, the parameters $\nu$ and $\tau$ are $\mathbb P$-names in $M$, so the definability part of the [Forcing Theorem](/theorems/4290) applies to the forcing formula $p \Vdash \nu \subseteq \tau$. Since $N_\alpha \times \mathbb P \in M$, Separation in $M$ gives $\rho \in M$. Hence $\rho_G \in M[G]$. Here $\nu \subseteq \tau$ abbreviates the forcing-language assertion that every element of $\nu_G$ is an element of $\tau_G$.[/step]

[guided]The definition of $\rho$ must range only over genuine forcing names. Although $V_\alpha^M$ is a set in $M$, not every element of $V_\alpha^M$ is a $\mathbb P$-name, and the expression $p \Vdash \nu \subseteq \tau$ is part of the forcing relation only when $\nu$ and $\tau$ are names. We therefore first define \begin{align*} N_\alpha := \{\nu \in V_\alpha^M : M \models ``\nu \text{ is a } \mathbb P\text{-name}''\}. \end{align*} This is a set in $M$ because namehood is defined recursively by the first-order condition that every element of $\nu$ is an ordered pair whose first coordinate is again a $\mathbb P$-name and whose second coordinate lies in $\mathbb P$. Now we define \begin{align*} \rho := \{(\nu,p) \in N_\alpha \times \mathbb P : p \Vdash \nu \subseteq \tau\}. \end{align*} For each $\nu \in N_\alpha$, both $\nu$ and $\tau$ are $\mathbb P$-names in $M$. This verifies the parameter hypothesis needed for the definability part of the [Forcing Theorem](/theorems/4290). Hence the relation "$p \Vdash \nu \subseteq \tau$" is definable over $M$ on $N_\alpha \times \mathbb P$, and Separation in $M$ gives $\rho \in M$. Since every name in $M$ evaluates to an element of $M[G]$, we get $\rho_G \in M[G]$.[/guided]

[step:Show that $\rho_G$ is exactly the power set of $a$ in $M[G]$] First let $y \in \rho_G$. Then there are $\nu \in V_\alpha^M$ and $p \in G$ such that $(\nu,p) \in \rho$ and $y = \nu_G$. By the definition of $\rho$, we have $p \Vdash \nu \subseteq \tau$. Since $p \in G$, the soundness direction of the [Forcing Theorem](/theorems/4290) gives \begin{align*} M[G] \models \nu_G \subseteq \tau_G. \end{align*} Thus $y = \nu_G \subseteq \tau_G = a$, so $y \in \mathcal{P}(a)^{M[G]}$. Conversely, let $x \in \mathcal{P}(a)^{M[G]}$. By the previous nice-name construction, there is a name $\nu \in V_\alpha^M$ such that $\nu_G = x$. Since $x \subseteq a$, we have \begin{align*} M[G] \models \nu_G \subseteq \tau_G. \end{align*} By the [Truth Lemma](/theorems/4291), there is a condition $p \in G$ such that $p \Vdash \nu \subseteq \tau$. Therefore $(\nu,p) \in \rho$, and hence $x = \nu_G \in \rho_G$. We have proved both inclusions: \begin{align*} \rho_G \subseteq \mathcal{P}(a)^{M[G]}. \end{align*} and \begin{align*} \mathcal{P}(a)^{M[G]} \subseteq \rho_G. \end{align*} Therefore \begin{align*} \rho_G = \mathcal{P}(a)^{M[G]}. \end{align*} Since $\rho \in M$, its interpretation $\rho_G$ belongs to $M[G]$. Hence $\mathcal{P}(a)^{M[G]} \in M[G]$, as required.[/step]

[guided]We prove equality by two inclusions. First suppose $y \in \rho_G$. Then $y = \nu_G$ for some $\nu \in N_\alpha$ and some $p \in G$ with $(\nu,p) \in \rho$. By the definition of $\rho$, the condition $p$ forces $\nu \subseteq \tau$. Since $p \in G$, the soundness direction of the [Forcing Theorem](/theorems/4290) gives \begin{align*} M[G] \models \nu_G \subseteq \tau_G. \end{align*} Thus $y = \nu_G \subseteq \tau_G = a$, so $y \in \mathcal{P}(a)^{M[G]}$. Conversely, suppose $x \in \mathcal{P}(a)^{M[G]}$. The nice-name construction gives a $\mathbb P$-name $\nu \in V_\alpha^M$ such that $\nu_G = x$. Since $\nu$ is a name, $\nu \in N_\alpha$. The assumption $x \subseteq a$ says \begin{align*} M[G] \models \nu_G \subseteq \tau_G. \end{align*} By the [Truth Lemma](/theorems/4291), there is a condition $p \in G$ such that $p \Vdash \nu \subseteq \tau$. Therefore $(\nu,p) \in \rho$, and hence $x = \nu_G \in \rho_G$. The two inclusions give \begin{align*} \rho_G = \mathcal{P}(a)^{M[G]}. \end{align*} Since $\rho \in M$, its interpretation belongs to $M[G]$. Therefore $\mathcal{P}(a)^{M[G]} \in M[G]$.[/guided]