Permutation groups, stabilizers, supports, and normal filters

Let $G$ be a group of permutations of the atom set $A$. Extend $g\in G$ by rank recursion: $ga$ is the given atom permutation and $gx=\{gy:y\in x\}$ for sets. Then $x\in y$ iff $gx\in gy$, and pure sets are fixed.

Put ${\mathrm{sym}}_G(x)=\{g\in G:gx=x\}$ and, for $E\subseteq A$, ${\mathrm{fix}}_G(E)=\{g\in G:g\upharpoonright E={\mathrm{i}\mathrm{d}}_E\}$. A normal filter of subgroups $\mathcal{F}$ is nonempty, upward closed among subgroups, closed under finite intersections and conjugation, and contains ${\mathrm{fix}}_G(\{a\})$ for every atom $a$. A set is $\mathcal{F}$-symmetric when its stabilizer lies in $\mathcal{F}$. A finite $E$ is a support of $x$ when ${\mathrm{fix}}_G(E)\subseteq {\mathrm{sym}}_G(x)$.

Rank induction gives ${\mathrm{sym}}_G(gx)=g{\mathrm{sym}}_G(x)g^{-1}$; hence normality makes symmetry invariant under $G$. Finite unions combine finite supports, and singleton stabilizers make every atom symmetric. No choice principle is used.