The tail-flip symmetric model refutes BPI

Let $\mathcal{C}=\{A\subseteq \omega :\omega \setminus A\text{ is finite}\}$. It contains $\omega$, excludes $\mathrm{\varnothing }$ because $\omega$ is infinite, is upward closed, and is closed under finite intersections because the complement of an intersection is the finite union of the complements. Hence $\mathcal{C}$ is a proper set filter in the model.

Suppose BPI holds. By F3, the set Ultrafilter Lemma extends $\mathcal{C}$ to an ultrafilter $U$ on $\omega$. For every $k<\omega$, the cofinite set $\omega \setminus \{k\}$ belongs to $U$. But the principal ultrafilter at $k$ omits that set, so $U$ is not principal at any point and is free by F4. This contradicts F1.

Therefore BPI fails. Since F3 proves both directions of the equivalence, the set Ultrafilter Lemma fails as well. The empty-set UFL instance is vacuous, while the explicit nonempty witness is the cofinite filter on $\omega$ from step 1.1.