Size, collapse, and factorization for the PFA iteration

By F1 every stage forces its iterand proper, so F2 makes every $P_{\alpha }$, including $P_{\kappa }$, proper. F3 therefore preserves ${\omega }_1$.

Let $S$ be the set of $\alpha \in [{\omega }_1,\kappa )$ for which $\mathrm{\ell }(\alpha )$ is a valid $P_{\alpha }$-name for $\mathrm{Col}({\omega }_1,\alpha {)}^{V^{P_{\alpha }}}$. We verify the required reflection instead of assuming it. Let $\dot{C}$ be the canonical $P_{\kappa }$-name for $\mathrm{Col}({\omega }_1,\kappa {)}^{V^{P_{\kappa }}}$. The Laver anticipation property gives a sufficiently closed supercompactness embedding $j:V\to M$ with $j(\mathrm{\ell })(\kappa )=\dot{C}$. By elementarity and the recursive definition in F1, the first $\kappa$ stages of $j(P_{\kappa })$ are exactly $P_{\kappa }$, so $M$ recognizes $\dot{C}$ as the required proper collapse name at stage $\kappa$. Hence $\kappa \in j(S)$. If $S$ were bounded below some $\eta <\kappa$, then $j(S)=S\subseteq \eta$, contradicting $\kappa \in j(S)$. Thus $S$ is unbounded.

By F8, $\kappa$ is inaccessible. Inductively, $P_{\alpha }$ and every iterand name for $\alpha <\kappa$ have hereditary size below $\kappa$: F1 places the guesses in $V_{\kappa }$, while F5 bounds the number of countable supports and the countable products of earlier hereditary presentations. At every limit of uncountable cofinality, countable support is bounded, so the inverse-limit carrier equals the direct limit; such limits form a stationary subset of inaccessible $\kappa$. For a $\kappa$-sized family of conditions, F6 thins their countable supports to a delta system. The root is bounded below some $\beta <\kappa$; since $\mathrm{\mid }{P}_{\beta }\mathrm{\mid }<\kappa$, regularity thins again so all root restrictions agree. The union of any two remaining conditions is a condition: below $\beta$ they agree, and beyond the root their supports are disjoint, so at each coordinate monotonicity of the earlier forcing relation preserves the unique tail requirement. Hence the family has two compatible members and $P_{\kappa }$ is $\kappa$-Knaster, in particular $\kappa$-cc. Every countable support is bounded in $\kappa$, so $P_{\kappa }={\bigcup }_{\alpha <\kappa }{P}_{\alpha }$ and $\mathrm{\mid }{P}_{\kappa }\mathrm{\mid }\le \kappa$.

For $\alpha \in S$ the collapse is countably closed and hence proper, so F1 uses it rather than the fallback. Consequently, for every ground cardinal $\mu$ with ${\omega }_1<\mu <\kappa$, a stage $\alpha \in S$ above $\mu$ makes $\mathrm{\mid }\mu \mathrm{\mid }\le {\omega }_1$. Moreover $P_{\alpha +1}$ has at least $\mathrm{\mid }\alpha \mathrm{\mid }$ conditions: the one-point functions in $\mathrm{Col}({\omega }_1,\alpha )$ give that many distinct last-coordinate conditions. Since $S$ is unbounded, $\mathrm{\mid }{P}_{\kappa }\mathrm{\mid }\ge \kappa$, so equality holds in step 2.1. By F7, $\kappa$ itself remains a cardinal, while step 1.1 preserves ${\omega }_1$; therefore the final model has no cardinal strictly between them and forces $\kappa ={\omega }_2$.

Let $j:V\to M$ be supplied by F4 with enough closure to contain the relevant $P_{\kappa }$-name $\dot{Q}$, and suppose $j(\mathrm{\ell })(\kappa )=\dot{Q}$ and $P_{\kappa }$ forces $\dot{Q}$ proper. Since $\mathrm{crit}(j)=\kappa$, elementarity applied to the recursive definition in F1 makes the first $\kappa$ stages of $j(P_{\kappa })$ exactly $P_{\kappa }$. The closure agreement makes $M$ recognize the same forced-properness assertion, so stage $\kappa$ is $\dot{Q}$, not the fallback. Splitting the remaining image iteration after that coordinate gives a tail name $\dot{R}$ and the canonical dense isomorphism $j(P_{\kappa })\simeq P_{\kappa }\ast \dot{Q}\ast \dot{R}$. This proves every clause, with Choice used exactly through A1 and the declared suppliers.