[proofplan] We prove that a dense embedding transports generic filters in both directions. Starting with a $P$-generic filter $G$, the generated set $H$ is a $Q$-filter, and dense subsets of $Q$ pull back to dense subsets of $P$. Conversely, a $Q$-generic filter $H$ induces a directed base $G_0$ in $P$; genericity of $H$ is used to meet dense sets below the relevant image conditions, and incompatibility preservation then gives directedness in $P$. Finally, the two filters are shown to correspond for the same pair $(G,H)$, and the recursive translations of names along $i$ identify the two generic extensions. [/proofplan] [step:Show that the image-generated set from a $P$-generic filter is a $Q$-filter] We use the defining clauses of a dense embedding: $i$ is order-preserving, the image $i[P]$ is dense in $Q$, $i$ preserves incompatibility, and whenever $p \in P$ and $q \in Q$ satisfy $q \le_Q i(p)$, there is $p' \in P$ such that $p' \le_P p$ and $i(p') \le_Q q$. We do not assume that $i$ reflects the order; where a preimage-membership statement is needed, it will be proved from genericity and incompatibility preservation. For $a,b \in P$, write $a \perp_P b$ to mean that no $c \in P$ satisfies $c \le_P a$ and $c \le_P b$; for $s,t \in Q$, write $s \perp_Q t$ to mean that no $u \in Q$ satisfies $u \le_Q s$ and $u \le_Q t$. These clauses and definitions belong to $M$ because $P$, $Q$, and $i$ belong to $M$. Assume that $G \subset P$ is $P$-generic over $M$, and define \begin{align*} H := \{q \in Q : \exists p \in G \text{ such that } i(p) \le_Q q\}. \end{align*} First, $H$ is upward closed. Let $q \in H$ and let $q' \in Q$ satisfy $q \le_Q q'$. Choose $p \in G$ with $i(p) \le_Q q$. By transitivity of $\le_Q$, \begin{align*} i(p) \le_Q q'. \end{align*} Thus $q' \in H$. Next, $H$ is downward directed. Let $q_0,q_1 \in H$. Choose $p_0,p_1 \in G$ such that \begin{align*} i(p_0) \le_Q q_0 \end{align*} and \begin{align*} i(p_1) \le_Q q_1. \end{align*} Since $G$ is downward directed, there exists $p_2 \in G$ such that \begin{align*} p_2 \le_P p_0 \end{align*} and \begin{align*} p_2 \le_P p_1. \end{align*} Since $i$ is order-preserving, \begin{align*} i(p_2) \le_Q i(p_0) \le_Q q_0 \end{align*} and \begin{align*} i(p_2) \le_Q i(p_1) \le_Q q_1. \end{align*} Because $i(p_2) \in H$, this proves that $H$ is downward directed. Hence $H$ is a filter on $Q$. [/step] [step:Pull dense subsets of $Q$ back to dense subsets of $P$] Let $D \subset Q$ be dense in $Q$ with $D \in M$. Define \begin{align*} D_P := \{p \in P : \exists d \in D \text{ such that } i(p) \le_Q d\}. \end{align*} Since $D$, $P$, $Q$, and $i$ belong to $M$, Separation in $M$ gives $D_P \in M$. We prove that $D_P$ is dense in $P$. Let $p_0 \in P$. Since $D$ is dense in $Q$, there exists $d \in D$ such that \begin{align*} d \le_Q i(p_0). \end{align*} By the lifting clause for the dense embedding $i$, there exists $p_1 \in P$ such that \begin{align*} p_1 \le_P p_0 \end{align*} and \begin{align*} i(p_1) \le_Q d. \end{align*} The same $d \in D$ witnesses $p_1 \in D_P$. Thus $D_P$ is dense in $P$. Since $G$ is $P$-generic over $M$, choose $p \in G \cap D_P$. By definition of $D_P$, choose $d \in D$ such that \begin{align*} i(p) \le_Q d. \end{align*} Because $p \in G$ and $i(p) \le_Q d$, the definition of $H$ gives $d \in H$. Therefore $d \in H \cap D$. Hence $H$ meets every [dense subset](/page/Dense%20Subset) of $Q$ belonging to $M$, so $H$ is $Q$-generic over $M$. [guided] We want to prove that $H$ is generic, so we must show that it meets every dense set $D \subset Q$ in $M$. The order convention is that stronger conditions are smaller, and filters are upward closed toward weaker conditions. Therefore we must arrange to find a condition $d \in D$ weaker than some image condition $i(p)$ with $p \in G$; then $d$ belongs to $H$ by the definition of $H$. Define \begin{align*} D_P := \{p \in P : \exists d \in D \text{ such that } i(p) \le_Q d\}. \end{align*} This set belongs to $M$ because it is definable in $M$ from the parameters $D$, $P$, $Q$, and $i$, all of which belong to $M$. We verify density. Let $p_0 \in P$. Since $D$ is dense in $Q$, there exists $d \in D$ such that \begin{align*} d \le_Q i(p_0). \end{align*} The lifting clause for the dense embedding applies to the pair $p_0 \in P$ and $d \le_Q i(p_0)$. Hence there exists $p_1 \in P$ such that \begin{align*} p_1 \le_P p_0 \end{align*} and \begin{align*} i(p_1) \le_Q d. \end{align*} This is exactly the relation needed in the definition of $D_P$, with the same witness $d \in D$. Therefore $p_1 \in D_P$. This proves that $D_P$ is dense in $P$. Because $G$ is $P$-generic over $M$, choose $p \in G \cap D_P$. Then there exists $d \in D$ such that \begin{align*} i(p) \le_Q d. \end{align*} Since $p \in G$, the definition of $H$ says that every $q \in Q$ above $i(p)$ belongs to $H$. Applying this with $q=d$ gives $d \in H$. Hence \begin{align*} d \in H \cap D. \end{align*} Thus $H$ meets $D$. Since $D \in M$ was arbitrary, $H$ is $Q$-generic over $M$. [/guided] [/step] [step:Construct a directed base in $P$ from a $Q$-generic filter] Assume now that $H \subset Q$ is $Q$-generic over $M$, and define \begin{align*} G_0 := \{p \in P : \exists q \in H \text{ such that } q \le_Q i(p)\}. \end{align*} We prove that $G_0$ is downward directed. Let $p_0,p_1 \in G_0$. Choose $q_0,q_1 \in H$ such that \begin{align*} q_0 \le_Q i(p_0) \end{align*} and \begin{align*} q_1 \le_Q i(p_1). \end{align*} Since $H$ is downward directed, choose $q \in H$ such that \begin{align*} q \le_Q q_0 \end{align*} and \begin{align*} q \le_Q q_1. \end{align*} Thus $q \le_Q i(p_0)$ and $q \le_Q i(p_1)$. Define \begin{align*} D_{q,p_0,p_1} := \{s \in Q : s \perp_Q q \text{ or } \exists r \in P \text{ such that } r \le_P p_0,\ r \le_P p_1,\ s \le_Q q,\text{ and } s \le_Q i(r)\}. \end{align*} Because $M$ is transitive and contains $P$ and $Q$, the elements $p_0,p_1 \in P$ and $q \in Q$ belong to $M$. Hence Separation in $M$ gives $D_{q,p_0,p_1} \in M$ from the parameters $P$, $Q$, $i$, $p_0$, $p_1$, and $q$. We prove that $D_{q,p_0,p_1}$ is dense in $Q$. Let $s_0 \in Q$. If $s_0 \perp_Q q$, then $s_0 \in D_{q,p_0,p_1}$. Otherwise choose $s_1 \in Q$ such that \begin{align*} s_1 \le_Q s_0 \end{align*} and \begin{align*} s_1 \le_Q q. \end{align*} Since $s_1 \le_Q q \le_Q i(p_0)$, the lifting clause gives $a \in P$ such that \begin{align*} a \le_P p_0 \end{align*} and \begin{align*} i(a) \le_Q s_1. \end{align*} Then $i(a) \le_Q s_1 \le_Q q \le_Q i(p_1)$, so $i(a)$ and $i(p_1)$ are compatible in $Q$. Since $i$ preserves incompatibility, the contrapositive gives that $a$ and $p_1$ are compatible in $P$. Choose $r \in P$ such that \begin{align*} r \le_P a \end{align*} and \begin{align*} r \le_P p_1. \end{align*} Then $r \le_P p_0$ as well, and order preservation gives \begin{align*} i(r) \le_Q i(a) \le_Q s_1 \le_Q s_0 \end{align*} and \begin{align*} i(r) \le_Q i(a) \le_Q s_1 \le_Q q. \end{align*} Taking $s := i(r)$ shows that some element of $D_{q,p_0,p_1}$ lies below $s_0$. Thus $D_{q,p_0,p_1}$ is dense in $Q$. Since $H$ is $Q$-generic over $M$, choose $h \in H \cap D_{q,p_0,p_1}$. The alternative $h \perp_Q q$ is impossible: because $h,q \in H$ and $H$ is downward directed, there would be $k \in H$ with $k \le_Q h$ and $k \le_Q q$, contradicting $h \perp_Q q$. Therefore the second alternative in the definition of $D_{q,p_0,p_1}$ holds. Choose $r \in P$ such that \begin{align*} r \le_P p_0 \end{align*} and \begin{align*} r \le_P p_1 \end{align*} and \begin{align*} h \le_Q i(r). \end{align*} Since $h \in H$, this witnesses $r \in G_0$. Hence $G_0$ is downward directed. [guided] The subtle point is that we cannot merely find a common strengthening $r \le_P p_0,p_1$ and hope that $H$ contains a condition below $i(r)$. A generic filter is upward closed toward weaker conditions, so from a condition of $H$ above or compatible with $i(r)$ we do not get membership in $G_0$. Instead, we build a dense set which directly forces $H$ to supply a condition below the image of a common $P$-strengthening. Let $p_0,p_1 \in G_0$. Choose $q_0,q_1 \in H$ such that $q_0 \le_Q i(p_0)$ and $q_1 \le_Q i(p_1)$. Since $H$ is downward directed, choose $q \in H$ such that $q \le_Q q_0$ and $q \le_Q q_1$. Therefore \begin{align*} q \le_Q i(p_0) \end{align*} and \begin{align*} q \le_Q i(p_1). \end{align*} The condition $q$ is the part of $H$ that will rule out the incompatible branch of the dense set below. Define \begin{align*} D_{q,p_0,p_1} := \{s \in Q : s \perp_Q q \text{ or } \exists r \in P \text{ such that } r \le_P p_0,\ r \le_P p_1,\ s \le_Q q,\text{ and } s \le_Q i(r)\}. \end{align*} This set belongs to $M$: transitivity of $M$ and $P,Q \in M$ imply that $p_0,p_1 \in M$ and $q \in M$, and Separation in $M$ applies to the displayed definition using only the parameters $P$, $Q$, $i$, $p_0$, $p_1$, and $q$. We verify that $D_{q,p_0,p_1}$ is dense in $Q$. Let $s_0 \in Q$. If $s_0 \perp_Q q$, then $s_0$ already belongs to $D_{q,p_0,p_1}$. Otherwise $s_0$ is compatible with $q$, so choose $s_1 \in Q$ satisfying \begin{align*} s_1 \le_Q s_0 \end{align*} and \begin{align*} s_1 \le_Q q. \end{align*} Now $s_1 \le_Q q \le_Q i(p_0)$. The lifting clause for the dense embedding gives $a \in P$ with \begin{align*} a \le_P p_0 \end{align*} and \begin{align*} i(a) \le_Q s_1. \end{align*} Since also $s_1 \le_Q q \le_Q i(p_1)$, we have $i(a) \le_Q i(p_1)$. Thus $i(a)$ and $i(p_1)$ are compatible in $Q$. The dense embedding preserves incompatibility, so its contrapositive says that $a$ and $p_1$ are compatible in $P$. Choose $r \in P$ such that \begin{align*} r \le_P a \end{align*} and \begin{align*} r \le_P p_1. \end{align*} Then $r \le_P p_0$ because $r \le_P a \le_P p_0$. Order preservation gives \begin{align*} i(r) \le_Q i(a) \le_Q s_1 \le_Q s_0 \end{align*} and \begin{align*} i(r) \le_Q i(a) \le_Q s_1 \le_Q q. \end{align*} Taking $s := i(r)$, we have found a condition below $s_0$ which lies in the second branch of $D_{q,p_0,p_1}$. Hence $D_{q,p_0,p_1}$ is dense in $Q$. Since $H$ is $Q$-generic over $M$, choose $h \in H \cap D_{q,p_0,p_1}$. The first branch $h \perp_Q q$ cannot occur. Indeed, $h \in H$ and $q \in H$, and downward directedness of $H$ gives $k \in H$ with \begin{align*} k \le_Q h \end{align*} and \begin{align*} k \le_Q q, \end{align*} which contradicts $h \perp_Q q$. Therefore $h$ lies in the second branch of the definition of $D_{q,p_0,p_1}$. Choose $r \in P$ such that \begin{align*} r \le_P p_0 \end{align*} and \begin{align*} r \le_P p_1 \end{align*} and \begin{align*} h \le_Q i(r). \end{align*} Because $h \in H$, this last inequality is exactly the witness required by the definition of $G_0$. Thus $r \in G_0$, and since $r \le_P p_0$ and $r \le_P p_1$, the set $G_0$ is downward directed. [/guided] [/step] [step:Take the upward closure of the base and prove $P$-genericity] Define \begin{align*} G := \{r \in P : \exists p \in G_0 \text{ such that } p \le_P r\}. \end{align*} By definition, $G$ is upward closed. Since $G_0$ is downward directed, $G$ is downward directed as well: if $r_0,r_1 \in G$, choose $p_0,p_1 \in G_0$ with $p_0 \le_P r_0$ and $p_1 \le_P r_1$, then choose $p_2 \in G_0$ with $p_2 \le_P p_0,p_1$, giving $p_2 \le_P r_0,r_1$. Hence $G$ is a filter on $P$. Let $E \subset P$ be dense in $P$ with $E \in M$. Define \begin{align*} E_Q := \{q \in Q : \exists e \in E \text{ such that } q \le_Q i(e)\}. \end{align*} Since $E$, $P$, $Q$, and $i$ belong to $M$, Separation in $M$ gives $E_Q \in M$. We prove that $E_Q$ is dense in $Q$. Let $q_0 \in Q$. By density of the image of $i$, choose $p_0 \in P$ such that \begin{align*} i(p_0) \le_Q q_0. \end{align*} Since $E$ is dense in $P$, choose $e \in E$ such that \begin{align*} e \le_P p_0. \end{align*} Since $i$ is order-preserving, \begin{align*} i(e) \le_Q i(p_0) \le_Q q_0. \end{align*} Thus $i(e) \in E_Q$ and $i(e) \le_Q q_0$, proving that $E_Q$ is dense in $Q$. Since $H$ is $Q$-generic over $M$, choose $q \in H \cap E_Q$. Choose $e \in E$ such that \begin{align*} q \le_Q i(e). \end{align*} Then $e \in G_0 \subset G$. Therefore $G \cap E \neq \varnothing$. Since $E \in M$ was arbitrary, $G$ is $P$-generic over $M$. [/step] [step:Translate names recursively and identify the generic extensions] First suppose $G \subset P$ is $P$-generic over $M$ and $H$ is generated from $G$ by \begin{align*} H = \{q \in Q : \exists p \in G \text{ such that } i(p) \le_Q q\}. \end{align*} We record the membership equivalence \begin{align*} p \in G \quad \Longleftrightarrow \quad i(p) \in H. \end{align*} The forward implication follows from reflexivity of $\le_Q$. For the reverse implication, assume $i(p) \in H$. We first show that $p$ is compatible with every member of $G$. Let $g \in G$. Since $i(g) \in H$ by the forward implication and $i(p) \in H$ by assumption, downward directedness of $H$ gives $u \in H$ such that \begin{align*} u \le_Q i(g) \end{align*} and \begin{align*} u \le_Q i(p). \end{align*} Thus $i(g)$ and $i(p)$ are compatible in $Q$. Since $i$ preserves incompatibility, its contrapositive gives that $g$ and $p$ are compatible in $P$. Define \begin{align*} D_p := \{r \in P : r \le_P p \text{ or } r \perp_P p\}. \end{align*} Since $p \in P \in M$ and $M$ is transitive, $p \in M$; hence Separation in $M$ gives $D_p \in M$. The set $D_p$ is dense in $P$: for any $r_0 \in P$, either $r_0 \perp_P p$, in which case $r_0 \in D_p$, or $r_0$ is compatible with $p$, in which case there is $r_1 \in P$ such that $r_1 \le_P r_0$ and $r_1 \le_P p$, so $r_1 \in D_p$ below $r_0$. By $P$-genericity, choose $r \in G \cap D_p$. The alternative $r \perp_P p$ is impossible because the preceding paragraph shows that every member of $G$ is compatible with $p$. Therefore $r \le_P p$. Since $G$ is upward closed and $r \in G$, it follows that $p \in G$. Define the forward translation on $P$-names by recursion: \begin{align*} \widehat{\tau} := \{(\widehat{\sigma}, i(p)) : (\sigma,p) \in \tau\}. \end{align*} Here $\tau$ and $\sigma$ range over $P$-names, and $\widehat{\tau}$ is a $Q$-name. The recursion is legitimate in $M$: if $\tau \in M$ is a $P$-name, then all lower-rank translated names belong to $M$ by the induction hypothesis, and Replacement in $M$ together with $i,P,Q \in M$ gives $\widehat{\tau} \in M$. A rank induction on $P$-names proves that $\widehat{\tau}^{\,H} = \tau^G$ for every $P$-name $\tau$. Indeed, assuming the equality for all names of smaller rank than $\tau$, we have \begin{align*} \widehat{\tau}^{\,H} = \{\widehat{\sigma}^{\,H} : \exists p \in P \text{ such that } (\sigma,p) \in \tau \text{ and } i(p) \in H\}. \end{align*} Using the membership equivalence and the induction hypothesis, this becomes \begin{align*} \widehat{\tau}^{\,H} = \{\sigma^G : \exists p \in G \text{ such that } (\sigma,p) \in \tau\} = \tau^G. \end{align*} Therefore $M[G] \subset M[H]$. For the reverse inclusion for this same pair $(G,H)$, use the backward translation on $Q$-names defined recursively by \begin{align*} \rho^\flat := \{(\sigma^\flat,p) : \exists q \in Q \text{ such that } (\sigma,q) \in \rho \text{ and } i(p) \le_Q q\}. \end{align*} As above, this recursion is legitimate in $M$ because $i,P,Q \in M$. A rank induction on $Q$-names, using the defining equivalence $q \in H \Longleftrightarrow \exists p \in G \text{ such that } i(p) \le_Q q$, gives $(\rho^\flat)^G = \rho^H$ for every $Q$-name $\rho$. Hence $M[H] \subset M[G]$, and therefore $M[G]=M[H]$ in the forward construction. Now suppose conversely that $H \subset Q$ is $Q$-generic over $M$ and $G$ is the upward closure of the directed base $G_0$ constructed above. First we prove the preimage equivalence \begin{align*} p \in G \quad \Longleftrightarrow \quad i(p) \in H \end{align*} for every $p \in P$. If $p \in G$, choose $p_0 \in G_0$ such that $p_0 \le_P p$. By the definition of $G_0$, choose $h \in H$ such that $h \le_Q i(p_0)$. Since $i$ is order-preserving, $i(p_0) \le_Q i(p)$, and hence $h \le_Q i(p)$. Upward closure of $H$ gives $i(p) \in H$. Conversely, if $i(p) \in H$, then the same condition $i(p)$ witnesses $p \in G_0$, so $p \in G$. Next we prove that $H$ is exactly the image-generated filter from $G$: \begin{align*} q \in H \quad \Longleftrightarrow \quad \exists p \in G \text{ such that } i(p) \le_Q q. \end{align*} For the reverse implication, if $p \in G$ and $i(p) \le_Q q$, then the preimage equivalence gives $i(p) \in H$, and upward closure of $H$ gives $q \in H$. For the forward implication, fix $q \in H$. Define \begin{align*} E_q := \{p \in P : i(p) \le_Q q \text{ or } i(p) \perp_Q q\}. \end{align*} Since $q \in Q \in M$ and $M$ is transitive, $q \in M$; hence Separation in $M$ gives $E_q \in M$ from the parameters $P$, $Q$, $i$, and $q$. We prove that $E_q$ is dense in $P$. Let $p_0 \in P$. If $i(p_0) \perp_Q q$, then $p_0 \in E_q$. Otherwise choose $s \in Q$ such that \begin{align*} s \le_Q i(p_0) \end{align*} and \begin{align*} s \le_Q q. \end{align*} By the lifting clause for the dense embedding applied to $s \le_Q i(p_0)$, choose $p_1 \in P$ such that \begin{align*} p_1 \le_P p_0 \end{align*} and \begin{align*} i(p_1) \le_Q s. \end{align*} Then $i(p_1) \le_Q q$, so $p_1 \in E_q$. Thus $E_q$ is dense in $P$. Since $G$ is $P$-generic over $M$, choose $p \in G \cap E_q$. The alternative $i(p) \perp_Q q$ is impossible because $p \in G$ implies $i(p) \in H$ by the preimage equivalence, while $q \in H$, and downward directedness of $H$ would give a common strengthening of $i(p)$ and $q$. Therefore $i(p) \le_Q q$, with $p \in G$, proving the forward implication. [guided] The converse direction needs two separate correspondences, and then the name translations use exactly those correspondences. First we prove that $G$ is the preimage of $H$ under $i$: \begin{align*} p \in G \quad \Longleftrightarrow \quad i(p) \in H. \end{align*} If $p \in G$, then by definition of upward closure there is $p_0 \in G_0$ with $p_0 \le_P p$. Since $p_0 \in G_0$, there is $h \in H$ such that $h \le_Q i(p_0)$. Order preservation gives $i(p_0) \le_Q i(p)$, so transitivity gives $h \le_Q i(p)$. Because filters are upward closed toward weaker conditions, $i(p) \in H$. Conversely, if $i(p) \in H$, then $p \in G_0$ by taking the witness $q=i(p)$ in the definition of $G_0$, and hence $p \in G$. Now fix $q \in Q$. We prove that $H$ is generated from $G$ by the image of $i$: \begin{align*} q \in H \quad \Longleftrightarrow \quad \exists p \in G \text{ such that } i(p) \le_Q q. \end{align*} The reverse implication follows directly from the preimage equivalence: if $p \in G$ and $i(p) \le_Q q$, then $i(p) \in H$, and upward closure of $H$ gives $q \in H$. For the forward implication, assume $q \in H$. We need an image condition below $q$, not merely one compatible with $q$. Define \begin{align*} E_q := \{p \in P : i(p) \le_Q q \text{ or } i(p) \perp_Q q\}. \end{align*} The set $E_q$ belongs to $M$ because $q \in Q \in M$, transitivity gives $q \in M$, and Separation in $M$ applies to the displayed definition using the parameters $P$, $Q$, $i$, and $q$. We verify density of $E_q$ in $P$. Let $p_0 \in P$. If $i(p_0) \perp_Q q$, then $p_0 \in E_q$. Otherwise $i(p_0)$ and $q$ are compatible in $Q$, so choose $s \in Q$ such that \begin{align*} s \le_Q i(p_0) \end{align*} and \begin{align*} s \le_Q q. \end{align*} The lifting clause for the dense embedding applies to $s \le_Q i(p_0)$. Therefore there exists $p_1 \in P$ such that \begin{align*} p_1 \le_P p_0 \end{align*} and \begin{align*} i(p_1) \le_Q s. \end{align*} Since $s \le_Q q$, transitivity gives $i(p_1) \le_Q q$, so $p_1 \in E_q$. Thus $E_q$ is dense in $P$. Because $G$ is $P$-generic over $M$, choose $p \in G \cap E_q$. If $i(p) \perp_Q q$, then the preimage equivalence gives $i(p) \in H$, while $q \in H$ by assumption. Downward directedness of $H$ would give $k \in H$ with \begin{align*} k \le_Q i(p) \end{align*} and \begin{align*} k \le_Q q, \end{align*} contradicting $i(p) \perp_Q q$. Hence the incompatible branch is impossible, and the other branch gives $i(p) \le_Q q$. This is the required witness with $p \in G$. Now we translate names. For every $P$-name $\tau$, define the forward translation by rank recursion: \begin{align*} \widehat{\tau} := \{(\widehat{\sigma}, i(p)) : (\sigma,p) \in \tau\}. \end{align*} The object $\widehat{\tau}$ is a $Q$-name in $M$: lower-rank translations are in $M$ by the induction hypothesis, and Replacement in $M$, using the parameters $i$, $P$, and $Q$, forms the displayed set. We prove by rank induction on $P$-names that \begin{align*} \widehat{\tau}^{\,H}=\tau^G. \end{align*} Assume the equality for all $P$-names of smaller rank than $\tau$. By the definition of name valuation, \begin{align*} \widehat{\tau}^{\,H} = \{\widehat{\sigma}^{\,H} : \exists p \in P \text{ such that } (\sigma,p) \in \tau \text{ and } i(p) \in H\}. \end{align*} Using the preimage equivalence $p \in G \Longleftrightarrow i(p) \in H$ and the induction hypothesis $\widehat{\sigma}^{\,H}=\sigma^G$, this becomes \begin{align*} \widehat{\tau}^{\,H} = \{\sigma^G : \exists p \in G \text{ such that } (\sigma,p) \in \tau\} = \tau^G. \end{align*} Therefore every element of $M[G]$ is represented by a $Q$-name evaluated by $H$, so $M[G] \subset M[H]$. For every $Q$-name $\rho$, define the backward translation by rank recursion: \begin{align*} \rho^\flat := \{(\sigma^\flat,p) : \exists q \in Q \text{ such that } (\sigma,q) \in \rho \text{ and } i(p) \le_Q q\}. \end{align*} This is a $P$-name in $M$ by the same rank-recursion argument, now using Separation and Replacement in $M$ to collect all pairs $(\sigma^\flat,p)$ satisfying the displayed formula. We prove by rank induction on $Q$-names that \begin{align*} (\rho^\flat)^G = \rho^H. \end{align*} Assume the equality for all $Q$-names of smaller rank than $\rho$. By valuation of the translated name, \begin{align*} (\rho^\flat)^G = \{(\sigma^\flat)^G : \exists p \in G \text{ and } \exists q \in Q \text{ such that } (\sigma,q) \in \rho \text{ and } i(p) \le_Q q\}. \end{align*} Using the induction hypothesis $(\sigma^\flat)^G=\sigma^H$ and the image-generation equivalence \begin{align*} q \in H \quad \Longleftrightarrow \quad \exists p \in G \text{ such that } i(p) \le_Q q, \end{align*} we obtain \begin{align*} (\rho^\flat)^G = \{\sigma^H : \exists q \in H \text{ such that } (\sigma,q) \in \rho\} = \rho^H. \end{align*} Thus $M[H] \subset M[G]$. Combining the inclusions gives \begin{align*} M[G] = M[H]. \end{align*} [/guided] The recursive name translations now work without invoking any external forcing-equivalence theorem. For every $P$-name $\tau$, the forward translation \begin{align*} \widehat{\tau} := \{(\widehat{\sigma}, i(p)) : (\sigma,p) \in \tau\} \end{align*} is a $Q$-name in $M$ by rank recursion and Replacement in $M$. The rank induction already given for the forward construction applies verbatim, using $p \in G \Longleftrightarrow i(p) \in H$, and gives $\widehat{\tau}^{\,H}=\tau^G$. Thus $M[G] \subset M[H]$. For every $Q$-name $\rho$, define the backward translation \begin{align*} \rho^\flat := \{(\sigma^\flat,p) : \exists q \in Q \text{ such that } (\sigma,q) \in \rho \text{ and } i(p) \le_Q q\}. \end{align*} This is a $P$-name in $M$ by rank recursion, Separation, and Replacement in $M$. A rank induction on $Q$-names, using $q \in H \Longleftrightarrow \exists p \in G \text{ such that } i(p) \le_Q q$, gives $(\rho^\flat)^G = \rho^H$ for every $Q$-name $\rho$. Hence $M[H] \subset M[G]$. Combining the two inclusions gives \begin{align*} M[G] = M[H]. \end{align*} This completes the proof. [/step]