Prove the Existence of an Inverse Function We're asked to prove formally that if $f: X \rightarrow Y$ is one-to-one, then there is a $f^{-1}: f(X) \rightarrow X$ such that $(f^{-1} \circ f)(x) = x$.
Let $f = \{ (x,y) | x \in X, y = f(x) \}$ and define $f^{-1} = \{ (y,x) | y \in f(X), x = f^{-1}(y) \}$.  Show that $f^{-1}$ is a one-to-one function from $f(X)$ onto $X$. 
1.  Since $f$ is one-to-one, $f(x) = y = f(x') \rightarrow x = x'$.  If $(y, x), (y, x')$ are elements of $f^{-1}$, $x = x'$.  So $f^{-1}$ is a function. 
2.  Since $f$ is a function, $y = f(x) = y'$, entailing that if $(y, x), (y', x)$ are elements of $f^{-1}$, $y = y'$.  $f^{-1}$ is one-to-one. 
3.  By the fact that the domain of $f^{-1}$ is $f(X)$, for all $x \in X$, there is a $y \in f(X)$ such that (y, x) is an element of $f^{-1}$.  So $f^{-1}$ is onto.
I want to argue that there is only one $x$ and only one $y$ such that $(x, y) \in f$ and $(y,x) \in f^{-1}$.  Therefore, $f(f^{-1}(y)) = f(x) = y$ and $f^{-1}(f(x)) = f^{-1}(y) = x$.  Can you kindly give me a clue on how to do that?
 A: Let $\phi = \{(y,x) | (x,y) \in f \}$.
First show that it is a function: If $(y,x_1), (y,x_2) \in \phi$, then $(x_1,y), (x_2,y) \in f$, and since $f$ is injective, we have $x_1 = x_2$.
The domain of $\phi$ is $\{ y | (y,x) \in \phi \} = \{ y | (x,y) \in f \}=f(X)$.
Now check to see if $\phi \circ f = \operatorname{Id}$. So suppose $(y,x_2) \in \phi$ and $(x_1,y) \in f$. Then $(x_2,y ) \in f$, and since $f$ is injective, we have $x_1=x_2$. Hence $\phi \circ f = \{ (x,x) | x \in X \} = \operatorname{Id}$.
Let $f^{-1} = \phi$ to finish.
A: Using a (better) notation:
$$G_f := {\rm graph}(f) := \{(x,y) \in X\times Y|\quad \exists\ x\in X, y\in Y: f(x) = y\}$$
and $G_{f^{-1}}$ analogously.
You want to show
$$\forall (x',y) \in G_f \qquad \exists!\ x\in X: f(x) = y$$
and
$$\forall (x, y') \in G_f \qquad \exists!\ y\in Y: f(x) = y$$
The former is equivalent to the definition of injective (one-one):
Let $(x,y), (x',y) \in G_f$, then $f(x) = y = f(x')$ since $f$ is injective, $x=x' \Rightarrow (x,y) = (x',y)$
q.e.d.
The latter is the definition of a (well-defined) function.

Since those two properties hold for $G_f$ you can define $f^{-1}$ by
$$f^{-1}(y) = x | \qquad \exists!\ (x,y) \in G_f$$
$$f(x) = y | \qquad \exists!\ (x,y) \in G_f$$
