I'm reading section 1.12 in Solovay's A model of Set-Theory in Which Every Set of Reals is Lebesgue Measurable, which aims to prove a uniformization property for definable sets of reals. More precisely, the situation is as follows (I'll be mostly following his notation):
Let $M$ be a transitive model of ZFC, $\Omega$ an inaccessible cardinal in $M$, and $\mathbb{P}$ the Levy collapse which makes $\Omega$ the $\omega_1$ of the extension. We let $N$ be some $\mathbb{P}$-generic extension of $M$, i.e. $N=M[H] $ for some $H$ which is generic over $M$. Suppose $A\subset \mathbb{R}^2$, $A\in N$, and $A$ is definable from parameters in $\mathbb{R}\cup M$. We want to produce $h:\mathbb{R}\to \mathbb{R}$ such that $(x,h(x))\in A$ for all $x\in\mathbb{R}$.
At one point in the proof (Lemma 2), we let $x$ be a real random over $M$ and $G$ an $\mathbb{P}$-generic filter over $M[x]$. Let $\Psi_2(\xi)$ be a formula which says $$ \xi<\Omega\wedge A_x\cap M[x][G^\xi]\neq\emptyset $$ where $G^\xi$ is the induced generic in the collapse up to $\xi$. This formula is in an extension of the language of set theory (which already includes a symbol for the ground model) by constants $\mathbf x$ and $\mathbf G$, intepreted in $M[x][G]$ in the obvious way. As a side question, is this equivalent to just looking at the forcing language for $\mathbb{P}$ in $M[x]$?
By general facts of the Levy collapse, we know that, given $G$ and $x$ as above, there is some $\xi<\Omega$ with $$ M[x][G]\models \Psi_2(\xi) $$ so that there is some $p\in G$ which force $\Psi_2(\check \xi)$ (where we force over the ground $M[x]$). By homogeneity, $\Vdash\Psi_2(\check \xi)$ .
Now Solovay says (page 48 of the paper) that we can find a formula $\Psi_3(x,\xi)$ such that $$ M[x]\models \Psi_3(x,\xi)\iff M[x][G]\models (\Vdash \Psi_2(\xi)) $$ I'm afraid I don't see what's going on here. What poset does the above instance of $\Vdash$ refer to? And how are we finding such a formula?
As a side question, are there any more modern treatments of this particular uniformization result? I've checked Jech, Kanamori, and Bartoszynski-Judah with no luck. Solovay's writing style is very nice, but I do feel I am getting lost in the slightly out-of-fashion notation/terminology.