Equivalent Dedekind-finiteness tests in the basic Cohen model

If $B\subseteq A$ is countably infinite, a displayed bijection $b:\omega \to B$ followed by inclusion is an injection $\omega \to A$. Conversely, the range of an injection $i:\omega \to A$ is a subset of $A$ bijective with $\omega$. These are explicit maps and require no simultaneous choices.

From an injection $i:\omega \to A$, define $h:A\to A\setminus \{i(0)\}$ by $h(i(n))=i(n+1)$ and $h(x)=x$ off $i[\omega ]$. The two pieces are disjoint, and the inverse sends $i(n+1)$ to $i(n)$ and fixes the complement, so $h$ is a bijection onto a proper subset.

Conversely, if $h:A\to B⊊A$ is a bijection, choose the single witness $x_0\in A\setminus B$ and recursively put $x_{n+1}=h(x_n)$. Injectivity of $h$ and the fact that $x_0$ is not in its range show by cancellation that the $x_n$ are distinct. Thus $n\mapsto x_n$ injects $\omega$ into $A$. This uses one existential witness and recursion, not Countable Choice.

F1 rules out the proper-subset bijection. By step 1.1, step 1.2, step 1.3 it therefore rules out an $\omega$-injection and a countably infinite subset as well. Both implications of every equivalence have been accounted for in ZF.