Every prime ideal on the power set of omega is principal in the tail-flip symmetric model

Suppose for contradiction that $I$ is not principal. For each $k<\omega$, primality applied to $\{k\}\cap (\omega \setminus \{k\})=\mathrm{\varnothing }\in I$ puts one of the two factors in $I$. If $\omega \setminus \{k\}\in I$, downward closure and propriety give $I=\{A\subseteq \omega :k\mathrm{\notin }A\}$, the principal prime ideal generated by that coatom. Thus $\{k\}\in I$ for every $k$, and finite-union closure puts every finite subset of $\omega$ in $I$.

Since $\dot{I}$ is HS, choose $m$ with $H_m\subseteq \mathrm{sym}(\dot{I})$, as in F1. Put $A=S_m$, which belongs to ${\mathsf{F}}_{\mathrm{t}\mathrm{f}}$ because its canonical name is supported by $H_{m+1}$. Since $A\cap (\omega \setminus A)=\mathrm{\varnothing }$, F2 yields either $A\in I$ or $\omega \setminus A\in I$. Let $C$ denote the member selected by these two exhaustive cases, and let $\dot{C}$ be the corresponding canonical name.

By F4 choose a finite $Q$ in the actual generic which forces $\dot{C}\in \dot{I}$. Apply F1 with the support bound $m$, condition $Q$, and coordinate $m$. Its tail automorphism $\pi$ fixes both $Q$ and $\dot{I}$. By F5, $Q=\pi Q$ forces $\pi \dot{C}\in \dot{I}$. Hence both $C$ and $\pi C$ belong to $I$ in the actual extension.

If $C=A$, then F1 gives $\pi C\mathrm{△}(\omega \setminus A)$ finite. If $C=\omega \setminus A$, automorphisms commute with Boolean complementation and F1 gives $\pi C\mathrm{△}A$ finite. Thus in either case $\pi C$ differs finitely from $\omega \setminus C$. By step 1.1 the finite difference belongs to $I$; since $\omega \setminus C\subseteq \pi C\cup (\pi C\mathrm{△}(\omega \setminus C))$, F2 puts $\omega \setminus C$ in $I$.

Step 2.1 gives $C\in I$ and step 3.1 gives its complement in $I$. Finite-union closure then puts $\omega$ in $I$, contradicting propriety. Therefore the assumption in step 1.1 was false, and every prime ideal is principal. Both decisions in step 1.2 lead to the same contradiction, and every finite-modification use was derived from the finite singletons rather than assumed.