Can someone give me their opinion on how I wrote this proof also all my definitions are at the end.
Given a function $f:A\to B$, its inverse relation $f^{-1}$ is a function from $B$ to $A$ if and only if $f$ is a bijection from $A$ onto $B$.
$\textbf{My attempt:}(\Longrightarrow)$ Assume the function $f:A\to B$ has an inverse relation $f^{-1}$ which is a function from $B$ to $A$. Then $f^{-1}\circ f=i_A$. Fix $a_1,a_2\in A$ and $f(a_1)=f(a_2)$.Then
$i_A(a_1)=a_1$ and $i_A(a_2)=a_2$
$f^{-1}\circ f(a_1)=i_A(a_1)=a_1$
$f^{-1}\circ f(a_2)=i_A(a_2)=a_2$ by assumption $a_1=a_2$.
WLOG the opposite will also be true and hence $a_2=a_1$ and therefore the function $f$ is injective.
Fix $b\in B$
$a=f^{-1}(b)$
$f(a)=f(f^{-1}(b))$
$=f\circ f^{-1}(b)$
$=i_B$
$=b$
Thus $f(a)=b$ so $f$ is surjective and therefore is bijective.
$(\Longleftarrow)$ Assume $f$ is a bijection from $A$ onto $B$. Since $f$ is bijective, then it will be surjective and by definition 2, the domain of $f^{-1}$ would then be $B$ thus $dom(f^{-1})=B$. Also since $f$ is bijective, then it will be injective and by definition 1, $f^{-1}$ will only have one element of $A$ for each element of $B$. So by definition 4, $f:A\to B$, its inverse relation $f^{-1}$ is a function from $B$ to $A$.
Definitions
$\textbf{(1)}$ A relation $R\subseteq A\times B$ is injective if $(x_1,y) \in R$ and $(x_2,y) \in R$ implies $x_1=x_2$
$\textbf{(2)}$ We say a function $f:A\to B$, is a surjection from A onto B if $\forall y\in B$ $\exists x \in A (f(x)=y).$ In this case we will also call $f$ a surjection from $A$ onto $B.$
$\textbf{(3)}$ We say a function $f:A\to B$, is said to be a bijection from $A$ to $B$ if it is injective and surjective.
$\textbf{(4)}$ A function $f$ from a set $A$ to a set $B$ is a relation from $A$ to $B$ for which $(((x,y_1) \in f) \land ((x,y_2) \in $f$)) \rightarrow y_1=y_2$,
Best Answer
It follows directly from the definitions. For this, view mappings as relations.
A mapping $f:A\rightarrow B$ is a relation $f\subseteq A\times B$ which is left-total $$\forall x\in A\exists y\in B[xfy]$$ and right-unique $$\forall x\in A\forall y,y'\in B[xAy\wedge xAy'\rightarrow y=y'].$$ A mapping $f$ is injective (left-unique) if $$\forall x,x'\in A\forall y\in B[xAy\wedge x'Ay\rightarrow x=x'].$$ A mapping $f$ is surjective (right-total) if $$\forall y\in B\exists x\in A[xAy].$$
So $f$ is bijective means that $f$ is left-total, right-unique, right-total, and left-unique.
Note that inverse relation $f^{-1}\subseteq B\times A$ always exists. (Going from $f$ to $f^{-1}$ the left-properties become right-properties and vice versa.)
This means that $f^{-1}$ is right-total, left-unique, left-total, and right-unique, i.e., $f^{-1}$ is bijective.