MA(aleph-one) eliminates Suslin trees

Suppose toward a contradiction that $T$ is a Suslin tree. Every level $T_{\alpha }$ is nonempty: height ${\omega }_1$ gives a node above any prescribed $\alpha$, and its predecessor well-order has a node of height $\alpha$. By AC choose $t_{\alpha }\in T_{\alpha }$ and an injection $e_{\alpha }:T_{\alpha }\to \omega$ for every $\alpha <{\omega }_1$. Then $\alpha \mapsto t_{\alpha }$ injects ${\omega }_1$ into $T$, while $t\mapsto (\mathrm{ht}(t),e_{\mathrm{ht}(t)}(t))$ injects $T$ into ${\omega }_1\times \omega$. F7 gives $\mathrm{\mid }{\omega }_1\times \omega \mathrm{\mid }={\mathrm{\aleph }}_1$, and F8 applied to the two displayed injections gives $\mathrm{\mid }T\mathrm{\mid }={\mathrm{\aleph }}_1$.

Form $P(T)$. It is nonempty because it contains the empty condition by F2, and it is ccc by F3 because $T$ is Aronszajn. The family $\mathcal{D}=\{D_t:t\in T\}$ has size at most $\mathrm{\mid }T\mathrm{\mid }={\mathrm{\aleph }}_1$, and every member is dense by F4. Apply F1 to obtain a filter $G\subseteq P(T)$ meeting every $D_t$. Because $T$ and hence $\mathcal{D}$ are nonempty, this filter is nonempty; its filter directedness has exactly the orientation required by F4.

By F4, $f=\bigcup G$ is a total specializing function $T\to \omega$. For each $n<\omega$, the fiber $A_n=f^{-1}(\{n\})$ is a tree antichain by F5. Since $T$ is Suslin, each $A_n$ is countable, but $T={\bigcup }_{n<\omega }{A}_n$ would then be countable by F6 and A1. This contradicts $\mathrm{\mid }T\mathrm{\mid }={\mathrm{\aleph }}_1$ from step 1.1, because ${\mathrm{\aleph }}_1$ is uncountable.

Therefore no Suslin tree can exist under $\mathrm{M}\mathrm{A}({\mathrm{\aleph }}_1)$. AC is spent at step 1.1 and through the ccc and countable-union suppliers; the dense-set union lemma itself makes no choice.