Proving the injective part of the First Isomorphism Theorem I'm reviewing set theory, and am trying to work out part of the proof of the First Isomorphism Theorem.

*

*Let $f$ be a function from sets $X$ to $Y$. I'd like to prove that $f$ induces an injection from $X/\mathrm{Ker}(f)$ to $\mathrm{Im}(f)$.


*Let $R_1,R_2\in X/\mathrm{Ker}(f)$, and let $g:X/\mathrm{Ker}(f)\rightarrow X$ be a choice function such that $x_1 = g(R_1)$ and $x_2 = g(R_2)$. Now if $f(x_1)=f(x_2)$ then $(x_1,x_2)\in\mathrm{Ker}(f)$, according to the definition of the kernel of $f$.


*But now since $R_1 = \{y\in X:(y,x_1)\in\mathrm{Ker}(f)\}$, both $x_1$ and $x_2$ are members of $R_1$. The same can be said for $R_2$, and so $R_1$ must be the same as $R_2$, since $R_1$ and $R_2$ are part of a partition (they must be identical or otherwise mutually exclusive).


*Therefore, we have that $f(x_1)=f(x_2)\rightarrow R_1 = R_2$, so the mapping induced by $f$ is injective.
Does this seem correct? Do I really need to invoke choice functions? It really seems there must be a simpler way to do this.

The first step is to define a mapping from $\varphi:X/\ker f\to\operatorname{im}f$: you can’t prove that it’s injective until you know what it is. For each $x\in X$ let
$$[x]=\{y\in X:f(y)=f(x)\}\in X/\ker f\,;$$
the natural thing to try is
$$\varphi:X/\ker f\to\operatorname{im}f:[x]\mapsto f(x)\,.$$
The first step is to show that $\varphi$ is well-defined. That is, we need to make sure that if $x_0,x_1\in R\in X/\ker f$, so that $[x_0]$ and $[x_1]$ are both names for the same set $R$, the value of $\varphi(R)$ does not depend on which of these names we use. This isn’t hard: if $x_0,x_1\in R\in X/\ker f$, then $f(x_0)=f(x_1)$, and therefore
$$\varphi([x_0])=f(x_0)=f(x_1)=\varphi([x_1]),,$$
as desired.
Now that we know that $\varphi$ really does define a function, we can try to show that this function is injective. Suppose that $\varphi([x_0])=\varphi([x_1])$. Then
$$f(x_0)=\varphi([x_0])=\varphi([x_1])=f(x_1)\,,$$
so $x_0\in[x_1]$, $[x_0]=[x_1]$, and $\varphi$ is indeed injective.
