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
