König’s lemma for finite levels

Call $t$ good if the heights of nodes above or equal to $t$ are unbounded in $\omega$. The height assumption and F1 imply that every level is nonempty. Some root is good: otherwise, each of the finitely many roots has a finite height bound on its extensions; their maximum bounds all nodes because each node has a root predecessor (or is a root). That contradicts height $\omega$.

If a good node $t$ has height $n$, its immediate successors are precisely its extensions at height $n+1$, by F1. This is a finite set. Each higher extension of $t$ passes through one of these successors. If none were good, the maximum of their finitely many bounds, together with $n+1$, would bound all extensions of $t$. Thus a good immediate successor exists.

Fix a well-order of $T$ using AC. Let $t_0$ be the least good root and send each good node to its least good immediate successor. On the set of good nodes this is a self-map, so recursion gives $t_n$ at height $n$ with $t_n{<}_T{t}_{n+1}$ for every $n$.

The set $B=\{t_n:n<\omega \}$ is an infinite chain. If $u$ could be added to it, put $n=\mathrm{ht}(u)$. Comparability with $t_n$ and the level-antichain conclusion of F1 force $u=t_n$. Thus $B$ is already maximal, hence is an infinite branch.