Every symmetric submodel satisfies Choice

Let $G$ be generic for the basic Cohen forcing over a ZFC ground. By F1 the ambient $M[G]$ satisfies AC. The hereditarily symmetric interpretation $N\subseteq M[G]$, however, contains the invariant set $A$ while every proposed enumeration is moved by a finite-support transposition. By F2, $N\models \mathrm{\neg }\mathrm{A}\mathrm{C}$. Thus $N$ directly refutes the universal statement.

The socks construction sharpens the same failure mode: the indexed pair family is invariant, while a swap outside a proposed choice name's finite support exchanges its selected mate. Hence the family lies in the symmetric model but no choice function does.

The failed inference is therefore $M[G]\models \mathrm{A}\mathrm{C}\Rightarrow N\models \mathrm{A}\mathrm{C}$. Transitivity and satisfaction of ZF pass to the symmetric interpretation by its separate model theorem; AC does not.