Working on the book: Richard Hammack. "Book of Proof" (p. 251)
Theorem 12.3 Let $f$ : $A \to B$ be a function. Then $f$ is bijective if and only if the inverse relation $f^{-1}$ is a function from $B$ to A.
Defining inverse relation $f^{-1}$ as: $$ \forall x\forall y((y,x) \in f^{-1} \leftrightarrow ((x,y) \in A \times B \land (x,y) \in f)) $$ $(\implies)$ I need to show: $$ \forall x(x \in B \to \exists!y(y \in A \land (x,y) \in f^{-1})) $$
Rules of inference used can be found in Appendix C of this book: forall x: An Introduction to Formal Logic.
My questions: The author justifies the proof by invoking a theorem. I tried to do it with these four premises. Is this a valid proof ?
Proof using Fitch-Style natural deduction system (ommited obvious inferences):
$ \def\fitch#1#2{\quad\begin{array}{|l}#1\\\hline#2\end{array}} \def\Ae#1{\qquad\mathbf{\forall E} \: #1 \\} \def\Ai#1{\qquad\mathbf{\forall I} \: #1 \\} \def\Ee#1{\qquad\mathbf{\exists E} \: #1 \\} \def\Ei#1{\qquad\mathbf{\exists I} \: #1 \\} \def\R#1{\qquad\mathbf{R} \: #1 \\} \def\ci#1{\qquad\mathbf{\land I} \: #1 \\} \def\ce#1{\qquad\mathbf{\land E} \: #1 \\} \def\oi#1{\qquad\mathbf{\lor I} \: #1 \\} \def\oe#1{\qquad\mathbf{\lor E} \: #1 \\} \def\ii#1{\qquad\mathbf{\to I} \: #1 \\} \def\ie#1{\qquad\mathbf{\to E} \: #1 \\} \def\be#1{\qquad\mathbf{\leftrightarrow E} \: #1 \\} \def\bi#1{\qquad\mathbf{\leftrightarrow I} \: #1 \\} \def\qi#1{\qquad\mathbf{=I}\\} \def\qe#1{\qquad\mathbf{=E} \: #1 \\} \def\ne#1{\qquad\mathbf{\neg E} \: #1 \\} \def\ni#1{\qquad\mathbf{\neg I} \: #1 \\} \def\IP#1{\qquad\mathbf{IP} \: #1 \\} \def\x#1{\qquad\mathbf{X} \: #1 \\} \def\DNE#1{\qquad\mathbf{DNE} \: #1 \\} $
$ \fitch{1.\,\forall x(x \in A \to \exists! y(y \in B \land (x,y) \in f) \qquad\textit{f is a function from A to B}\\ 2.\,\forall x\forall x'((x \in A \land x' \in A \land x \neq x') \to f(x) \neq f(x')) \qquad\textit{f is injective}\\ 3.\,\forall y(y \in B \to \exists x(x \in A \land f(x) = y)) \qquad\textit{f is surjective}\\ 4.\,\forall x\forall y((y,x) \in f^{-1} \leftrightarrow ((x,y) \in A \times B \land (x,y) \in f)) }{ \fitch{5.\,b \in B}{ 6.\,b \in B \to \exists x(x \in A \land f(x) = b)) \Ae{3} 7.\,\exists x(x \in A \land f(x) = b)) \ie{6,5} \fitch{8.\,a \in A \land f(a)=b}{ 9.\,f(a)=b \ce{8} 10.\,(b,a) \in f^{-1} \leftrightarrow ((a,b) \in A \times B \land (a,b) \in f) \Ae{4} 11.\,a \in A \ce{8} 12.\,b \in B \ce{5} 13.\,(a,b) \in A \times B \\ 14.\,(a,b) \in f \\ 15.\,(a,b) \in A \times B \land (a,b) \in f \ci{14,9} 16.\,(b,a) \in f^{-1} \be{15,14} 17.\,a \in A \land (b,a) \in f^{-1} \ci{11,16} \fitch{18.\,c \in A \land (b,c) \in f^{-1}}{ 19.\,(b,c) \in f^{-1} \ce{18} 20.\,(c,b) \in f\\ \fitch{21.\,a \neq c}{ 22.\,(a \in A \land c \in A \land a \neq c) \to f(a) \neq f(c) \Ae{2} 23.\,(a \in A \land c \in A \land a \neq c) \ci{21} 24.\,f(a) \neq f(c) \ie{22,23} 25.\,(a,b) \in f\\ 26.\,(c,b) \in f\R{20} 27.\,f(c)=b\\ 28.\,f(a)=f(c) \qe{27,9} 29.\,\bot \ne{24,28} }\\ 30.\,a = c \IP{21-29} }\\ 31.\,(c \in A \land (b,c) \in f^{-1}) \to a = c \ii{18,30} 32.\,\forall z(z \in A \land (b,z) \in f^{-1}) \to a = z \Ai{31} 33.\,a \in A \land (b,a) \in f^{-1} \land \forall z(z \in A \land (b,z) \in f^{-1}) \to a = z \ci{17,32} 34.\,\exists y(y \in A \land (b,a) \in f^{-1} \land \forall z(z \in A \land (y,z) \in f^{-1}) \to a = z) \Ei{33} 35.\,\exists!y(y \in A \land (a,y) \in f^{-1}) }\\ 36.\,\exists!y(y \in A \land (a,y) \in f^{-1}) \Ee{7,8-35} }\\ 37.\,b \in B \to \exists!y(y \in A \land (x,y) \in f^{-1}) \ii{5-36} 38.\,\forall x(x \in A \to \exists!y(y \in A \land (x,y) \in f^{-1})) \Ai{37} } $