Is it known whether every $\omega$-tree with an infinite antichain has an infinite chain in $\mathsf{ZF}$? In this paper by Good and Tree, the following result is mentioned without proof as part of Proposition 6.5:

Each of the following statements imply those beneath it.

*

*The countable union of finite sets is countable.


*Every $\omega$-tree has either (sic) an infinite chain or an infinite antichain.


*Every countable collection of [non-empty] finite sets has a choice function.

By "tree," it is meant "single-rooted tree" in this sense. An $\omega$-tree is a tree of height $\omega$ with all of its levels finite. An antichain is a set of mutually incomparable elements of the tree.
I know that the first and (edited) last statements are equivalent, so that these statements should all be equivalent, according to the paper.
Proving that the first implies the second (with "either" removed) is not difficult. Given an $\omega$-tree $T$, we know $T$ is countably-infinite since each of its countably-infinitely-many non-empty levels is finite. Let $f:\omega\to T$ a bijection. Supposing that $T$ has no infinite antichain, let $A$ be the set of all nodes of $T$ without successor. Since this is readily an antichain, then it is finite, so, put $$m=\max\bigl(\{0\}\cup\{k<\omega:A\cap T_k\ne\emptyset\}\bigr).$$ Let $c_0\in T_{m+1}.$ Given $c_n$ with height greater than $m$, we have by definition of $A$ and $m$ that $c_n$ has a successor, and letting $$c_{n+1}=f\bigl(\min\{k<\omega:c_n<f(k)\}\bigr),$$ the height of $c_{n+1}$ is greater than that of $c_n$, so also greater than $m$. In this way, we recursively define a strictly increasing sequence of points of $T$, so we have an infinite chain, as desired.
Showing that the second statement implied the third, though, was not so straightforward, even with edits.
I began by taking $\{X_n:n<\omega\}$ to be a countably-infinite collection of finite non-empty sets, putting $X=\bigcup_{n<\omega}X_n,$ and letting $$T=\left\{f\in{}^{<\omega}X:\forall n\in\operatorname{dom}(f)\:f(n)\in X_n\right\},$$ where ${}^{<\omega}X$ is the set of all functions $k\to X$ with $k<\omega$. It is readily shown that $\langle T,\subsetneq\rangle$ is an $\omega$-tree. Now, if the tree has an infinite chain $C,$ then $$B=\bigcup_{f\in C}\{g\in T:g\subsetneq f\}$$ is a branch of length $\omega,$ and $f=\bigcup B$ is readily the desired choice function. On the other hand, if the tree has no infinite chain, then it has an infinite antichain, say $A.$ If $A$ happens to be Dedekind-infinite, then there is a countably-infinite antichain $A'\subseteq A,$ and without loss of generality, we may assume that $A'$ has at most one node on each level. Indexing the elements of $A'$ in order of increasing level by $f_n,$ we define $g(X_k)=f_0(k)$ for $k\in\operatorname{dom}(f_0)$ and $g(X_k)=f_{n+1}(k)$ where $k\in\operatorname{dom}(f_{n+1})\setminus\operatorname{dom}(f_n).$ Then $g$ is the desired choice function, and we're done.
If $A$ is infinite and Dedekind-finite, then...what in the world can be done? We need another (even stronger!) Choice principle to conclude that this is impossible, thereby finishing my proof.
[Related question initially posed at Math.SE.]

Edit: Upon further research--in particular, upon inspecting the numerical list of forms from Howard and Rubin's "Consequences of the Axiom of Choice"--I noticed that Howard and Rubin's text actually references Good and Tree's paper. I also see that the first statement above readily implies Form 10A from H & R, the second statement above is Form 216 from H & R, the third statement above is Form 10 from H & R, and I give proof in the comments below that the third statement implies the first, so that the first statement is again equivalent to form 10. Furthermore, I noted that form 10F from H & R is the following:

Every $\omega$-tree has an infinite chain.

This clearly implies the second of G & T's statement above (with "either" removed), and I suspect that it is what was intended by G & T, in the first place. Most notably, according to this site, H & R's text cites that Form 10 is stronger than Form 216, but that it was not known to be strictly stronger. This leads me to suspect (even more strongly) an error on G & T's part. Obviously, if it holds in $\mathsf{ZF}$ that every $\omega$-tree with an infinite antichain must have an infinite chain, then it isn't strictly stronger, but I'm unable to prove this or find any information confirming/denying this. Does anyone know whether this is true, false, or independent of $\mathsf{ZF}$?
P.S.: One thing I was able to find is that Keremidis published a proof (in Mathematica Japonica, Vol. 51, No. 2, pp. 175-178) that Form 9 from H & R (Every Dedekind-finite set is finite.), which is strictly stronger than Forms 10 and 216 in $\mathsf{ZF}$, is equivalent to the following statement:

Every infinite tree has a countably infinite chain or a countably infinite antichain.

This readily implies the second of the statements from G & T (if the "either" is removed), but cannot follow from it unless $\mathsf{ZF}$ is inconsistent.
 A: As shown in the OP, if every countable collection of non-empty finite sets has a choice function, then any countable union of finite sets is countable.
Suppose that the countable union of finite sets is countable, and suppose that $\langle T,\sqsubset\rangle$ is an $\omega$-tree, whence $T$ is countably-infinite (as the countable union of disjoint finite levels). Let $f:\Bbb N\to T$ be a bijection, and use it to induce a well ordering $\prec$ of $T$ given by $x\prec y$ iff $f^{-1}(x)<f^{-1}(y).$ Note that the root $x_0$ of the tree has infinitely-many (not necessarily immediate) $\sqsubset$-successors, so at least one of its immediate successors must also have infinitely-many $\sqsubset$-successors (if not, then $T$ would be a finite union of finite sets, and so finite); let $x_1$ be the $\prec$-least such $\sqsubset$-successor. At a given stage, if $x_n$ has infinitely-many $\sqsubset$-successors, then by a similar argument, it has a $\prec$-least immediate $\sqsubset$-successor which has infinitely-many $\sqsubset$-successors. By recursion on $n,$ the set $\{x_n:n\in\omega\}$ is an infinite chain (in fact, a branch) in $\langle T,\sqsubset\rangle.$
Finally, suppose that every $\omega$-tree has an infinite chain. By the same procedure as used in the OP (attempting to prove that the second statement implied the third), it follows that every countable collection of non-empty finite sets has a choice function. Thus, removing "or an infinite antichain" from the second statement yields three equivalent statements. The third statement is Form 10 in Howard and Rubin's "Consequences of the Axiom of Choice." Form 216 is that every $\omega$-tree has an infinite chain or an infinite antichain.
We show herein that if $\mathsf{ZF}$ + Form 10 is consistent, then so is $\mathsf{ZF}$ + Form 216 + $\neg$Form 10. Thus, unless $\mathsf{ZF}$ is inconsistent, Form 216 is strictly weaker than Form 10 in $\mathsf{ZF},$ based on David Pincus's transferability result$^{[1]}.$ We do so by exploring a permutation model developed by Harry West.
First, we prove the following:
Lemma 1: If $\langle T,\sqsubset\rangle$ is an $\omega$-tree, then it has an infinite antichain if and only if it has an infinite subtree $S$ such that each node of $S$ has a $\sqsubset$-successor that is not in $S.$
Proof: On the one hand, suppose that $A$ is an infinite antichain in $\langle T,\sqsubset\rangle,$ let $S:=\{x\in T:\exists y\in A(x\sqsubset y)\}.$ By definition of antichain, since $\sqsubset$ is irreflexive, then it is immediate that $A\cap S=\emptyset,$ and so each node of $S$ has a $\sqsubset$-successor that is not in $S.$ Note that the root of $\langle T,\sqsubset\rangle$ cannot be an element of $A,$ and is necessarily an element of $S.$ Take any $x\in S,$ so that there is some $y\in A$ such that $x\sqsubset y.$ If $z\in T$ such that $z\sqsubset x,$ then by transitivity, $z\sqsubset y,$ and so $z\in A.$ Thus, $S$ is a subtree of $T.$ Finally, take any $n\in\omega.$ Since a finite union of finite sets is finite, and since the levels of $\langle T,\sqsubset\rangle$ are finite, and since $A$ is infinite, and since all nodes of $\langle T,\sqsubset\rangle,$ have finite height, then $A$ has an element of finite height greater than $n,$ which necessarily has an immediate $\sqsubset$-predecessor in $S$ with height at least $n.$ Thus, $S$ has nodes of arbitrarily large finite height, and so $S$ is infinite, as desired.
On the other hand, suppose that $S$ is an infinite subtree as described. Taking any $y\in T\setminus S,$ the set $\{x\in T:x\sqsubseteq y\}$ is well-ordered by $\sqsubset$ and contains at least one element of $T\setminus S,$ so $\{x\in T\setminus S:x\sqsubseteq y\}$ has a $\sqsubset$-least element, say $m_y.$ The set $A:=\{m_y:y\in T\setminus S\}$ is a non-empty subset of $T,$ and readily each element of $A$ is $\sqsubset$-minimal in $T\setminus S,$ whence $A$ is an antichain in $\langle T,\sqsubset\rangle.$ Take any $n\in\omega.$ Since $S$ is an infinite subtree of an $\omega$-tree, then it has at least one node $s$ of height $n,$ and by hypothesis, there is some $t\in T\setminus S$ with $s\sqsubset t,$ whence $t$ has height at least $n+1.$ Since $m_t$ is the least element of $\{x\in T\setminus S:x\sqsubseteq t\},$ then $s\neq m_t$ (since $s\in S$ and $m_t\notin S$) and $s,m_t\in\{x\in T:x\sqsubseteq t\}.$ Since $S$ is downward-closed with respect to $\sqsubset$ and $m_t\notin S,$ then we cannot have $m_t\sqsubset s,$ but $\{x\in T:x\sqsubseteq t\}$ is well-ordered (and so totally ordered) by $\sqsubset,$ so by trichotomy, $s\sqsubset m_t,$ whence $m_t$ has height greater than $n.$ Since $A$ has elements of arbitrarily large finite height, then $A$ is infinite, as desired. $\Box$

Setup: Let $n\mapsto p_n$ be any enumeration of the positive prime ordinals by $\Bbb Z_{>0}.$ For any $n\in\Bbb Z_{>0}$ and any $\overline i\in\Bbb Z/p_n\Bbb Z,$ we let $a(n,\overline i)$ indicate a unique atom. For each $n\in\Bbb Z_{>0},$ we let $A_n:=\left\{a(n,\overline i):\overline i\in\Bbb Z/p_n\Bbb Z\right\},$ and let $A:=\bigcup_{n\in\Bbb Z_{>0}}A_n.$
Consider the group $G:=\prod_{n\in\Bbb Z_{>0}}(\Bbb Z/p_n\Bbb Z),$ and define the action of $G$ on $A$ by $\pi\bigl(a(n,\overline i)\bigr):=a(n,\overline i+\pi_n).$
Now, we define a set $V_\alpha$ for each ordinal $\alpha$ by transfinite recursion as follows:

*

*$V_0:=A,$


*$V_{\alpha+1}:=V_\alpha\cup\mathcal P(V_\alpha),$ and


*for limit ordinals $\lambda,$ $V_\lambda:=\bigcup_{\alpha<\lambda}V_\alpha.$
The class $\mathscr{V}$ given by the union of all $V_\alpha$ is a model of $\mathsf{ZFA}.$ The rank of an element $x\in\mathscr V$ is the least ordinal $\alpha$ such that $x\in V_\alpha.$ Thus, the atoms are precisely the elements of rank $0.$ We extend the action of $G$ on $A$ to all of $\mathscr{V}$ by $\pi(x):=\{\pi(y):y\in x\},$ using recursion on the rank of $x.$
A few quick facts are readily seen:

*

*$\pi(\emptyset)=\emptyset$ for any $\pi\in G.$ By recursion on rank, we see that for any ordinal $\alpha,$ $\pi(\alpha)=\alpha.$


*More generally, if $x\in\mathscr{V}\setminus A$ and the transitive closure of $x$ is disjoint from $A,$ then $\pi(x)=x$ for all $\pi\in G.$ We call such $x$ "pure sets," and the class of all pure sets "the kernel of $G.$" This class is readily identical to the class of all hereditary sets in the standard cumulative heirarchy of $\mathsf{ZF}.$


*For any $\pi\in G,$ the map $x\mapsto\pi(x)$ is a permutation $\mathscr{V}\to\mathscr{V}.$
Next, consider the set $\mathcal{S}$ of subsets of $\Bbb Z_{>0}$ of zero upper density. The following facts are readily shown:

*

*$\emptyset\in\mathcal S.$


*If $S\in\mathcal S$ and $S'\subseteq S,$ then $S'\in\mathcal S.$


*If $S,S'\in\mathcal S,$ then $S\cup S'\in\mathcal S.$


*If $A\subset\Bbb Z_{>0}$ and $|A|<\aleph_0,$ then $A\in\mathcal S.$
Given any $S\in\mathcal S,$ define $$G(S):=\{\pi\in G:\forall n\in S,\pi_n=\overline 0\},$$ which is readily a subgroup of $G,$ and let $$\mathcal F:=\{H<G:\exists S\in\mathcal S(G(S)\subseteq H)\}.$$ Noting that $G(\emptyset)=G,$ we readily have $G\in\mathcal F$ by the first fact about $\mathcal S$ above. Immediately, if $H\in\mathcal F$ and $K$ is a subgroup of $G$ such that $H\subseteq K,$ then $K\in\mathcal F.$ Given $H,H'\in\mathcal F,$ there exist $S,S'\in\mathcal F$ such that $G(S)\subseteq H$ and $G(S')\subseteq H',$ so noting that $G(S\cup S')=G(S)\cap G(S')\subseteq H\cap H',$ then by the third fact about $\mathcal S$ above, $H\cap H'\in\mathcal F.$ Since $G$ is abelian, then for any $\pi\in G$ and any $H\in\mathcal F,$ $\pi H\pi^{-1}=H\in\mathcal F.$ Finally, letting $a\in A,$ there is a unique $n\in\Bbb Z_{>0}$ such that $a\in A_n,$ and noting that $G(\{n\})=\{\pi\in G:\pi(a)=a\},$ then by the fourth fact about $\mathcal S$ above, $\{\pi\in G:\pi(a)=a\}\in\mathcal F.$ Thus, $\mathcal F$ is a normal filter on $G$ (see p. 46 of Thomas Jech's The Axiom of Choice).
Now, given any $x\in\mathscr{V},$ we say that $x$ is "symmetric" if $\{\pi\in G:\pi(x)=x\}\in\mathcal F,$ and "hereditarily symmetric" if $x$ is symmetric and all elements of $x$ are hereditarily symmetric (by recursion on rank, hereditary symmetry is well-defined). Let $\mathscr{N}$ be the class of all hereditarily symmetric elements of $\mathscr{V}.$ By Theorem 4.1 from Jech, $\mathscr{N}$ is a transitive model of $\mathsf{ZFA}$ containing all elements of the kernel of $G$ as well as all elements of $A.$

Claim A: Form 10 fails to hold in $\mathscr N.$
Proof: To show that Form 10 fails, we show that $A$ is not countable in $\mathscr{N},$ but that $\{A_n:n\in\Bbb Z_{>0}\}$ is countable and each $A_n$ is finite in $\mathscr{N}.$
Note that for any $n\in\Bbb Z_{>0},$ we have by definition of the action of $G$ on $A$ that $\pi(A_n)=A_n$ for all $\pi\in G.$ Since $\omega$ and each of its elements lie in the kernel of $G,$ then the function $f:\omega\to\{A_n:n\in\Bbb Z_{>0}\}$ given by $k\mapsto A_{k+1}$ is thus a bijection and $f\in\mathscr{N},$ so that $\{A_n:n\in\Bbb Z_{>0}\}$ is countable in $\mathscr{N}.$
Fixing any $n\in\Bbb Z_{>0}$, we have for any $\pi\in G(\{n\})$ and any $i\in p_n$ that $\pi(a(n,\overline i))=a(n,\overline i),$ so the function $p_n\to A_n$ given by $i\mapsto a(n,\overline i)$ is both a bijection and an element of $\mathscr{N},$ whence each $A_n$ is finite in $\mathscr{N}.$
Now consider any function $g:\omega\to A$ such that $g\in\mathscr{N}.$ We show that $g$ is not a surjection $\omega\to A,$ and so $A$ is uncountable in $\mathscr{N}.$ Since $g\in\mathscr{N},$ then by definition, there is some $S\in\mathcal S$ such that for all $\pi\in G(S),$ we have $\pi(g)=g.$ Since $S\in\mathcal S,$ then $S\subsetneq\Bbb Z_{>0},$ so there is some $n\in\Bbb Z_{>0}$ such that $n\notin S,$ and so there is some $\pi\in G(S)$ such that $\pi_n\neq \overline 0.$ Take any $\langle k,a\rangle\in g,$ so that $\pi(k)=k$ (since $k$ is in the kernel of $G$), and so $$\langle k,\pi(a)\rangle=\langle \pi(k),\pi(a)\rangle=\pi\bigl(\langle k,a\rangle\bigr)\in\pi(g)=g.$$ Since $g$ is a function and $\langle k,a\rangle,\langle k,\pi(a)\rangle\in g,$ it follows that $\pi(a)=a.$ Since $\pi_n\neq \overline 0,$ it follows that $a\notin A_n.$ Thus, the range of $g$ is disjoint from $A_n,$ so $g:\omega\to A$ is not a surjection, as was to be shown. $\Box$
Lemma 2: Suppose that $S\in\mathcal S$ and $x\in\mathscr{N}$ such that the set $\{\pi(x):\pi\in G(S)\}$ has finite cardinality $m.$ Then there is a $\subseteq$-least finite set $X\subsetneq\Bbb Z_{>0}$ such that for all $\pi\in G(S\cup X),$ $\pi(x)=x.$ In particular, $X=\{k\in\Bbb Z_{\geq 0}:p_k\mid m\},$ and $$m=\prod_{k\in X}p_k.$$
Proof: If $m=1,$ then immediately, $X=\emptyset$ satisfies all of the desired properties, so suppose that $m>1,$ whence $X:=\{k\in\Bbb Z_{>0}:p_k\mid m\}$ is immediately finite and non-empty since $n\mapsto p_n$ is an enumeration of the primes.
By orbit-stabilizer theorem, $\operatorname{Stab}(x):=\{\phi\in G(S):\phi(x)=x\}$ is a (normal) subgroup of $G(S)$ of index $m,$ so the order of each element of $G(S)/\operatorname{Stab}(x)$ divides $m.$ Thus, for any $\pi\in G(S),$ $m\pi+\operatorname{Stab}(x)=\operatorname{Stab}(x),$ meaning that $m\pi\in\operatorname{Stab}(x),$ and so $mG(S)\subseteq\operatorname{Stab}(x).$ Readily, $mG(S)$ is a subgroup of $G,$ so a subgroup of $\operatorname{Stab}(x),$ and since $G$ is abelian, then $mG(S)$ is a normal subgroup of $\operatorname{Stab}(x).$ Thus, $$[G(S):mG(S)]=[G(S):\operatorname{Stab}(x)][\operatorname{Stab}(x):mG(S)]=m\cdot[\operatorname{Stab}(x):mG(S)]\ge m.$$
Take any $\pi\in G(S),$ meaning that $\pi\in G$ and that $\pi_n=\overline 0$ for all $n\in S,$ and consider $m\pi.$ Given any $n\in X,$ we have by definition that $p_n\mid m,$ so $p_n\mid m\pi_n\equiv_{p_n}(m\pi)_n,$ and so $(m\pi)_n=\overline 0.$ Also, for $n\in S$ we immediately have $(m\pi)_n\equiv_{p_n}m\pi_n=m\overline 0=\overline 0.$ Hence, $(m\pi)_n=\overline 0$ for all $n\in S\cup X,$ meaning that $m\pi\in G(S\cup X),$ whence $mG(S)\subseteq G(S\cup X).$
On the other hand, suppose $\phi\in G(S\cup X)$ with $\phi$ not the identity element, and take any $n\in\Bbb Z_{>0}\setminus (S\cup X)$ such that $\phi_n\neq \overline 0.$ Since $n\notin X,$ then $p_n\not\mid m,$ and so there exists $k\in\Bbb Z_{>0}$ such that $p_n\mid(mk-1).$ Let $k_n$ be the least such $k,$ so since $\phi_n\neq \overline 0$ and $k_n$ is coprime with $p_n,$ then $k_n\phi_n\neq\overline 0.$
We show that $\phi\in mG(S),$ so that $G(S\cup X)=mG(S)$ by double-inclusion. Define $\pi\in G$ as follows. For each $n\in(\Bbb Z_{>0}\setminus S)\cap(\Bbb Z_{>0}\setminus X)$ such that $\phi_n\neq \overline 0,$ let $\pi_n=k_n\phi_n\neq\overline 0.$ For each $n\in(\Bbb Z_{>0}\setminus S)\cap(\Bbb Z_{>0}\setminus X)$ such that $\phi_n=\overline 0,$ let $\pi_n=\overline 0.$ For each $n\in S,$ let $\pi_n=\overline 0,$ so that $\pi\in G(S).$ For each $n\in(\Bbb Z_{>0}\setminus S)\cap X,$ let $\pi_n=\overline 1.$
Note that $\bigl\{S,(\Bbb Z_{>0}\setminus S)\cap X,(\Bbb Z_{>0}\setminus S)\cap(\Bbb Z_{>0}\setminus X)\bigr\}$ is a partition of $\Bbb Z_{>0},$ whence $\pi\in G$ is well-defined. As noted above, $\pi\in G(S);$ furthermore, $(m\pi)_n=\overline 0=\phi_n$ for all $n\in S,$ since $\phi\in G(S\cup X)\subseteq G(S).$ Now, for $n\in (\Bbb Z_{>0}\setminus S)\cap X,$ we have that $p_n\mid m,$ so $(m\pi)_n=m\pi_n=\overline 0,$ and since $\phi\in G(S\cup X)\subseteq G(X)$ and $n\in X,$ then $(m\pi)_n=\overline 0=\phi_n.$ For $n\in\Bbb Z_{>0}\setminus(S\cup X),$ we have that $\pi_n=\overline 0$ iff $\phi_n=\overline 0,$ so for $n\in\Bbb Z_{>0}\setminus(S\cup X)$ such that $\pi_n=\overline 0,$ we have that $m\pi_n=\overline 0,$ whence $(m\pi)_n=\phi_n.$ Finally, if $n\in\Bbb Z_{>0}\setminus(S\cup X)$ such that $\pi_n\neq \overline 0,$ then $\pi_n=k_n\phi_n.$ Since $p_n\not\mid m$ by definition of $X,$ this is equivalent to $m\pi_n=mk_n\phi_n\,$ so since $p_n\mid(mk_n-1),$ this is equivalent to $m\pi_n=\phi_n,$ whence $(m\pi)_n=\phi_n.$ Thus, $m\pi=\phi,$ so $\phi\in mG(S),$ so $G(S\cup X)\subseteq mG(S),$ and so $mG(S)=G(S\cup X)$ by double inclusion.
By definition, $G(S)\cong\prod_{n\in \Bbb Z_{>0}\setminus S}(\Bbb Z/p_n\Bbb Z),$ so $$\begin{eqnarray*}mG(S) & \cong & \left(\prod_{n\in (\Bbb Z_{>0}\setminus S)\cap X}m(\Bbb Z/p_n\Bbb Z)\right)\times\left(\prod_{n\in \Bbb Z_{>0}\setminus(S\cup X)}m(\Bbb Z/p_n\Bbb Z)\right)\\ & = & \left(\prod_{n\in (\Bbb Z_{>0}\setminus S)\cap X}0(\Bbb Z/p_n\Bbb Z)\right)\times\left(\prod_{n\in \Bbb Z_{>0}\setminus(S\cup X)}(\Bbb Z/p_n\Bbb Z)\right).\end{eqnarray*}$$ Hence, $$G(S)/mG(S)\cong\prod_{n\in (\Bbb Z_{>0}\setminus S)\cap X}(\Bbb Z/p_n\Bbb Z),$$ so $$[G(S):mG(S)]:=\bigl|G(S)/mG(S)\bigr|=\prod_{n\in (\Bbb Z_{>0}\setminus S)\cap X}\bigl|\Bbb Z/p_n\Bbb Z\bigr|=\prod_{n\in (\Bbb Z_{>0}\setminus S)\cap X}p_n,$$ so $[G(S):mG(S)]\mid m$ by definition of $X.$ Hence, $m\leq[G(S):mG(S)]\leq m,$ so $[G(S):mG(S)]=m.$ Moreover, since $\prod_{n\in X}p_n$ divides $m$ by definition of $X,$ and since $m=\prod_{n\in (\Bbb Z_{>0}\setminus S)\cap X}p_n,$ then $X\subseteq(\Bbb Z_{>0}\setminus S)\cap X,$ whence $X\subseteq \Bbb Z_{>0}\setminus S,$ so that $S\cap X=\emptyset,$ and $m=\prod_{n\in X}p_n.$
Since $m=[G(S):mG(S)]=m\cdot[\operatorname{Stab}(x):mG(S)],$ then $[\operatorname{Stab}(x):mG(S)]=1,$ so $G(S\cup X)=mG(S)=\operatorname{Stab}(x).$
Finally, suppose that $Y\subseteq\Bbb N$ such that $G(S\cup Y)$ fixes $x,$ whence $G(S\cup Y)$ is a subgroup of $\operatorname{Stab}(x)=G(S\cup X),$ and so $G(S\cup Y)\subseteq G(S\cup X).$ Take any $n\in X$ and any $\pi\in G(S\cup Y),$ so since $\pi\in G(S\cup X)=G(S)\cap G(X),$ then $\pi_n=0.$ Since $\pi\in G(S\cup Y)$ was arbitrary, then $n\in S\cup Y,$ but $n\in X$ and $S\cap X=\emptyset,$ so $n\in Y.$ Thus, $X\subseteq Y,$ as desired. $\Box$
Lemma 3: Suppose that $\langle T,\sqsubset\rangle\in\mathscr V$ and that there is some $S\in\mathcal S$ such that $G(S)$ fixes $\langle T,\sqsubset\rangle.$ Then for each $\pi\in G(S),$ $\pi\restriction_T$ is a tree automorphism of $\langle T,\sqsubset\rangle.$
Proof: Since each such $\pi$ fixes $\langle T,\sqsubset\rangle,$ then each such $\pi$ fixes $T$ and $\sqsubset.$
Fix any $\pi\in G(S).$ Since $\pi$ is a permutation of $\mathscr{V}$ and $\pi(T)=T,$ then $\pi\restriction_T:T\to T$ is a bijection. For any $\bigl\langle a,b\bigr\rangle\in\;\sqsubset$, we have $\bigl\langle\pi(a),\pi(b)\bigr\rangle=\pi\bigl(\langle a,b\rangle\bigr)\in\pi(\sqsubset)=\;\sqsubset.$ Analogously, for any $\bigl\langle c,d\bigr\rangle\in\;\sqsubset$, we have $\langle\pi^{-1}(c),\pi^{-1}(d)\rangle\in\;\sqsubset,$ so if $\bigl\langle\pi(a),\pi(b)\bigr\rangle\in\;\sqsubset,$ then letting $c=\pi(a)$ and $d=\pi(b),$ we have $\langle a,b\rangle\in\;\sqsubset.$ Therefore, $\pi\restriction_T$ is an order automorphism of $\langle T,\sqsubset\rangle,$ as desired. $\Box$
Lemma 4: Suppose $X$ is an infinite subset of $\Bbb Z_{\geq 0}.$ Then $X$ has an infinite subset $S$ of zero upper density.
Proof: For each $n\in\Bbb Z_{\geq 0},$ we have $n^2\in\Bbb Z_{\geq 0}.$
Clearly, $0^2=0$ isn't an upper bound of $X,$ so let $s_0:=\min\{k\in X:k>0\}.$ Given $s_n,$ we have that $\max\bigl\{(n+1)^2, s_n\bigr\}$ is not an upper bound of $X,$ so let $s_{n+1}:=\min\left\{k\in X:k>(n+1)^2,k>s_n\right\}.$ By recursion, $n\mapsto s_n$ is an increasing map $\Bbb Z_{\geq 0}\to X,$ so $S:=\{s_n:n\in\Bbb Z_{\geq 0}\}$ is an infinite subset of $X.$ Moreover, $s_n>n^2$ for all $n\in\Bbb Z_{\geq 0},$ so the upper density of $S$ is $$\limsup_{n\to\infty}\frac{n}{s_n}\leq\limsup_{n\to\infty}\frac{n}{n^2+1}=0.$$ Since upper density is always a nonnegative number, then $S$ has zero upper density, as desired. $\Box$
Lemma 5: Suppose that $\langle T,\sqsubset\rangle\in\mathscr N$ is an $\omega$-tree, that $T'$ is a subtree of $\langle T,\sqsubset\rangle,$ and that $A$ is the set of $\sqsubset$-minimal elements of $T\setminus T'.$ Then $A\in\mathscr N$ if and only if $T'\in\mathscr N.$
Proof: Since $T\in\mathscr N,$ then $T\subset\mathscr N,$ so $A\subseteq\mathscr N$ and $T'\subseteq\mathscr N.$ It remains to show that $A$ is symmetric iff $T'$ is symmetric.
Since $\langle T,\sqsubset\rangle\in\mathscr N,$ then there is some $S_T\in\mathcal S$ such that each $\pi\in G(S_T)$ fixes $\langle T,\sqsubset\rangle.$ Given any $S\in\mathcal S,$ we have that $S_T\cup S\in\mathcal S,$ whence $G(S_T\cup S)=G(S_T)\cap G(S)$ is a subgroup of $G(S_T),$ and so each $\pi\in G(S_T\cup S)$ fixes $\langle T,\sqsubset\rangle.$ Any such $\pi$ fixes $T'$ iff it fixes $T\setminus T',$ since $\pi\restriction_T:T\to T$ is a bijection. Further, by Lemma 3, any such $\pi$ maps $\sqsubset$-minimal elements of $T'$--that is, elements of $A$--to $\sqsubset$-minimal elements of $\pi(T').$
If such a $\pi$ fixes $T',$ then $\pi(T')=T',$ so by the above, $\pi(A)=A.$ On the other hand, suppose that $\pi(A)=A$ for some such $\pi.$ Since $T'$ is a subtree of $\langle T,\sqsubset\rangle,$ then $T'$ is non-empty and has the root of $T$ as an element. In addition, every element of $A$ is of finite height, so since the root of $T$ is not in $A,$ then each element of $A$ is a successor of some (unique) element of $T'.$ Put another way, each element of $T'$ is a predecessor of an element of $A$, so by Lemma 3, is necessarily fixed by $\pi.$ The Lemma then follows. $\Box$
Claim B: Suppose that Form 10 holds in $\mathscr V.$ Then Form 216 holds in $\mathscr{N}.$
Proof: Take any $\omega$-tree $\langle T,\sqsubset\rangle\in\mathscr V,$ and suppose that there is some $S_T\in\mathcal S$ such that $G(S_T)$ fixes $\langle T,\sqsubset\rangle,$ so that $\langle T,\sqsubset\rangle\in\mathscr N.$ Further suppose that if $f\in\mathscr V$ such that $f:\langle\omega,\in\rangle\to\langle T,\sqsubset\rangle$ is an embedding, then $f\notin\mathscr N.$ To show that Form 216 holds in $\mathscr N,$ it suffices (by Lemmas 1 and 5) to show that $\langle T,\sqsubset\rangle$ has an infinite subtree $T'$, every node of which is bounded above by some element of $T\setminus T'.$
Since Form 10 holds in $\mathscr V,$ then there exists $f:\omega\to T$ such that for all $n\in\omega,$ $f(n)\sqsubset f(n+1).$ Note that we may assume without loss of generality that for each $n\in\omega,$ $f(n)$ is on the $n$th level of $\langle T,\sqsubset\rangle$--that is, that the image of $f$ is an infinite branch of $\langle T,\sqsubset\rangle$--since if not, then the downward closure of the image of $f$ is such an infinite branch, and we may enumerate the elements of that branch in increasing order as desired. Let $x_n:=f(n)$ for each $n\in\omega.$ By Lemma 3, we have that $G(S_T)$ fixes each level of $\langle T,\sqsubset\rangle,$ and since each such level has finite cardinality, then for each $n\in\omega,$ $\{\pi(x_n):\pi\in G(S_T)\}$ has finite cardinality, so by Lemma 2, we can let $X_n$ be the unique, minimal, finite subset $X\subseteq \Bbb Z_{>0}$ such that for all $\pi\in G(S_T\cup X),$ $\pi(x_n)=x_n.$
Given $m,n\in\omega$ with $m<n,$ take any $\pi\in G(S_T\cup X_n).$ Since $\bigl\langle\pi(x_m),x_n\bigr\rangle=\bigl\langle\pi(x_m),\pi(x_n)\bigr\rangle=\pi\bigl(\langle x_m,x_n\rangle\bigr)\in\pi(\sqsubset)=\;\sqsubset,$ then both $x_m$ and $\pi(x_m)$ are predecessors of $x_n$ on the $m$th level of $\langle T,\sqsubset\rangle,$ but the set of predecessors of $x_n$ is well-ordered, whence $\pi(x_m)=x_m.$ Thus, $\pi\in G(S_T\cup X_m),$ so $G(S_T\cup X_n)\subseteq G(S_T\cup X_m),$ so $S_T\cup X_m\subseteq S_T\cup X_n,$ and so $X_m\subseteq X_n$ since $S_T\cap X_m=S_T\cap X_n=\emptyset.$
Let $X':=\bigcup_{n\in\omega}X_n,$ so $S_T\cap X'=\emptyset,$ and for each $n\in\omega$ and each $\pi\in G(S_T\cup X')$ we have $\pi(x_n)=x_n.$ Since each $x_n\in\mathscr{N},$ and since $f\notin\mathscr{N},$ then $\{x_n:n\in\omega\}\notin\mathscr{N},$ meaning that there exists no $S\in\mathcal{S}$ such that $\pi(x_n)=x_n$ for all $n\in\omega$ and $\pi\in G(S).$ In particular, then, $S_T\cup X'\notin\mathcal{S},$ but $S_T\in\mathcal{S},$ so since $\mathcal{S}$ is closed under finite unions, then $X'\notin\mathcal{S},$ meaning that $X'$ is a subset of $\Bbb Z_{\geq 0}$ with upper density not equal to zero, so that $X'$ is infinite.
By Lemma 4, $X'$ has an infinite subset $S'$ of zero upper density, so that $S_T\cup S'\in\mathcal S,$ and since $S'\subseteq X'$ and $S_T\cap X'=\emptyset,$ then $S_T\cap S'=\emptyset.$ Since $S_T\subseteq S_T\cup S',$ then $G(S_T\cup S')\subseteq G(S_T),$ and so each $\pi\in G(S_T\cup S')$ fixes $\langle T,\sqsubset\rangle.$
Let $T':=\bigl\{t\in T:t=\pi(x_n)\text{ for some }n\in\omega,\pi\in G(S_T\cup S')\bigr\}.$ Letting $\iota$ indicate the identity of $G,$ we have $\iota\in G(S_T\cup S'),$ and so for each $n\in\omega,$ we have $x_n=\iota(x_n)\in T',$ whence $T'$ is infinite. Taking any $t\in T',$ and any $s\in T$ such that $s\sqsubset t,$ we have by definition of $T'$ that $t=\pi(x_n)$ for some $n\in\omega$ and some $\pi\in G(S_T\cup S').$ Since $x_n$ is on the $n$th level of $\langle T,\sqsubset\rangle$ by Lemma 3, then so is $t,$ and since $s\sqsubset t,$ then $s$ is on the $m$th level of $\langle T,\sqsubset\rangle$ for some $m\in\omega$ with $m<n.$ On the other hand, we have by Lemma 3 that $\pi(x_m)\sqsubset\pi(x_n)=t$ since $x_m\sqsubset x_n,$ so since $t$ has a unique predecessor on the $m$th level of $\langle T,\sqsubset\rangle,$ then $s=\pi(x_m)\in T'.$ Thus, $T'$ is downward closed with respect to $\sqsubset,$ and so $T'$ is a(n infinite) subtree of of $\langle T,\sqsubset\rangle.$ It remains to show that $T'\in\mathscr N$ and that each node of $T'$ has a $\sqsubset$-successor that is not in $T'.$
Take any $t\in T'$ and any $\phi\in G(S_T\cup S').$ By definition of $T',$ there is some $\pi\in G(S_T\cup S')$ and some $n\in\omega$ such that $t=\pi(x_n).$ Then $\phi(t)=\phi\bigl(\pi(x_n)\bigr)=(\phi\circ\pi)(x_n),$ and since $\phi\circ\pi\in G(S_T\cup S'),$ then $\phi(t)\in T'.$ Since $S_T\cup S'\in\mathcal S,$ then $T'$ is symmetric. Moreover, since $T\in\mathscr N,$ then each element of $T$ (and so each element of $T'\subseteq T$) is symmetric, whence $T'\in\mathscr N.$
Now, take any $i\in\omega,$ so that $x_i\in T'.$ It suffices to show that there is some $y\in T\setminus T'$ such that $x_i\sqsubset y.$ Recall that $X_i$ is finite, and that for all $j\in\omega$ with $i<j,$ we have $X_i\subseteq X_j.$ Since $S'$ is infinite, then there is some $n\in S'\subseteq X'=\bigcup_{j\in\omega}X_j,$ such that $n\notin X_i,$ and so for sufficiently large $j\in \omega,$ $n\in X_j\setminus X_i,$ and so $n\in(X_j\setminus X_i)\cap S'.$ Fix any such $n,$ and define $\phi\in G$ by $$\phi_k:=\begin{cases}\overline 1 & k=n\\\overline 0 & \text{otherwise.}\end{cases}$$ Immediately, we have that $\phi\in G(S_T)$ and that $\phi\notin G(S_T\cup S').$ Consequently, $\phi(x_j)\in T\setminus T'.$
Since $n\in X_j$ and $S_T\cap X_j=\emptyset,$ then $n\notin S_T.$ Moreover,since $n\in X_j\setminus X_i,$ then $n\notin X_i,$ and so $n\notin S_T\cup X_i.$ Thus, by Lemma 2, we have that $\phi\in G(S_T\cup X_i)\setminus G(S_T\cup X_j).$ In particular, this means that $\phi(x_i)=x_i.$ Since $x_i\sqsubset x_j$ by Lemma 3, then (again by Lemma 3) we have $x_i=\phi(x_i)\sqsubset\phi(x_j).$ Since $x_i\in T'$ and $\phi(x_j)\in T\setminus T',$ then the proof is complete. $\Box$

[1] Zermelo-Fraenkel Consistency Results by Fraenkel-Mostowski Methods, David Pincus, The Journal of Symbolic Logic, Vol. 37, No. 4 (Dec., 1972), pp. 721-743
