Solution (source code)

= Solution

Use the displayed family to form the <coherent-injection Aronszajn tree>. A node at level $\beta$ is a restriction $e_\alpha\upharpoonright\beta$ for some $\alpha\ge\beta$. Every such node differs only finitely from $e_\beta$. There are countably many finite <subsets> of the countable domain $\beta$ and countably many assignments of natural-number values to each, so there are only countably many possible finite modifications. Hence each level is countable. It is nonempty because it contains $e_\beta$.

Every shorter restriction of a node is again a node, and its predecessors have order type its domain <ordinal>. Thus this is a <set-theoretic tree> of height $\omega_1$. If it had an uncountable <chain in a partial order>, its domain heights would be unbounded in $\omega_1$, since the levels below any countable height contain only countably many nodes. The union of that <chain in a partial order> would be an <injection> $\omega_1\to\omega$, impossible. Therefore
$$
\boxed{T\text{ is an }\aleph_1\text{-Aronszajn tree}.}
$$
The countable-level proof uses coherence, whereas the no-branch proof uses injectivity; the two features play different roles.