The number $3$ plays an interesting role in the following statement:

> $\newcommand{\S}{\sf(S_3)}\S$ $\;$ Let $X$ be a non-empty set and let $f:X \to X$ be fixpoint-free (that is $f(x) \neq x$ for all $x\in X$). Then there are subsets $X_1, X_2, X_3 \subseteq X$ with $X_1\cup X_2\cup X_3 = X$ and $$X_i \cap f(X_i) = \emptyset$$ for $i \in \{1,2,3\}$.

There are easy examples showing that one cannot get by using $2$ subsets only. Statement $\S$ can be [proved](https://math.stackexchange.com/a/3633820/169699) using the axiom of choice. (Although the full force of (AC) is not needed as the strictly weaker [Boolean Prime Ideal Theorem](https://en.wikipedia.org/wiki/Boolean_prime_ideal_theorem) (BPI) [is sufficient](https://mathoverflow.net/a/358030/8628), but it appears that the $\S$ is not a theorem of $\newcommand{\ZF}{{\sf (ZF)}}\ZF$.)

The motivation of this question is to find a weakening of $\S$ that is a theorem of $\ZF$.

**Question.** Is the following statement a theorem of $\ZF$?

> If $f:\mathbb{N}\to\mathbb{N}$ is fixed-point free, then there is a finite set ${\frak S}\subseteq {\cal P}(\mathbb{N})$ with $\bigcup{\frak S} = \mathbb{N}$ such that $S\cap f(S) = \emptyset$ for all $S\in {\frak S}$.

(Note that if we drop the requirement that ${\frak S}$ be finite, then ${\frak S} = \big\{\{n\}:n\in\mathbb{N}\big\}$ would be a trivial solution.)