If $X$ is a set and $I$ is an ideal on $X$. Let $\mathbb{P}$ be the forcing poset consisting of $I^+$ subsets of $X$ with the subset partial ordering. Let $G$ be $\mathbb{P}$-generic filter over $M$, where $M$ is the ground model.

As in Jech Lemma 22.13, it can be shown that $G$ is a $M$-ultrafilter on $X$. I presume this means that in $M[G]$, it is proved that $G$ is $M$-ultrafilter.

Then the generic ultrapower is defined in $M[G]$ as follows : it consist of the equivalence classes of function $f : X \rightarrow M$ with $f \in M$ under the usual ultrapower equivalence relation with $\in^{Ult_G(M)}$ defined in the usual way.

I would like to think of the generic ultrapower as a class model in $M[G]$, but it is not immediately clear that it is definable.

The first issue is how exactly is Lemma 22.13 phrased in $M[G]$. How does $M[G]$ talk about $M$?

Then in the construction of the ultrapower, the equivalence class can of course be made into sets by considering element of least rank in each class. However, $M[G]$ still needs to distinguish those $f : X \rightarrow M$ which are in the ground models. Again, the main issue here seems to be whether $M$ is an inner model of $M[G]$.

I am vaguely aware of some result about $M$ being in some sense definable in $M[G]$? I do not know the result precisely to be able to tell if this result could be used to think of the generic ultrapower as a proper class. Nevertheless, it seems that Solovay used the generic ultrapower well before this result was known. How did he handle the definability issue of the generic ultrapower?