[proofplan] Choose $\mathbb{P}$-names $\tau,\zeta \in M$ for $a$ and $z$. Inside $M$, use the definability of the forcing relation to build a name $\rho$ whose possible elements are exactly those names appearing in $\tau$ and whose tags force the desired formula. The verification has two inclusions: membership in $\rho_G$ implies membership in the separated subset by the [forcing theorem](/theorems/6531), and membership in the separated subset gives a forcing condition in the generic filter by the truth lemma and directedness of $G$. [/proofplan]

[step:Choose names for the set and the parameter] Since $a,z \in M[G]$, by the definition of the forcing extension there exist $\mathbb{P}$-names $\tau,\zeta \in M$ such that \begin{align*} \tau_G = a \end{align*} and \begin{align*} \zeta_G = z. \end{align*} We use the standard valuation of a name by a generic filter: \begin{align*} \theta_G = \{\sigma_G : \text{there exists } p \in G \text{ such that } (\sigma,p) \in \theta\} \end{align*} for every $\mathbb{P}$-name $\theta \in M$. We also fix the forcing notation used below. For a condition $p \in \mathbb{P}$, a formula $\psi(v_1,\dots,v_n)$ of set theory, and $\mathbb{P}$-names $\theta_1,\dots,\theta_n \in M$, the expression \begin{align*} p \Vdash_{\mathbb{P}} \psi(\theta_1,\dots,\theta_n) \end{align*} means that $p$ forces the formula $\psi$ with the displayed names as parameters. Equivalently, for every $M$-generic filter $H \subseteq \mathbb{P}$ with $p \in H$, the forcing theorem gives \begin{align*} M[H] \models \psi((\theta_1)_H,\dots,(\theta_n)_H). \end{align*} The order convention is that $p \leq q$ means that $p$ is stronger than $q$; with this convention, a filter is upward closed from stronger conditions to weaker conditions. [/step]

[step:Define the separating name inside $M$]Let $S \in M$ be the set of first coordinates appearing in $\tau$: \begin{align*} S = \{\sigma : \text{there exists } q \in \mathbb{P} \text{ such that } (\sigma,q) \in \tau\}. \end{align*} This is a set in $M$ by Replacement applied in $M$ to the set $\tau$. Define $B \in M$ by \begin{align*} B = \{p \in \mathbb{P} : \text{there exist } \sigma \in S \text{ and } q \in \mathbb{P} \text{ such that } (\sigma,q) \in \tau \text{ and } p \leq q\}. \end{align*} This is a subset of $\mathbb{P}$ definable in $M$ from $\tau$ and $\mathbb{P}$, so $B \in M$ by Separation in $M$. Now define the $\mathbb{P}$-name $\rho$ by \begin{align*} \rho = \{(\sigma,p) \in S \times B : \text{there exists } q \in \mathbb{P} \text{ such that } (\sigma,q) \in \tau,\ p \leq q,\text{ and } p \Vdash_{\mathbb{P}} \varphi(\sigma,\zeta)\}. \end{align*} The relation $p \Vdash_{\mathbb{P}} \varphi(\sigma,\zeta)$ is definable over $M$ by the forcing theorem (citing a result not yet in the wiki: Forcing Theorem). Therefore $\rho$ is a subset of the set $S \times B$ definable in $M$ from parameters $\tau,\zeta,\mathbb{P}$, and Separation in $M$ gives $\rho \in M$.[/step]

[guided]The goal is to build, before passing to the extension, a name whose interpretation will be the separated subset. Since $a=\tau_G$, every possible element of $a$ has the form $\sigma_G$ for some first coordinate $\sigma$ appearing in $\tau$. We therefore define \begin{align*} S = \{\sigma : \text{there exists } q \in \mathbb{P} \text{ such that } (\sigma,q) \in \tau\}. \end{align*} Because $\tau$ is a set in $M$, the collection of its first coordinates is also a set in $M$. Next we restrict the possible tags. If a condition $p$ is to certify that $\sigma_G$ belongs to the separated subset, then $p$ should strengthen some condition $q$ already tagging $\sigma$ in $\tau$. This motivates \begin{align*} B = \{p \in \mathbb{P} : \text{there exist } \sigma \in S \text{ and } q \in \mathbb{P} \text{ such that } (\sigma,q) \in \tau \text{ and } p \leq q\}. \end{align*} This is a subset of the forcing poset $\mathbb{P}$, and the defining condition only uses parameters belonging to $M$. Since $M \models \mathrm{ZFC}$, Separation inside $M$ gives $B \in M$. We now define \begin{align*} \rho = \{(\sigma,p) \in S \times B : \text{there exists } q \in \mathbb{P} \text{ such that } (\sigma,q) \in \tau,\ p \leq q,\text{ and } p \Vdash_{\mathbb{P}} \varphi(\sigma,\zeta)\}. \end{align*} The important point is that this is not a proper class construction. The pair $(\sigma,p)$ ranges over the set $S \times B$, and the additional predicate $p \Vdash_{\mathbb{P}} \varphi(\sigma,\zeta)$ is definable over $M$ by the forcing theorem (citing a result not yet in the wiki: Forcing Theorem). Thus the defining condition is a legitimate formula over $M$ with parameters in $M$. Applying Separation in $M$ to the set $S \times B$ gives $\rho \in M$.[/guided]

[step:Show that every element of $\rho_G$ satisfies the separating formula] Let $x \in \rho_G$. By the valuation definition, there exist a name $\sigma \in M$ and a condition $p \in G$ such that \begin{align*} (\sigma,p) \in \rho \end{align*} and \begin{align*} x = \sigma_G. \end{align*} By the definition of $\rho$, there exists $q \in \mathbb{P}$ such that \begin{align*} (\sigma,q) \in \tau, \end{align*} \begin{align*} p \leq q, \end{align*} and \begin{align*} p \Vdash_{\mathbb{P}} \varphi(\sigma,\zeta). \end{align*} Since $G$ is a filter and $p \in G$ with $p \leq q$, the upward closure convention for filters gives $q \in G$. Hence $\sigma_G \in \tau_G$, so \begin{align*} x \in a. \end{align*} Also, since $p \in G$ and $p \Vdash_{\mathbb{P}} \varphi(\sigma,\zeta)$, the forcing theorem gives \begin{align*} M[G] \models \varphi(\sigma_G,\zeta_G). \end{align*} Using $\sigma_G=x$ and $\zeta_G=z$, we obtain \begin{align*} M[G] \models \varphi(x,z). \end{align*} Therefore \begin{align*} \rho_G \subseteq \{x \in a : M[G] \models \varphi(x,z)\}. \end{align*} [/step]

[step:Show that every element satisfying the formula is named by $\rho$] Let \begin{align*} x \in \{y \in a : M[G] \models \varphi(y,z)\}. \end{align*} Then $x \in a=\tau_G$, so by the valuation definition there exist a name $\sigma \in M$ and a condition $q \in G$ such that \begin{align*} (\sigma,q) \in \tau \end{align*} and \begin{align*} \sigma_G = x. \end{align*} Since $M[G]\models \varphi(x,z)$, and since $x=\sigma_G$ and $z=\zeta_G$, we have \begin{align*} M[G]\models \varphi(\sigma_G,\zeta_G). \end{align*} By the [truth lemma for forcing](/theorems/6518) (citing a result not yet in the wiki: Truth Lemma), there exists $p_0 \in G$ such that \begin{align*} p_0 \Vdash_{\mathbb{P}} \varphi(\sigma,\zeta). \end{align*} Because $G$ is a filter, it is directed downward with respect to the order $\leq$. Hence, from $p_0,q \in G$, there exists $r \in G$ such that \begin{align*} r \leq p_0 \end{align*} and \begin{align*} r \leq q. \end{align*} Forcing is monotone under strengthening, so from $r \leq p_0$ and $p_0 \Vdash_{\mathbb{P}} \varphi(\sigma,\zeta)$ we get \begin{align*} r \Vdash_{\mathbb{P}} \varphi(\sigma,\zeta). \end{align*} Together with $(\sigma,q)\in\tau$ and $r \leq q$, the definition of $\rho$ gives \begin{align*} (\sigma,r) \in \rho. \end{align*} Since $r \in G$, the valuation definition yields $\sigma_G \in \rho_G$. Thus $x=\sigma_G \in \rho_G$, proving \begin{align*} \{x \in a : M[G] \models \varphi(x,z)\} \subseteq \rho_G. \end{align*} [/step]

[step:Identify the separated subset as an element of the extension] Combining the two inclusions, we have \begin{align*} \rho_G = \{x \in a : M[G] \models \varphi(x,z)\}. \end{align*} Since $\rho \in M$ is a $\mathbb{P}$-name, its valuation $\rho_G$ belongs to $M[G]$ by the definition of the forcing extension. Therefore \begin{align*} \{x \in a : M[G] \models \varphi(x,z)\} \in M[G]. \end{align*} This proves Separation in the forcing extension. [/step]