[proofplan] Choose $\mathbb{P}$-names $\tau,\zeta \in M$ for $a$ and $z$, and strengthen inside the generic filter to a condition forcing the functional statement for these names. Below that condition, use the rank-bound theorem for forced unique values to obtain an ordinal $\alpha \in M$ such that every possible output has an equivalent name in $V_\alpha^M$. Then define, in $M$, a bounded name $\rho$ whose tagged names are precisely those bounded representatives forced to be values of $\varphi$ on tagged elements of $\tau$. Finally prove that $\rho_G$ is exactly the desired image set by the [forcing theorem](/theorems/6531) and truth lemma. We use the standard forcing theorem, truth lemma, and rank-bound theorem for forced unique values; citing results not yet verified in the wiki: Forcing Theorem, Truth Lemma, rank-bound theorem for forced unique values. [/proofplan]

[step:Choose names and pass to a cone where the functional statement is forced] Choose $\mathbb{P}$-names $\tau,\zeta \in M$ such that $\tau_G = a$ and $\zeta_G = z$. Since \begin{align*} M[G] \models \forall x \in \tau_G\, \exists! y\, \varphi(x,y,\zeta_G), \end{align*} the Truth Lemma applied to the original forcing poset $\mathbb{P}$, the $M$-generic filter $G$, and the $\mathbb{P}$-names $\tau$ and $\zeta$ gives a condition $p_0 \in G$ such that \begin{align*} p_0 \Vdash_{\mathbb{P}} \forall x \in \tau\, \exists! y\, \varphi(x,y,\zeta). \end{align*} We keep the original forcing poset $\mathbb{P}$ throughout the proof. Thus every name used below is a $\mathbb{P}$-name in $M$, and every appeal to the Forcing Theorem or the Truth Lemma is made over $\mathbb{P}$ with the given $M$-generic filter $G$. Conditions stronger than $p_0$ are handled by explicitly requiring $p \le p_0$, rather than replacing $\mathbb{P}$ by the cone below $p_0$. [/step]

[step:Obtain a uniform rank bound for all forced outputs] Apply the [Rank Bound for Replacement Names](/theorems/6536) to the forcing poset $\mathbb{P}$, the condition $p_0$, the input name $\tau$, the parameter name $\zeta$, and the formula $\varphi(x,y,z)$. Its hypotheses are satisfied because $\mathbb{P},p_0,\tau,\zeta \in M$ and the previous step proves \begin{align*} p_0 \Vdash_{\mathbb{P}} \forall x \in \tau\, \exists! y\, \varphi(x,y,\zeta). \end{align*} Therefore there is an ordinal $\alpha \in M$ such that the following uniform rank-bound statement holds in $M$: for every tagged input $(\sigma,q) \in \tau$ and every condition $p \in \mathbb{P}$ satisfying $p \le p_0$ and $p \le q$, if \begin{align*} p \Vdash_{\mathbb{P}} \exists y\, \varphi(\sigma,y,\zeta), \end{align*} then the set of conditions $r \le p$ for which there is a $\mathbb{P}$-name $\nu \in V_\alpha^M$ satisfying \begin{align*} r \Vdash_{\mathbb{P}} \varphi(\sigma,\nu,\zeta) \end{align*} is dense below $p$ in $\mathbb{P}$. This is the precise uniformity needed later: the ordinal $\alpha$ is independent of the tagged member $(\sigma,q) \in \tau$ and independent of the stronger condition $p$ below both $p_0$ and $q$. [/step]

[step:Define a bounded name for the image inside $M$]Define a $\mathbb{P}$-name $\rho \in M$ by \begin{align*} \rho := \{(\nu,p) \in V_\alpha^M \times \mathbb{P} : p \le p_0 \text{ and } \exists (\sigma,q) \in \tau \text{ such that } p \le q \text{ and } p \Vdash_{\mathbb{P}} \varphi(\sigma,\nu,\zeta)\}. \end{align*} This is a set in $M$: the ambient set $V_\alpha^M \times \mathbb{P}$ belongs to $M$, the name $\tau$ belongs to $M$, and the forcing relation for the fixed formula $\varphi$ over $\mathbb{P}$ is definable in $M$. Hence $\rho$ is obtained by separation in $M$.[/step]

[guided]The purpose of $\rho$ is to collect only bounded names, namely names $\nu \in V_\alpha^M$, while still representing every actual output in the extension. The rank-bound theorem supplies the ordinal $\alpha$, so it is enough to search inside the set $V_\alpha^M$ rather than through the proper class of all names. We define \begin{align*} \rho := \{(\nu,p) \in V_\alpha^M \times \mathbb{P} : p \le p_0 \text{ and } \exists (\sigma,q) \in \tau \text{ such that } p \le q \text{ and } p \Vdash_{\mathbb{P}} \varphi(\sigma,\nu,\zeta)\}. \end{align*} Each part of this definition has a specific role. The requirement $\nu \in V_\alpha^M$ enforces the rank bound. The requirement $p \le p_0$ records that we are working below the condition that forces the functional statement, while still using the original forcing poset $\mathbb{P}$. The requirement $(\sigma,q) \in \tau$ says that $\sigma$ is a name tagged as a possible member of $\tau$. The inequality $p \le q$ ensures that whenever $p \in G$, upward closure of the filter gives $q \in G$, and therefore $\sigma_G \in \tau_G=a$. Finally, the forcing condition \begin{align*} p \Vdash_{\mathbb{P}} \varphi(\sigma,\nu,\zeta) \end{align*} ensures that $\nu_G$ is forced to be the $\varphi$-value associated to the input $\sigma_G$. We must also justify that $\rho$ is itself a name in $M$. The product $V_\alpha^M \times \mathbb{P}$ is a set of $M$ because $\alpha \in M$, $M$ satisfies $\mathrm{ZFC}$, and $\mathbb{P} \in M$. The relation “$(\sigma,q) \in \tau$” is bounded by the set $\tau \in M$, and the forcing relation for the fixed formula $\varphi$ over the set forcing $\mathbb{P}$ is definable in $M$. Therefore separation in $M$ produces the set $\rho \subseteq V_\alpha^M \times \mathbb{P}$. Thus $\rho$ is a $\mathbb{P}$-name belonging to $M$.[/guided]

[step:Show every element interpreted from $\rho$ is in the desired image] Let $y \in \rho_G$. By the definition of name evaluation, there are $\nu \in V_\alpha^M$ and $p \in G$ such that $(\nu,p) \in \rho$ and $\nu_G=y$. Since $(\nu,p) \in \rho$, there exists $(\sigma,q) \in \tau$ such that $p \le p_0$, $p \le q$, and \begin{align*} p \Vdash_{\mathbb{P}} \varphi(\sigma,\nu,\zeta). \end{align*} Because $p \in G$ and $p \le q$, upward closure of the filter gives $q \in G$. Hence $(\sigma,q) \in \tau$ with $q \in G$, so $\sigma_G \in \tau_G=a$. The Forcing Theorem applies because $\sigma,\nu,\zeta$ are $\mathbb{P}$-names in $M$, $p \in G$, and $G$ is $M$-generic for $\mathbb{P}$. It gives \begin{align*} M[G] \models \varphi(\sigma_G,\nu_G,\zeta_G). \end{align*} Since $\zeta_G=z$ and $\nu_G=y$, there exists $x \in a$, namely $x=\sigma_G$, such that \begin{align*} M[G] \models \varphi(x,y,z). \end{align*} Therefore $y$ belongs to the displayed image set. [/step]

[step:Show every value of the formula is interpreted from $\rho$] Let $y \in M[G]$ satisfy \begin{align*} \exists x \in a \text{ such that } M[G] \models \varphi(x,y,z). \end{align*} Choose $x \in a$ with \begin{align*} M[G] \models \varphi(x,y,z). \end{align*} Choose a $\mathbb{P}$-name $\mu \in M$ such that $\mu_G=y$. Since $x \in a=\tau_G$, there are a name $\sigma \in M$ and a condition $q \in G$ such that $(\sigma,q) \in \tau$ and $\sigma_G=x$. Because $p_0,q \in G$ and $G$ is directed, choose $s_0 \in G$ such that \begin{align*} s_0 \le p_0 \quad \text{and} \quad s_0 \le q. \end{align*} Since \begin{align*} M[G] \models \varphi(\sigma_G,\mu_G,\zeta_G), \end{align*} the Truth Lemma applies over $\mathbb{P}$ to the $\mathbb{P}$-names $\sigma,\mu,\zeta$ and gives a condition $s_1 \in G$ with $s_1 \le s_0$ such that \begin{align*} s_1 \Vdash_{\mathbb{P}} \varphi(\sigma,\mu,\zeta). \end{align*} By the rank-bound property from the previous step, applied to the tagged input $(\sigma,q) \in \tau$ and to the condition $s_1 \le p_0,q$, the set of conditions below $s_1$ that force the output to be represented by some bounded name $\nu \in V_\alpha^M$ is dense below $s_1$. Since $G$ is $M$-generic and $s_1 \in G$, choose $r \in G$ and $\nu \in V_\alpha^M$ such that $r \le s_1$ and \begin{align*} r \Vdash_{\mathbb{P}} \varphi(\sigma,\nu,\zeta). \end{align*} Because $r \le s_1 \le s_0 \le p_0$ and $r \le s_1 \le s_0 \le q$, the defining condition for membership in $\rho$ is satisfied, so $(\nu,r) \in \rho$. Since $p_0$ forces uniqueness of the $\varphi$-value for every element of $\tau$, $r \le p_0$, and $r$ forces both $\varphi(\sigma,\mu,\zeta)$ and $\varphi(\sigma,\nu,\zeta)$, monotonicity of forcing and first-order logic inside the forcing relation give \begin{align*} r \Vdash_{\mathbb{P}} \mu=\nu. \end{align*} As $r \in G$, the Forcing Theorem gives $\mu_G=\nu_G$. Therefore \begin{align*} y=\mu_G=\nu_G\in \rho_G. \end{align*} Thus every element of the displayed image set belongs to $\rho_G$. [/step]

[step:Identify the image set as a member of the generic extension] The two inclusions prove \begin{align*} \rho_G = \{y \in M[G] : \exists x \in a \text{ such that } M[G] \models \varphi(x,y,z)\}. \end{align*} Since $\rho \in M$ is a $\mathbb{P}$-name and $G$ is the original $M$-generic filter, the definition of the generic extension gives $\rho_G \in M[G]$. Therefore the desired image set belongs to $M[G]$. [/step]