 Solution

We use only the definability and truth clauses of the forcing theorem. For every formula, its forcing relation on names is definable inside $M$; forcing is preserved by strengthening; and $M[G]\models \phi ({\vec{\tau }}^G)$ exactly when some condition in $G$ forces $\phi (\vec{\tau })$. These clauses do not presuppose the Separation axiom we are proving.

Let $a={\tau }^G$ and let ${\vec{\sigma }}^G$ be the parameters in the desired instance. In $M$, form the nameThis is a set in $M$ by its Separation axiom and forcing definability, using the subnames of $\tau$ and $P$ as a set-sized bound.

If $x\in {\rho }^G$, some $q\in G$ activates $(\nu ,q)$ and $q\ge p$ activates $(\nu ,p)\in \tau$. Thus $x={\nu }^G\in a$, and the forcing theorem gives $\phi (x,{\vec{\sigma }}^G)$. Conversely, if $x\in a$ satisfies that formula, choose an active pair $(\nu ,p)\in \tau$ with $x={\nu }^G$ and a condition $r\in G$ forcing the formula. Directedness gives $q\in G$ stronger than both $p$ and $r$. Monotonicity puts $(\nu ,q)\in \rho$, so $x\in {\rho }^G$.

ThereforeEvery requested instance of separation in a generic extension follows.