Countable-support iterations preserve properness

Fix $\alpha \le \delta$ and a sufficiently large well-ordered $H_{\theta }$ containing the full iteration and $\alpha$. The countable elementary submodels containing these fixed parameters form a club. Fix one such $M$ and $p\in P_{\alpha }\cap M$; then $P_{\alpha }$ and the restricted iteration belong to $M$. At the trivial stage $P_0$, its unique condition $q_0$ is $(M,P_0)$-generic, and the canonical $P_0$-name $\check{p}$ is forced to belong to $P_{\alpha }\cap M$ with trivial restriction in $G_0$. Apply F1 with $\gamma =0$ to obtain an $(M,P_{\alpha })$-generic $q$ such that $q⊩\check{p}\in {\dot{G}}_{\alpha }$. Hence $q$ and $p$ are compatible: otherwise directedness of a generic filter would make $q$ force $\check{p}\mathrm{\notin }{\dot{G}}_{\alpha }$. Choose a common extension $q^{\mathrm{\prime }}\le q,p$. Predensity below $q$ persists below the stronger condition $q^{\mathrm{\prime }}$, so $q^{\mathrm{\prime }}$ is still $(M,P_{\alpha })$-generic and is now literally below $p$.

Step 1.1 proves the master condition on the club of models containing the full iteration and $\alpha$; F3 converts this to the all-model formulation in F2. Thus $P_{\alpha }$ is proper. Since $\alpha \le \delta$ was arbitrary and the hypotheses restrict to every initial segment, every $P_{\alpha }$, including $P_{\delta }$, is proper. Successor lengths, limits of countable cofinality, and limits where $M\cap \alpha$ is bounded are already the exhaustive cases in F1; no closure of the individual iterands is assumed. AC is used only as recorded in A1 and in the supplier F1.