$f$ is a monomorphism $\Rightarrow$ $f$ is injective, alternative proof

Question

Reading Aluffi (again) I stumbled across the proof of Prop. 2.3, which is

$f$ is injective $\Leftrightarrow$ $f$ is a monomorphism in the category Set.

This proposition comes in the text after the (Prop. 2.1) which states

(1) $f$ has a left-inverse $\Leftrightarrow$ $f$ is injective.

Now in the proof of "$\Leftarrow$" in Prop. 2.3 in the book, he says he will use "microscopic" information by going down to the level of sets and elements looking at maps $\alpha', \alpha''$ which only act on sets $Z$ which are singletons $\{p\}$. Then it becomes quickly clear that $f$ only can be an injective function.

Now I wonder if (and if not, why not) one really needs to go back at sets at this stage, or if its not rather possible to proof this using Prop. 2.1, which would be more elegant in my eyes.

So my attempt is the following:

$f$ is a monomorphism by supposition, proof by contradiction: Assume $f$ is not injective. By Prop. 2.3 that means $\neg(\exists g: g \circ f = \mathrm{id}_A)=(\forall g: g \circ f \ne \mathrm{id}_A).$ Now it is left to show that $f\circ\alpha'=f\circ\alpha''\Rightarrow\alpha' = \alpha''$ is impossible under that circumstance. And here I am hanging a bit. I am not sure if this conclusion can be made without recurring to mapping elements. Any comment is appreciated!

---

The definition of monomorphism from Aluffi this question is referring to is the following:

A function $f:A\to B$ is a monomorphism (or monic) if the following holds:

for all sets Z and functions $\alpha', \alpha'': Z\to A$

$f\circ\alpha'=f\circ\alpha''\Rightarrow\alpha' = \alpha''.$

Answer 1

Injectivity makes sense only in the category $\mathcal Set$ of sets and functions.

Then we can extend it to categories $\def\m{\mathcal} \m C$ equipped with an 'underlying set' functor $\m C\to\m Set$, and we will find that most of the times, an arrow in such a ('concrete') category is monomorphism iff it is injective.
The other property (having a left inverse) is usually much stronger: the set theoretic left inverses are rarely homomorphisms.
In $\m Set$ these properties happen to be equivalent.