The Fundamental Theorem of Proper Forcing

Statement

The Fundamental Theorem of Proper Forcing, due to Shelah, states that any countable support iteration of proper forcings is itself proper. This follows from the Proper Iteration Lemma, which states that whenever $(P_\alpha)_{\alpha\leq\kappa}$ is a countable support forcing iteration based on $(Q_\alpha)_{\alpha<\kappa}$ and $N$ is a countable elementary substructure of $H_\lambda$ for a sufficiently large regular cardinal $\lambda$, and $P_\kappa\in N$ and $\alpha\in \kappa\cap N$ and $p$ is $(N,P_\alpha)$-generic and $p$ forces $q\in P_\kappa/G_{P_\alpha}\cap N[G_{P_\alpha}]$, then there exists $r\in P_\kappa$ such that $r$ is $N$-generic and the restriction of $r$ to $P_\alpha$ equals $p$ and $p$ forces the restriction of $r$ to $[\alpha,\kappa)$ to be stronger or equal to $q$.

This version of the Proper Iteration Lemma, in which the name $q$ is not assumed to be in $N$, is due to Schlindwein.

The Proper Iteration Lemma is proved by a fairly straightforward induction on $\kappa$, and the Fundamental Theorem of Proper Forcing follows by taking $\alpha=0$.