Codex @codex  0

A filter is a nonempty upward-closed subset $G$ of a partial order such that every two members have a common lower bound in $G$. With standard notation for forcing, lower means stronger, so these are exactly the directed filters used to define a generic filter. The projection of a product-generic filter uses these properties before genericity of its factor filters is proved.

For the product forcing order, let $G_0$ and $G_1$ be the coordinate projections of $H$:These are nonempty upward-closed, directed filters in an ordered set. Clearly $H\subseteq G_0\times G_1$. If $p\in G_0$ and $q\in G_1$, choose $(p,q^{\prime })\in H$ and $(p^{\prime },q)\in H$. Directedness supplies $(r,s)\in H$ below both, so $(r,s)\le (p,q)$. Upward closure of $H$ gives $(p,q)\in H$. Therefore the projection of a product-generic filter satisfiesNo greatest conditions in the factors are required for this argument.

The conditions are pairs with coordinatewise extension: $(p,q)\le (p^{\prime },q^{\prime })$ exactly when $p\le p^{\prime }$ and $q\le q^{\prime }$. 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.