= Mutual genericity for product forcing
If $H=G_0\times G_1$ is generic for <product forcing> over $M$, then $G_1$ is generic over $M[G_0]$. For a name $\dot D$ for a dense <subset> of the second factor, take $p_0\in G_0$ forcing density. Ground-model pairs with first coordinate incompatible with $p_0$, or with first coordinate below $p_0$ forcing the second into $\dot D$, form a dense product <set>. The <existential clause of syntactic forcing> and the membership clause for a <canonical forcing name> give the density witnesses. The product filter meets this <set>, cannot use the incompatible case, and hence its second projection meets $\dot D^{G_0}$.
Back to article page
