Solution (source code)

= Solution

Use the standard <normal set-theoretic tree> convention: a unique root, extensions at every higher level, splitting into at least two successors, and <tree with unique limits>. The small-level and height assumptions already give an $\omega_1$-tree, while the given <tree antichain> condition gives the <countable chain condition for forcing>. We only need to exclude an uncountable branch.

If such a branch existed, its heights would be unbounded, since each initial segment contains only countably many nodes. Fill in predecessors to obtain its node $b_\alpha$ at every level. At each successor step choose a successor $s_\alpha$ of $b_\alpha$ different from $b_{\alpha+1}$. For $\alpha<\beta$, the node $s_\beta$ extends the branch successor $b_{\alpha+1}$, and so is incompatible with $s_\alpha$. Thus $\{s_\alpha:\alpha<\omega_1\}$ is an uncountable <tree antichain>, a contradiction.

Therefore \b[the <set-theoretic tree> is $\aleph_1$-Suslin]. The splitting part of normality matters: a single <chain in a partial order> of height $\omega_1$ would satisfy the <tree antichain> condition but not the conclusion if one used a weakened definition of normality allowing no splitting.