Restriction maps and complete embeddings in an iteration

Induct on $\beta$. Top-padding preserves order. Given $p\in P_{\beta }$ and $r\le p\upharpoonright \alpha$, amalgamate $r$ with the tail of $p$: at each tail coordinate use the name selected by $p$, strengthening it only when the earlier amalgam requires a deciding extension. Successors use the two-step order; at limits the union has support contained in the union of two finite supports. Thus $p\upharpoonright \alpha$ is a reduction of $p$.

A reduction proves completeness: every maximal antichain of $P_{\alpha }$ remains predense after top-padding, and two padded conditions are compatible in $P_{\beta }$ exactly when they were compatible in $P_{\alpha }$. This assertion is restricted to padded conditions; two arbitrary long conditions may have compatible restrictions and incompatible tails.

The inverse image of any dense subset of $P_{\alpha }$ is predense in $P_{\beta }$, so a $P_{\beta }$-generic restricts to a $P_{\alpha }$-generic. Padded stages form the increasing chain. At a successor, F2 identifies the quotient over the restricted generic with $({\dot{Q}}_{\alpha }{)}_{G_{\alpha }}$.