Rank of element in generic extension versus rank of its name I sometimes see the following fact used in some arguments:

suppose $M[G]$ is a generic extension of $M$ by a forcing $\mathbb P$ and suppose $x\in M[G]$ has rank $<\gamma$, where $\gamma$ is some limit ordinal above rank$(\mathbb{P})$. Then there is a name $\tau\in M^\mathbb{P}$ such that $\tau_G=x$ and $\tau$ has rank $<\gamma$.

For example, this fact is used in Reitz's The Ground Axiom in proving that the ground model is definable, at the end of the first paragraph in the proof of Lemma 7.1.
But I'm not sure how to prove this. Any help appreciated!
Added after edit: if we assume additionally that $\gamma$ is a $\beth$-fixed point (equivalently, $H_\gamma=V_\gamma$. This holds in the special case in Lemma 7.1 referenced above), then I think the following argument works.
By induction on rank, we show that if $x\in (H_\gamma)^{M[G]}$, then there is a name $\sigma\in H_\gamma\cap M^{\mathbb{P}}$ such that $\sigma_G=x$. So suppose this holds for all sets of lower ranks than $x$. Hence each $y\in trcl(x)$ has a name $n(y)$ whose rank is lower than $\gamma$. Now collecting all those names, let $z=\{n(y)\mid y\in trcl(x)\}$. Since $x\in (H_\gamma)^{M[G]}$, we know $|trcl(x)|=\kappa<\gamma$. This means also that $|z|=\kappa$. The preceding cardinality claims are all in the sense of $M[G]$, and we fix a surjection $f:\kappa\to z$ in $M[G]$.
Let $\rho$ be a name for $x$ and $\tau$ be a name for $z$. By the truth lemma, we may fix some $p\in G$ such that
$$
p\Vdash \rho\in (H_\gamma)^{M[G]} \wedge \text{ every element of } \rho \text{ has a name of rank } <\gamma \\ \wedge \tau \subseteq \check{(H_\gamma)} \wedge\dot{f}:\kappa \to \tau \text{ is a surjection}
$$
We then proceed to define our low-rank name $\sigma$ for $x$. For each $\alpha<\kappa$, we let
$$
X_\alpha = \{ q \in \mathbb{P} \mid \ (\exists \pi \in H_{\gamma}\cap M^{\mathbb{P}})~ q \leq p \wedge q \Vdash (\dot{f}(\alpha)=\check{\pi} \wedge \pi \in \rho)\}
$$
In other words, $X_\alpha$ collects those conditions below $p$ that will force (the evaluation of) an element in $z$ to be an element of $x$.
Now for each $X_\alpha$, fix a maximal antichain $A_\alpha$ that it intersects. For each $\alpha<\kappa$ and $q\in X_\alpha\cap A_\alpha$, there is some $\mathbb P$-name $v(\alpha,q)$ such that $q\Vdash v(\alpha,q)\in\rho\wedge \dot f(\alpha)=\check{v(\alpha,q)}$. Now we can define the name $\sigma$ to be
$$
\sigma = \{(\pi,q)\mid (\exists\alpha)( \alpha < \kappa \wedge q \in X_{\alpha} \cap A_{\alpha} \wedge \pi = v(\alpha,q))\}
$$
Then $\sigma$ is a name in $H_\gamma\cap M^{\mathbb P}$, and $p\Vdash \sigma=\rho$.
Second edit: it seems like the special case sketched above has a duplicate (?) Regardless, I'd still be interested in seeing how to argue for the stronger claim quoted.
 A: I will work over $V$ instead of $M$. I think the following proof works over $\mathsf{ZFC^-}$ (i.e., $\mathsf{ZFC}$ without Power Set and with Collection and the well-ordering principle) with the existence of $\mathcal{P}(\mathbb{P})$. (Especially, it holds over $M=H_\theta$ for large regular $\theta$.)

Lemma. Let $x\in V^\mathbb{P}$ be a name such that $\operatorname{rank}x\ge\operatorname{rank}\mathbb{P}$ and $\gamma$ be a ordinal greater than $\operatorname{rank}\mathbb{P}$. If $p\Vdash \operatorname{rank}x=\check{\gamma}$, then there is $\tau\in V^\mathbb{P}$ such that

*

*$p\Vdash x=\check{\tau}^{\dot{G}}$, and


*$\operatorname{rank}\tau\le\gamma_0+3n$, where $\gamma=\gamma_0+n$ for some limit $\gamma_0$ and $n\in\omega$.

Let me introduce some notation on ordinals: for each ordinal $\alpha$, $\alpha^*$ and $\alpha^@\in\omega$ be ordinals such that $\alpha=\alpha^*+\alpha^@$ and $\alpha^*$ is a limit ordinal.
I will use induction on the rank of $x$. Without loss of generality, we may assume that

*

*if $(y,q)\in x$ then $q\le p$, and


*(Downward closeness) if $(y,q)\in x$ and $r\le q$, then $(y,r)\in x$
by replacing $x$ to
$$x'=\{(y,r)\mid \exists q (y,q)\in x \text{ and } r\le p,q\}.$$
Since $\operatorname{rank} x\ge\operatorname{rank}\mathbb{P}$,  we have $\operatorname{rank}x'\le\operatorname{rank}x$.
Then for each $(y,q)\in x$, $q\Vdash \operatorname{rank}y<\check{\gamma}$. Find a maxinal antichain $A_{y,q}$ below $q$ which decides the value or $\operatorname{rank}y$; that is, if $r\in A_{y,q}$ then there is an ordinal $\beta_{y,q,r}<\gamma$ such that $r\Vdash \operatorname{rank}y=\check{\beta}_{y,q,r}$.
By the inductive hypothesis, we can find $\tau_{y,q,r}$ such that $r\Vdash y=\tau_{y,q,r}^{\dot{G}}$ and
$$\operatorname{rank}\tau_{y,q,r}\le\beta_{y,q,r}^*+3\beta_{y,q,r}^@.$$
Now take
$$\tau=\{(\tau_{y,q,r},r)\mid (y,q)\in x\text{ and }r\in A_{y,q}\}.$$
Then we can prove $p\Vdash x=\check{\tau}^{\dot{G}}$. It remains to check the rank of $\tau$. We can see that
$$\operatorname{rank}(\tau_{y,q,r},r)\le\max(\operatorname{rank}r, \beta_{y,q,r}^*+3\beta_{y,q,r}^@)+2$$

*

*Case 1. If $\gamma$ is a limit ordinal, then the right-hand-side is strictly less than $\gamma$. Hence $\operatorname{rank}\tau\le\gamma$.


*Case 2. If $\gamma=\gamma_0+n$ for some limit $\gamma_0$ and $1\le n<\omega$, then
$$p\Vdash \forall y\in x (\operatorname{rank} y\le\check{\gamma}_0+\check{n}-1).$$
Hence the corresponding $\beta_{y,q,r}$ satisfies $\beta_{y,q,r}\le \gamma_0+n-1$, and thus $\tau_{y,q,r}$ satisfies
$$\operatorname{rank}\tau_{y,q,r}\le\gamma_0+3(n-1).$$
The remaining argument is direct, and we have $\operatorname{rank} \tau\le\gamma_0+3n$.
