Normal Suslin-tree forcing is countably distributive

Conditions $s,t\in P$ are compatible exactly when they are comparable in $T$: a common stronger condition is a common tree extension, which makes $s,t$ comparable by F5, while the deeper member of two comparable nodes is already a common forcing extension. Therefore forcing antichains are exactly tree antichains, and F4 makes $P$ ccc. The unique root supplied by normality makes $P$ nonempty.

Let $D\subseteq P$ be dense open. In the inclusion poset of antichains contained in $D$, the empty antichain is present and the union of every chain is an antichain contained in $D$; F7 gives a maximal member $A_D$. It is maximal as a forcing antichain: for any $p$, density gives $d{\le }_{P}p$ in $D$, and if $d$ were incompatible with every member of $A_D$ it could be adjoined. By step 1.1, $A_D$ is countable. F6 therefore gives ${\alpha }_D<{\omega }_1$ above the heights of all its nodes. If $t$ has height greater than ${\alpha }_D$, maximality makes it compatible with some $a\in A_D$; comparability and the height inequality give $a{<}_{T}t$, hence $t{\le }_{P}a$, and openness puts $t$ in $D$. Thus every node above level ${\alpha }_D$ lies in $D$.

Let $(D_n{)}_{n<\omega }$ be dense open and fix $p\in P$. Apply step 2.1 to each $D_n$, using A1 for the simultaneous maximal-antichain and bound choices. By F6 the countable set $\{{\alpha }_{D_n}:n<\omega \}$ has a bound $\beta <{\omega }_1$. Normality gives a tree extension $t{>}_{T}p$ of height greater than $\beta$. Then $t\in D_n$ for every $n$ by step 2.1, and $t{\le }_{P}p$. Hence ${\bigcap }_n{D}_n$ is dense; it is open because every $D_n$ is open. This is ${\mathrm{\aleph }}_1$-distributivity by F1.

By F9, ${\mathrm{\aleph }}_1$ is regular in the stated ZFC setting. Apply F8 with $\kappa ={\mathrm{\aleph }}_1$ to the separative quotient of $P$; the quotient has the same dense-open distributivity and is forcing equivalent to $P$. Step 3.1 therefore implies that no sequence of ground-model elements of length below ${\mathrm{\aleph }}_1$ is added. By F10 every ordinal of a forcing extension is already a ground-model ordinal, and $\omega <{\mathrm{\aleph }}_1$, so forcing with $P$ adds no new $\omega$-sequence of ordinals. This last assertion comes from F8 and F10, not from the definition of distributivity.