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

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.

• This is just the axiom of choice for a finite family of sets, which is a consequence of $\mathsf{ZF}$; see this question. – Brian M. Scott Aug 2 '16 at 14:22

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$.