[proofplan] We work inside the transitive model $M$ and use Replacement there to make the possible witnesses uniform over the set of relevant input triples. For each triple $((\sigma,q),p)$ with $(\sigma,q)\in\tau$ and $p\leq q$, we consider the set of all pairs $(\mu,r)$ such that $r\leq p$ and $r$ forces $\varphi(\sigma,\mu,\zeta)$. Whenever this set is nonempty, we choose a witness whose name has minimal $M$-rank, and Replacement collects all selected names into one set $B\in M$. An ordinal $\alpha\in M$ bounding the ranks of names in $B$ then works, because the forced uniqueness of the $y$ satisfying $\varphi(\sigma,y,\zeta)$ turns the selected witness into a forced equal of any other witness. [/proofplan]

[step:Form the set of all relevant input triples inside $M$]Define, in $M$, the set \begin{align*} A := \{((\sigma,q),p) \in \tau \times \mathbb{P} : p \leq q\}. \end{align*} This is a set in $M$ by Separation, since $\tau,\mathbb{P}\in M$ and the order relation on $\mathbb{P}$ belongs to $M$. For each $a=((\sigma,q),p)\in A$, define the class \begin{align*} W_a := \{(\mu,r) : \mu \text{ is a } \mathbb{P}\text{-name in } M,\ r\in\mathbb{P},\ r\leq p,\ r\Vdash_{\mathbb{P}} \varphi(\sigma,\mu,\zeta)\}. \end{align*} The forcing relation for a fixed formula is definable over $M$, so the relation “$(\mu,r)\in W_a$” is first-order definable in $M$ from the parameters $a,\mathbb{P},\tau,\zeta,\varphi$.[/step]

[guided]The first task is to make precise the collection over which Replacement will be applied. The possible inputs are not arbitrary triples: they are exactly the tagged names $(\sigma,q)$ appearing in $\tau$, together with stronger conditions $p\leq q$. Thus we define \begin{align*} A := \{((\sigma,q),p) \in \tau \times \mathbb{P} : p \leq q\}. \end{align*} Because $\tau$ and $\mathbb{P}$ are elements of $M$, and because the order relation of the forcing poset is part of $\mathbb{P}$ as computed in $M$, Separation in $M$ gives $A\in M$. Now fix $a=((\sigma,q),p)\in A$. We want to know which names can serve as possible values of the uniquely defined object associated to $\sigma$. So we define \begin{align*} W_a := \{(\mu,r) : \mu \text{ is a } \mathbb{P}\text{-name in } M,\ r\in\mathbb{P},\ r\leq p,\ r\Vdash_{\mathbb{P}} \varphi(\sigma,\mu,\zeta)\}. \end{align*} This is a definable class of $M$, not necessarily a set at this point, because the name $\mu$ ranges over all $\mathbb{P}$-names in $M$. The important point is definability: for a fixed formula $\varphi$, the forcing relation $r\Vdash_{\mathbb{P}}\varphi(\sigma,\mu,\zeta)$ is definable in $M$. Therefore the assignment $a\mapsto W_a$ can be discussed by formulas inside $M$, which is exactly what Replacement and Separation require in the next step.[/guided]

[step:Choose one minimal-rank witness for each nonempty witness class] Let $\operatorname{rank}^M$ denote the rank function of $M$, restricted to the class of $\mathbb{P}$-names in $M$; thus $\operatorname{rank}^M(\mu)$ is the unique ordinal $\beta\in\operatorname{Ord}^M$ such that $M$ computes $\mu\in V_{\beta+1}^M\setminus V_\beta^M$. For $a=((\sigma,q),p)\in A$ with $W_a\neq\varnothing$, define $\beta_a$ to be the least ordinal $\beta\in\operatorname{Ord}^M$ for which there exist a $\mathbb{P}$-name $\mu\in V_{\beta+1}^M$ and a condition $r\in\mathbb{P}$ such that $(\mu,r)\in W_a$ and $\operatorname{rank}^M(\mu)=\beta$. This least ordinal exists because the $M$-ranks of names appearing in $W_a$ form a nonempty class of ordinals of $M$, and ordinals are well-ordered in $M$. For such $a$, define \begin{align*} C_a := \{(\mu,r)\in V_{\beta_a+1}^M \times \mathbb{P} : \operatorname{rank}^M(\mu)=\beta_a,\ r\leq p,\ r\Vdash_{\mathbb{P}}\varphi(\sigma,\mu,\zeta)\}. \end{align*} Then $C_a\in M$ by Separation, and $C_a$ is nonempty by the definition of $\beta_a$. Since $A$ is a set in $M$, the family of all nonempty sets $C_a$ for $a\in A$ and $W_a\neq\varnothing$ is a set-indexed family in $M$. By the [Axiom of Choice](/page/Axiom%20of%20Choice) in $M$, there is a choice function in $M$ selecting one pair \begin{align*} (\nu_a,r_a)\in C_a \end{align*} for every $a\in A$ with $W_a\neq\varnothing$. [/step]

[step:Apply Replacement to bound the selected names by one rank] Let \begin{align*} B := \{\nu_a : a\in A,\ W_a\neq\varnothing\}. \end{align*} Since the selected pair $(\nu_a,r_a)$ is chosen by a function in $M$ on a subset of the set $A\in M$, Replacement in $M$ gives $B\in M$. Define \begin{align*} \gamma := \sup\{\operatorname{rank}^M(\nu)+1 : \nu\in B\}. \end{align*} Since $B\in M$ is a set of names, Replacement and Union in $M$ imply that $\gamma$ is an ordinal of $M$. Let \begin{align*} \alpha := \gamma+1. \end{align*} Then $\alpha\in\operatorname{Ord}^M$, and every $\nu\in B$ belongs to $V_\alpha^M$. [/step]

[step:Compare an arbitrary witness with the selected minimal-rank witness]Fix $(\sigma,q)\in\tau$, $p\in\mathbb{P}$ with $p\leq q$, and a $\mathbb{P}$-name $\mu\in M$ such that \begin{align*} p\Vdash_{\mathbb{P}}\varphi(\sigma,\mu,\zeta). \end{align*} Set $a:=((\sigma,q),p)$. Then $a\in A$, and $(\mu,p)\in W_a$, so $W_a\neq\varnothing$. Therefore the construction above supplies a selected pair $(\nu_a,r_a)\in C_a$ with \begin{align*} r_a\leq p \end{align*} and \begin{align*} r_a\Vdash_{\mathbb{P}}\varphi(\sigma,\nu_a,\zeta). \end{align*} Moreover $\nu_a\in B\subseteq V_\alpha^M$. Since $(\sigma,q)\in\tau$, the condition $q$ forces $\sigma\in\tau$. Because $p\leq q$, monotonicity of forcing gives \begin{align*} p\Vdash_{\mathbb{P}}\sigma\in\tau. \end{align*} Also $1_{\mathbb{P}}$ forces \begin{align*} \forall x\in\tau\,\exists! y\,\varphi(x,y,\zeta), \end{align*} so every condition forces this sentence, in particular $r_a$ forces it. Since $r_a\leq p$, monotonicity gives \begin{align*} r_a\Vdash_{\mathbb{P}}\varphi(\sigma,\mu,\zeta). \end{align*} Thus $r_a$ forces both $\varphi(\sigma,\nu_a,\zeta)$ and $\varphi(\sigma,\mu,\zeta)$, while also forcing that the $y$ satisfying $\varphi(\sigma,y,\zeta)$ for this $\sigma\in\tau$ is unique. Hence \begin{align*} r_a\Vdash_{\mathbb{P}}\nu_a=\mu. \end{align*}[/step]

[guided]Now take an arbitrary witness from the statement. Thus we have $(\sigma,q)\in\tau$, a stronger condition $p\leq q$, and a name $\mu\in M$ such that \begin{align*} p\Vdash_{\mathbb{P}}\varphi(\sigma,\mu,\zeta). \end{align*} Define the corresponding input \begin{align*} a:=((\sigma,q),p). \end{align*} Because $(\sigma,q)\in\tau$ and $p\leq q$, this $a$ belongs to the set $A$ constructed earlier. Also $(\mu,p)\in W_a$, since $p\leq p$ and $p$ forces $\varphi(\sigma,\mu,\zeta)$. Therefore $W_a$ is nonempty, so the choice construction selected a pair $(\nu_a,r_a)\in C_a$. By the definition of $C_a$, this means \begin{align*} r_a\leq p \end{align*} and \begin{align*} r_a\Vdash_{\mathbb{P}}\varphi(\sigma,\nu_a,\zeta). \end{align*} By the definition of $B$ and the choice of $\alpha$, we also have $\nu_a\in B\subseteq V_\alpha^M$. It remains to prove that the selected name $\nu_a$ is forced equal to the arbitrary name $\mu$. The reason is uniqueness. Since $(\sigma,q)\in\tau$, the condition $q$ forces that $\sigma$ is an element of $\tau$. Because $p\leq q$, monotonicity of forcing gives \begin{align*} p\Vdash_{\mathbb{P}}\sigma\in\tau. \end{align*} Since $r_a\leq p$, monotonicity also gives \begin{align*} r_a\Vdash_{\mathbb{P}}\sigma\in\tau \end{align*} and \begin{align*} r_a\Vdash_{\mathbb{P}}\varphi(\sigma,\mu,\zeta). \end{align*} On the other hand, the hypothesis says \begin{align*} 1_{\mathbb{P}}\Vdash_{\mathbb{P}}\forall x\in\tau\,\exists! y\,\varphi(x,y,\zeta). \end{align*} Since every condition is stronger than $1_{\mathbb{P}}$, the condition $r_a$ also forces this uniqueness statement. Thus, below $r_a$, the object satisfying $\varphi(\sigma,y,\zeta)$ is unique; but $r_a$ forces that both $\nu_a$ and $\mu$ satisfy this same formula with input $\sigma$ and parameter $\zeta$. Therefore \begin{align*} r_a\Vdash_{\mathbb{P}}\nu_a=\mu. \end{align*}[/guided]

[step:Return the bounded replacement name] Set \begin{align*} \nu := \nu_a \end{align*} and \begin{align*} r := r_a. \end{align*} The preceding step gives $\nu\in V_\alpha^M$, $r\leq p$, and \begin{align*} r\Vdash_{\mathbb{P}}\nu=\mu. \end{align*} Since the original $(\sigma,q)$, $p$, and $\mu$ were arbitrary subject to the hypotheses, the ordinal $\alpha\in\operatorname{Ord}^M$ satisfies the required rank bound. [/step]