Product forcing
= Product forcing
{title2=$\mathbb P\times\mathbb Q$}
The conditions are pairs with coordinatewise extension: $(p,q)\leq(p',q')$ exactly when $p\leq p'$ and $q\leq q'$. The <projection of a product-generic filter> is a pair of factor filters whose <Cartesian product> is the original filter. Each is ground-model generic, and <mutual genericity for product forcing> makes the second generic over the extension by the first.