Specializing forcing kills a Suslin tree

Since a Suslin tree is Aronszajn, [F3] makes $P$ ccc; [F2] also verifies that $P$ is nonempty with greatest condition $1_P=\mathrm{\varnothing }$. Therefore [F5] says that forcing with $P$ preserves every ground cardinal and cofinality, including ${\omega }_1^M$.

In $M$ form the name $\dot{f}=\{⟨\check{z},p⟩:p\in P\text{ and }z\in p\}$. For every nonempty $G\subseteq P$, [F8] computes ${\dot{f}}_G=\bigcup G$. If $G$ is $M$-generic, it is a nonempty directed forcing filter and meets every $D_t\in M$; [F4] therefore makes $f={\dot{f}}_G$ a total specializing map $T\to \omega$. Functionality is not merely inferred from notation: if $p,q\in G$ contain values for the same node, directedness gives $r\in G$ extending both graphs, so [F2] forces those values equal; the identical common-extension argument gives unequal values for every comparable distinct pair.

Work in such an extension $M[G]$, which satisfies ZFC by [F10]. By step 1.1, ordinals and ${\omega }_1^M$ are preserved; the old tree set and relation are unchanged, its old countable-level enumerations remain, and its node-height set remains cofinal in ${\omega }_1^M$, so $T$ still has height ${\omega }_1$. A branch $b$ admits an injection into $\omega$ by $f\upharpoonright b$, since comparable distinct nodes have different values. If $b$ were cofinal, its node-height image would be an at most countable cofinal subset of ${\omega }_1$, contradicting [F6]; hence $T$ remains Aronszajn.

The fibers $A_n=f^{-1}(\{n\})$ are antichains and $T={\bigcup }_{n\in \omega }{A}_n$. If every $A_n$ were countable, [F7] would make $T$ countable; then its cofinal node-height image would again be a countable cofinal subset of ${\omega }_1$ by [F6], impossible. Thus some $A_n$ is an uncountable antichain. Consequently $T$ is special, remains Aronszajn, and is not Suslin in $M[G]$. This includes $n=0$ and does not assume in advance that any fiber is nonempty.

The preceding conclusions are forced internally. Concretely, below every $p\in P$, each $D_t\cap P\downarrow p$ is dense; a member carrying $(t,n)$ has the corresponding check-pair as a coefficient of $\dot{f}$, while common refinements give exactly the functionality and specialization calculations of step 1.2. Dense truth and persistence in [F9] therefore force the total-specialization clauses below every condition. The ccc preservation theorem and the ZFC argument of steps 2.1-3.1 then force preservation and non-Suslinity. Hence $1_P$ forces the assertion in the Statement. This uses internal names and forcing only; no $M$-generic over the universe was postulated.