= Solution
Conversely, suppose $p\in G$ and $p\Vdash^*\sigma\in\tau$. The <syntactic forcing relation> says that
$$
D=\{s\leq p:\exists(\rho,r)\in\tau\ (s\leq r\land s\Vdash^*\sigma=\rho)\}
$$
is <dense below a forcing condition> $p$. This is a <set> in $M$ by definability of forcing and <axiom schema of separation>. The <dense-below generic meeting lemma> gives $s\in G\cap D$: augment $D$ by all <incompatible forcing conditions> with $p$ to obtain a globally dense ground-model <set>, and use $p\in G$ to exclude the incompatible part.
Choose the witnessing $(\rho,r)\in\tau$. Since $s\leq r$ and $s\in G$, upward closure gives $r\in G$. The assumed equality truth lemma gives $\sigma^G=\rho^G$, while $r\in G$ gives $\rho^G\in\tau^G$. Combining both directions,
$$
\boxed{\sigma^G\in\tau^G\ \Longleftrightarrow\ \exists p\in G\ (p\Vdash^*\sigma\in\tau).}
$$
This completes the <atomic membership truth lemma for forcing>; no separate assumption of the membership truth lemma was made.
Back to article page
