= Solution
This is the forward implication of the <atomic membership truth lemma for forcing>. Suppose $\sigma^G\in\tau^G$. By the <evaluation of a forcing name>, choose $(\rho,r)\in\tau$ with $r\in G$ and $\sigma^G=\rho^G$. The assumed equality truth lemma supplies $s\in G$ with $s\Vdash^*\sigma=\rho$.
Directedness of the <generic filter> gives $p\in G$ with $p\leq r,s$. For every $q\leq p$, monotonicity of the <syntactic forcing relation> gives $q\Vdash^*\sigma=\rho$, and $q\leq r$. Thus $q$ itself witnesses the required membership density below $p$. Hence
$$
\boxed{\sigma^G\in\tau^G\ \Longrightarrow\ \exists p\in G\ (p\Vdash^*\sigma\in\tau).}
$$
Only the equality truth lemma stipulated in the source and the recursive membership clause have been used.
Back to article page
