Finite specialization of an Aronszajn tree is ccc

By F6 and A1 take an injective family $(p_{\xi }{)}_{\xi <{\omega }_1}$ from $X$. Apply F2 to their finite domains to obtain uncountable $J\subseteq {\omega }_1$ and finite root $r$ with $\mathrm{dom}(p_{\xi })\cap \mathrm{dom}(p_{\eta })=r$ for distinct $\xi ,\eta \in J$. Every such domain contains $r$, since every index in $J$ has a distinct partner.

The set of all maps $r\to \omega$ is countable: enumerate the finite set $r$, start with the one empty tuple, and apply F5 successively to obtain countability of each finite power of $\omega$. Thus F4, with A1, gives an uncountable $K\subseteq J$ and one assignment $v:r\to \omega$ such that $p_{\xi }\upharpoonright r=v$ for every $\xi \in K$; otherwise all these countably many assignment fibers would be countable and their union $J$ would be countable. For $r=\mathrm{\varnothing }$ there is just the empty assignment.

Put $s_{\xi }=\mathrm{dom}(p_{\xi })\setminus r$. Distinct petals are disjoint by step 1.1. If some $s_{\xi }$ is empty, then $p_{\xi }=v\subseteq p_{\eta }$ for any other $\eta \in K$, so $p_{\eta }$ is a common lower bound. Otherwise every petal is nonempty; disjointness makes the petals distinct, so $\{s_{\xi }:\xi \in K\}$ is an uncountable family. Apply F3 to obtain distinct $\xi ,\eta \in K$ whose petals are cross-incomparable.

In the latter situation put $u=p_{\xi }\cup p_{\eta }$. This is a finite function because both assignments agree on $r$, their exact overlap. For comparable distinct nodes $x,y$ in its domain, if both lie in $\mathrm{dom}(p_{\xi })$ or both lie in $\mathrm{dom}(p_{\eta })$, F1 already gives unequal labels. This covers pairs in the root, root-to-petal pairs, and pairs inside one petal. The only remaining possibility is one node in each different petal; step 3.1 makes such nodes incomparable. Hence every required inequality holds and $u$ is a condition below both. In either alternative in step 3.1, $X$ contains two compatible distinct conditions. Consequently no uncountable subset is an antichain, which is ccc by F7.