The basic Cohen symmetric system

Let $M$ be a transitive model of ZF, let $P=\mathrm{Add}(\omega ,\omega {)}^M$ be the finite partial maps $\omega \times \omega \to 2$ ordered by reverse inclusion as in Cohen, collapse, and Lévy-collapse forcing orders, and let $G_0$ be $M$-generic for $P$. A finite-support permutation $\pi$ of $\omega$ acts by $(\pi p)(\pi n,m)=p(n,m)$. Let $G$ be the resulting group of forcing automorphisms and let $\mathcal{F}$ be generated by $\mathrm{fix}(E)=\{\pi :\pi \upharpoonright E=\mathrm{i}\mathrm{d}\}$ for finite $E\subseteq \omega$. Conjugation sends $\mathrm{fix}(E)$ to $\mathrm{fix}(\pi E)$, so the filter is normal; every condition is supported by the finite projection of its domain to the first coordinate.

Define ${\dot{a}}_n=\{⟨\check{m},p⟩:p(n,m)=1\}$ and the orbit-set name $\dot{A}=\{⟨{\dot{a}}_n,1_P⟩:n\in \omega \}$. Direct calculation gives $\pi {\dot{a}}_n={\dot{a}}_{\pi n}$ and $\pi \dot{A}=\dot{A}$. The theorem Hereditarily symmetric interpretations form a transitive ZF model applies to the displayed $M$, symmetric system, and $M$-generic $G_0$, so $N={\mathrm{H}\mathrm{S}}_{\mathcal{F}}^{G_0}$ is the resulting transitive ZF model. No AC is used in this definition.