In Kunen's book (introduction to independence proofs, ) the following lemma is proved (chapter 8, lemma 5.14):

Assume that in M, $\alpha$ is a limit ordinal, $( ( \mathbb{P}_\xi : \xi \leq \alpha) , (\pi_\xi : \xi < \alpha) )$ is an $\alpha$-stage iterated forcing construction with supports in $\mathcal{I}$ , and each element of $\mathcal{I}$ is bounded in $\alpha$. suppose G is $\mathbb{P}_\alpha$-generic over $M \:,\: S \in M \:,\: X\subseteq S \:,\: X \in M[G] \:,\: and \: (|S| < cf(\alpha))^{M[G]}.$ then for some $\eta<\alpha \:,\: X\in M[i_{\eta\alpha}^{-1}(G)]. $

the proof seemed very simple at first glance. however:

kunen shows that "for $s \in S \:,\: s \in X $ if and only if there is a $ \xi = \xi_s < \alpha$ such that $\exists p \in G_\xi (i_{\xi\alpha}(p)\Vdash_{\mathbb{P}_\alpha}\check{s} \in \sigma )$".

pretty obvious. but then kunen uses this to form, **in M[G]** , the set $\{\xi_s : s \in X\}$. why is this set in M[G]? the "$\exists p \in G_\xi $" part is ok, since the sequence $(G_\xi : \xi < \alpha)$ is in M[G]. but the "$(i_{\xi\alpha}(p)\Vdash_{\mathbb{P}_\alpha}\check{s} \in \sigma )$" , although it is indeed definable in M by definability of forcing,
it is not necessarily definable in M[G].

then he does it again by showing that X = $\{s \in S : \exists p \in G_\eta (i_{\eta\alpha}(p)\Vdash_{\mathbb{P}_\alpha}\check{s} \in \sigma ) \}$ and concluding that $X \in M[G_\eta]$, "since $\Vdash_{\mathbb{P}_\alpha}$ is defined in M " , although not necessarily in M[G].

why are these two arguments valid?