PFA specializes an Aronszajn tree

Write $T_{\alpha }$ for the $\alpha$th level. Under A1 choose for every $\alpha <{\omega }_1$ an injection $e_{\alpha }:T_{\alpha }\to \omega$. Then $t⟼(\mathrm{ht}(t),e_{\mathrm{ht}(t)}(t))$ injects $T$ into ${\omega }_1\times \omega$. Since $\omega \subseteq {\omega }_1$, F5 bounds this product by $\mathrm{\mid }{\omega }_1\times {\omega }_1\mathrm{\mid }={\omega }_1$. Hence $\mathrm{\mid }T\mathrm{\mid }\le {\omega }_1$, so the family $\mathcal{D}=\{D_t:t\in T\}$ has cardinality at most ${\omega }_1$.

By F3, $P(T)$ is ccc, and F2 makes it proper. It is nonempty because the empty finite function is its greatest condition. By F4 every member of $\mathcal{D}$ is dense. Reindex the distinct members of $\mathcal{D}$ along an ordinal $\lambda \le {\omega }_1$ using step 1.1, and apply F1 to obtain a filter $G\subseteq P(T)$ meeting every $D_t$. Since the family is nonempty, so is $G$; by the filter convention it is downward directed.

Put $f=\bigcup G$. If two conditions in $G$ assign a value to the same node, a common stronger member of $G$ extends both, so the values agree and $f$ is a function. Meeting $D_t$ puts every $t\in T$ in its domain. If $s{<}_{T}t$, choose members of $G$ mentioning $s$ and $t$ and then a common stronger member; its specializing-condition inequality gives $f(s)\mathrm{\ne }f(t)$. Thus $f:T\to \omega$ is total and specializes $T$, exactly as F4 asserts.

The dense family may have repetitions, but step 2.1 reindexes its distinct members and loses no requirement. A one-node level, the label $0$, and the empty initial condition are all allowed by F4. PFA itself chooses the filter; no generic filter over the universe is postulated. AC is used exactly in step 1.1 and in the reindexing in step 2.1, and is retained through A1.