If $f: A \rightarrow B$ is injective, $\exists ! f^{-1}:f(A)\rightarrow A$ such that $f^{-1}f(x) = x$ If $f: A \rightarrow B$ is injective, $\exists ! f^{-1}:f(A)\rightarrow A$ such that $f^{-1}f(x) = x$
I know the proof of this is super simple, like 2 lines (+ some for uniqueness), but I can't figure how to logically work it out. For definition of injective function, I have $\forall x,y\in A, f(x)=f(y) \implies x=y$.
So we are trying to show that for all $y \in f(A),$ there exists a unique $x\in A$ with $f^{-1}(y) = x$. Could I change y to f(x) right there?
 A: We can use the following:
Lemma 1: A function $f : X \to Y$ is invertible if and only if it is one-to-one and onto.
Proof: Suppose that $f : X \to Y$ is invertible.  Then, there exists a function $g : Y \to X$ such that $(f \circ g)(x) = (g \circ f)(x) = x$.  To see that $f$ is onto, pick an element $y \in Y$.  Then, $f(g(y)) = y$ so that $y$ is in the range of $f$.  To see that $f$ is one-to-one, suppose that $f(x) = f(y)$.  Then, $$g(f(x)) = g(f(y)) \implies x = y.$$
Now, suppose that $f$ is one-to-one and onto.  We will show that $f$ is invertible.  As $f$ is onto, we have that $\forall y \in Y, \exists x \in X$ such that $y = f(x)$.  Since $f$ is injective, we have that $f(x) = f(y) \implies x = y, \forall x , y \in X$.  
Let $g : Y \to X$ be defined by $g(y) = x$ if and only if $f(x) = y ~$ (why can we assume such a $g$ exists?).  Then $g(f(x)) = g(y) = x$ and $f(g(y)) = f(x) = y$.  Hence $g$ is an inverse of $f$. QED.
Lemma 2: The inverse of a function $f$ is unique if it exists.  
Proof: Suppose that $f : X \to Y$ is invertible and it has two inverses $g, h : Y \to X$.  Note that $\forall x \in X$, we have $f(g(x)) = x = f(h(x))$.  Hence:
$$
g(x) = g(f(g(x))) = g (f(h(x))) \implies g(x) = h(x).
$$
Since $x$ was arbitrary, $g$ and $h$ must be identical as they have the same value for all $x \in X$. QED.
Finally, apply the above lemmas to the function $f\big|_A : A \to f(A)q$.  Note that the function $f : A\to f(A)$ is bijective so long as it is injective.  By definition,
$$
f(A) = \left\{y \in B : f(x) = y ~~~\text{ for some }~~ ~x \in X\right\},
$$
so that $f\big|_A : A \to f(A)$ is surjective, and hence $f|_A$ is bijective.
A: Note that the injectivity is needed for uniqueness only: If you are given $y \in f(A)$, then by the definition of $f(A) = \{f(x)\mid x \in A\}$ there exists a $x \in A$ with $f(x) = y$. 
For uniqueness use injectivity: If $f(x) = y$ and $f(x') = y$, then $f(x) = f(x')$, hence $x=x'$.
