Replacement holds in $M[G]$

Question

I'm studying Forcing using Kunen's "Set Theory: An Introduction to Independence Proofs" and I'm having trouble on understanding a small detail in the proof of theorem 4.2 of chapter VII.

Let $\phi(x, v, r, z_1, ..., z_n)$ be any formula and $\sigma_G, \tau_{1_G}, ..., \tau_{n_G} \in M[G]$. We must check that if $(\forall x \in \sigma_G \exists !y \phi(x, y, \sigma_G, \tau_{1_G}, ..., \tau_{n_G}))^{M[G]}$ then there is a $\rho \in M^\mathbb P$ such that: $$\forall x \in \sigma_G \exists y \in \rho_G(\phi(x, y, \sigma_G, \tau_{1_G}, ..., \tau_{n_G}))^{M[G]}$$

In order to show that Replacement holds in $M[G]$, Kunen chooses an $S \in M$ such that $S \subset M^\mathbb P$ and such that $$\forall \pi \in dom(\sigma)\forall p \in \mathbb P [\exists \mu \in M^\mathbb P(p\Vdash\phi(\pi, \mu)) \rightarrow \exists \mu \in S(p \Vdash \phi(\pi, \mu))]$$

He claims that such and $S$ exists because $\Vdash$ is definable by a formula relativized to $M$, so by reflection in M, we may take $S=R(\alpha)^M\cap M^\mathbb P$ for a suitable $\alpha$. I did not understand how to use the reflection theorem here. Can someone explain to me how does reflection applies here?

Answer 1

We must show that there exists $S \in M$ such that $S \subset M^\mathbb P$ and such that $$\forall \pi \in dom(\sigma)\forall p \in \mathbb P [\exists \mu \in M^\mathbb P(p\Vdash\phi(\pi, \mu)) \rightarrow \exists \mu \in S(p \Vdash \phi(\pi, \mu))]$$

Let $\beta$ be such that $\mathbb P, dom(\sigma) \in R(\beta)$. We use reflection within $M$ for the formulas $\exists \mu \in V^\mathbb P(p\Vdash^*\phi(\pi,\mu))$, $\mu$ is a name and $p\Vdash^*\phi(\pi,\mu)$ to get $\alpha>\beta$ such that both formulas are absolute for $R(\alpha)$.

But then, fixing $p$ and $\pi$, it follows that:

$\exists \mu \in M^\mathbb P(p \Vdash \phi(\pi, \mu))\rightarrow(\exists \mu \in V^\mathbb P(p \Vdash^* \phi(\pi, \mu)))^M\rightarrow((\exists \mu \in V^\mathbb P(p \Vdash^* \phi(\pi, \mu)))^{R(\alpha)})^M\rightarrow(\exists \mu \in V^\mathbb P \cap R(\alpha)(p \Vdash^* \phi(\pi, \mu)))^M\rightarrow \exists \mu \in M^\mathbb P \cap R(\alpha)^M(p \Vdash \phi(\pi, \mu))$

So we may take $S=M^\mathbb P \cap R(\alpha)^M$.