Blass's paired finite-modification classes

Suppose $c\in N$ chooses one member of $f(k)$ for every $k$ in an infinite $K\subseteq \omega$. By F2, a unique definition of $c$ uses only $f$, ordinals, and reals $s_1,\dots ,s_t\in S\setminus \{f\}$ coming from finitely many coordinate indices $m_1,\dots ,m_t$. Let $k$ be the least member of $K\setminus \{m_1,\dots ,m_t\}$; this canonical fresh choice uses no Choice principle. Interchanging the two labels if necessary, suppose $c(f(k))=\delta (a_k)$.

By F4 choose a finite $p\in G$ forcing both the unique defining formula for $c$ and $c(f(k))=\delta (a_k)$. Let $b=0$ if $p$ mentions no bit of row $k$, and otherwise let $b$ exceed every mentioned bit. Flip all $(k,j)$ with $j\ge b$. By F3 this fixes $p$, every ordinal, and each $s_i$. It sends $a_k$ to a finite modification of $\omega \setminus a_k$, so it interchanges $\delta (a_k)$ and $\delta (\omega \setminus a_k)$. It fixes $f(k)$ as an unordered pair and fixes all other values of $f$, hence fixes $f$.

Apply F5 to the assertion forced in step 2.1. Because its condition and every defining parameter are fixed, the same $p$ forces that the same uniquely defined $c$ satisfies $c(f(k))=\delta (\omega \setminus a_k)$. Since $p\in G$, both value equations hold in the extension, but F1 says their right-hand sides are distinct. This contradicts functionality of $c$. Thus no choice function exists on an infinite subfamily. A choice on the empty subfamily, on one pair, or on any other fixed finite subfamily is not excluded; the obstruction is exactly the infinite partial-choice claim. The example uses no assertion about ultrafilters on arbitrary sets.