Trees and their bodies

Work in ZF. For a set $E$, use the function sets of The set $B^A$ of all functions $A\to B$ to put $E^{<\omega }={\bigcup }_{n\in \mathbb{N}}{E}^n$. Replacement followed by Union forms this set. Write $\mathrm{\varnothing }$ for the empty word, $\mathrm{\mid }s\mathrm{\mid }$ for the domain length of $s$, and $s^{⌢}e$ for appending $e\in E$.

A tree on $E$ is a subset $T\subseteq E^{<\omega }$ such that $s\upharpoonright m\in T$ whenever $s\in T$ and $m\le \mathrm{\mid }s\mathrm{\mid }$. The empty tree is permitted. Every nonempty tree contains $\mathrm{\varnothing }$. Its body is

$[T]=\{x\in E^{\mathbb{N}}:(\mathrm{\forall }n\in \mathbb{N})x\upharpoonright n\in T\}\mathrm{.}$

A tree is pruned when every node has a proper extension in $T$. Equivalently, every $s\in T$ has a child $s^{⌢}e\in T$: restrict a proper extension to length $\mathrm{\mid }s\mathrm{\mid }+1$ for the forward implication; a child itself is a proper extension for the reverse implication. This is not a claim that branches exist through nodes of arbitrary-alphabet pruned trees in ZF.

The empty tree is vacuously pruned and has empty body, because every branch would require its empty prefix to belong to the tree. The root-only tree $\{\mathrm{\varnothing }\}$ has empty body and is not pruned. If $E=\mathrm{\varnothing }$, these are the only two trees, since $E^0=\{\mathrm{\varnothing }\}$ and $E^n=\mathrm{\varnothing }$ for $n>0$.