Can ZF prove that every surjection with finite codomain has a section?

Question

Can ZF prove the following?

Theorem. Let $X$ and $Y$ denote sets and $e : X \rightarrow Y$ denote a surjection. If $Y$ is finite, then $e$ has a section, i.e. a function $m : Y \rightarrow X$ such that $e \circ m = \mathrm{id}_Y$.

(Assuming the axiom of choice, this is trivial.)

(By finite, I mean bijectable with an element of $\omega$.)

I think this is provable at least for specific finite choices of $Y$; we should be able to prove it for $Y \cong 0$, for $Y \cong 1$, for $Y \cong 2$ etc. just by choosing values in $X$ for each element of $Y$. I don't understand the technical details. I also don't understand whether or not we can "glue" all these miniproofs together to derive the theorem of interest.

Answer 1

Yes, this is the same as saying that every finite family of nonempty sets admits a choice function, just the fibers.

And of course, using induction we can show that every finite family of nonempty sets admits a choice function.

Answer 2

Let me write out the proof explicitly, since you said you were unclear on the technical details. The key thing that lets you "glue together" all the "miniproofs" is induction. That is, we will prove by induction in $n\in \omega$ that if $Y$ is a set of cardinality $n$ and $e:X\to Y$ is a surjection, then it has a section.

If $n=0$, this is trivial: we must have $Y=\emptyset$, and then the unique map $m:\emptyset\to X$ works since there is only one map $Y\to Y$.

Now suppose we know the statement for $n$, and $Y$ has $n+1$ elements. Let $y_0\in Y$ be an element, let $Y'=Y\setminus\{y_0\}$, and $X'=e^{-1}(Y')$. Then $e$ restricts to a surjection $e':X'\to Y'$. By the induction hypothesis, there is a map $m':Y'\to X'$ such that $e'\circ m'=1_{Y'}$. Since $e$ is surjective, there exists $x_0\in X$ such that $e(x_0)=y_0$. Define $m:Y\to X$ by $e(y)=e'(y)$ if $y\in Y'$ and $e(y_0)=x_0$. Then $e\circ m=1_Y$.