An atom-free symmetric model has countable pairs without choice

F1 makes every $P_n$ and the indexed sequence HS, so the symmetric ZF model regards its range as countable pairs. Distinct-coordinate dense sets ensure $R_{n,0}\mathrm{\ne }{R}_{n,1}$.

Suppose $p⊩\dot{c}(n)\in {\dot{P}}_n$ for a supported choice name $\dot{c}$. Choose $n$ outside the finitely many supported pair indices and strengthen to $q\le p$ deciding, say, $\dot{c}(n)={\dot{R}}_{n,0}$. Choose a block swap at $n$ that fixes the support. By additionally permuting unused $j$-coordinates in that block, arrange that $q$ and its image have disjoint moved domains and hence are compatible.

F2 says the image condition forces the same $\dot{c}(n)$ to equal ${\dot{R}}_{n,1}$. A common extension then forces the two distinct mates equal, contradiction. Therefore no choice function exists and F3 fails. The construction is in pure ZF and uses neither the Recorded transfer result nor AC.