Quotient function without the axiom of choice

Question

Given a surjection $\pi:E\to F$ and a function $f:E\to G$ such that for all $x,y\in E, \pi(x)=\pi(y)\Rightarrow f(x)=f(y)$, I'd like to prove that there exists a function $g:F\to G$ such that $f=g\circ\pi$.

The simplest proof I found invokes the axiom of choice to get a right inverse $h:F\to E$ of the surjection $\pi$, and then set $g=f\circ h$.

Is there a proof that avoids the axiom of choice ?

Please give this proof in full Zermelo-Fraenkel details. I'm trying to clarify the usual phrase that for $g(y)$ "we can take $f(x)$, where $x$ is any element of $\pi^{-1}(y)$". I don't really like this specification of $x$ by "any".

Answer 1

To be perfectly explicit, define $$S=\{(y,z)\in F\times G:\text{there exists }x\in E\text{ such that }\pi(x)=y\text{ and }f(x)=z\}.$$ Since $F\times G$ is a set, $S$ is a set by Separation.

Now let us prove that $S$ is a function from $F$ to $G$: that is, for each $y\in F$, there exists a unique $z\in G$ such that $(y,z)\in S$. Given $y\in F$, there exists $x\in E$ such that $\pi(x)=y$. Let $z=f(x)$ for such an $x$*; then $(y,z)\in S$. Now we need to prove that this $z$ is unique, so suppose there exists $z'\in G$ such that $(y,z')\in S$ as well. Then there exists $x'\in E$ such that $\pi(x')=y$ and $\pi(x')=z'$. So $\pi(x')=\pi(x)$, which by hypothesis implies that $f(x')=f(x)$. That is, $z'=z$.

So $S$ is a function from $F$ to $G$, which we will call $g$. It remains to be checked that $f=g\circ \pi$. So given $x\in E$, we want to show that $g(\pi(x))=f(x)$. Writing $y=\pi(x)$, and $z=f(x)$, we have $(y,z)\in S$ by definition of $S$. This says exactly that $g(\pi(x))=f(x)$.

*I'm guessing you may object to "picking" such an $x$ here, but this is perfectly valid. One of the basic rules of first-order logic is that if you have a statement of the form $\exists x\varphi(x)$, then you can let $x$ denote some particular object such that $\varphi(x)$ is true and continue your proof using this $x$ (exactly how this is formalized may depend on exactly what deductive system you are using).