Proof of $ f:I_n \rightarrow I_m \Rightarrow n = m$ I am trying to improve my proof-writing skills.
Would the following proof be correct for the $ f:I_n \rightarrow I_m \Rightarrow n = m$ bit?
Problem:
Prove that the notion of number of elements of a nonempty finite set is a well defined concept. More precisely, prove that there exists a bijection $ f:I_n \rightarrow I_m $ if and only if $n = m$.
Attempt:
First prove $ f:I_n \rightarrow I_m \Rightarrow n = m$.
Assume that $ f $ is a bijective function such that $ f:I_n \rightarrow I_m $
By definition, since $f$ is injective, $ \forall a, b \in I_n, f(a) = f(b) \Rightarrow a = b $, where $ f(a), f(b) \in I_m $. Therefore every element in $I_m$ corresponds to at most one element in $I_n$. $\quad (1)$
Also by definition, since $f$ is surjective, $ \forall b \in I_m, \exists a \in I_n $. That is every element in $I_m$ corresponds to at least one element in $I_n$. $ \quad (2)$
Now if $ n > m$, then by $(2)$ some element in $I_n$ corresponds to an element in $I_m$ which is already mapped to. This cannot be true.
Likewise, if $ n < m$ then by $(1)$ some element in $I_n$ corresponds to more than one element in $I_m$. Again, this cannot be true.
Therefore $n = m$.
EDIT: 
$I_n = \{  j \in \mathbb{N} ; 1 \leq j \leq n \}$
EDIT 2:
Going into more detail as per the guidance in the comments. I have only proven statement $(1)$ as the proof for statement $(2)$ is similar.

By definition, since $f$ is injective, $ \forall a, b \in I_n, f(a) = f(b) \Rightarrow a = b $, where $ f(a), f(b) \in I_m $. 
Therefore every element in $I_m$ corresponds to at most one element in
  $I_n$. $\quad (1)$

Proof of this statement:
Select an arbitrary element $b \in I_m$. Assume that $f(a_1) = b$ and $f(a_2) = b$ where $a_1 \neq a_2$. But since $f$ is injective we know that $f(a_1) = f(a_2) \Rightarrow a_1 = a_2$. Therefore every element in $I_m$ corresponds at most to a single element in $I_n$.
 A: In this part of the argument:

... Now if $n>m$, then by (2) some element in $I_n$ corresponds to an element in $I_m$ which is already mapped to. This cannot be true.

you are implicitly using the pigeonhole principle.  However, given that one possible statement of the pigeonhole principle is: "If $|A| > |B|$ then no function $f : A \to B$ is injective" then the result you want to prove is clearly closely related to this formulation of the pigeonhole principle, and is at least at about the same level.  Therefore, if you're not careful, and your informal proof of the pigeonhole principle ends up implicitly relying on this result, then you could easily end up with a circular argument.
Here's an alternate approach which is more likely to avoid being an unintentional circular argument: proceed by induction on $m$.  To be more explicit about how we'll use the induction principle, let $P(m)$ be the statement: for all $n \in \mathbb{N}_0$, if there is a bijection $f : I_n \to I_m$, then $n = m$.  What we want to prove is: $\forall m \in \mathbb{N}_0, P(m)$.
I'll leave the base case $m=0$ to you.  (Or — depending on whether or not you're comfortable reasoning about functions with empty domain and/or codomain — you might find it easier to treat the base case as being $m=1$.)
For the inductive step $\forall m \in \mathbb{N}_0, P(m) \rightarrow P(m+1)$, suppose for some $n$ that we have a bijection $f : I_n \to I_{m+1}$; we then want to prove that $n = m+1$.  First, note that since $f$ is surjective, there must exist some $x \in I_n$ such that $f(x) = m+1$; therefore $I_n$ is nonempty so $n > 0$.  Thus $n = n' + 1$ for some $n' \in \mathbb{N}_0$.  Now, $f$ is a bijection from $I_{n'+1} = I_{n'} \sqcup \{ n' + 1 \}$ to $I_{m+1} = I_m \sqcup \{ m + 1 \}$.  I will now refer to the answers to How to prove $ A \cup \{a\} \approx B \cup \{ b \} \Rightarrow A \approx B $ to conclude that there exists a bijection $g : I_{n'} \to I_m$, which by the inductive hypothesis $P(m)$ implies that $n' = m$.  Therefore, $n = n'+1 = m+1$.
(In case you want to treat the base case as being $m=1$, i.e. you want to prove the statement only in case $m, n \in \mathbb{N}_+$, then the adjustment to make is: the first step will be to show that if we have a bijection $f : I_n \to I_{m+1}$ with $m \ge 1$ then $n \ge 2$.  Once you show that, then conclude $n = n' + 1$ for some $n \ge 1$ and from here we can proceed as in the previous paragraph.)

Note that it's also possible to use induction on $n$ instead of induction on $m$, and the resulting proof will end up being very similar.
A: By my training, this would not be considered a correct proof.

By definition, since $f$ is injective, $\forall a,b \in I_n$, $f(a)=f(b)\Rightarrow a=b$, where $f(a),f(b)\in I_m$.
Therefore every element of $I_m$ corresponds to at most one element in $I_n$.

This is just a statement of a definition and the statement of a conclusion. There isn't any reasoning connecting the two.  I would start by choosing an arbitrary element of $I_m$ and proving, based on the fact that $f$ is injective, that there cannot exist more than one corresponding element of $I_n$. I can't say much more without giving the answer away; it's pretty simple.
If this were part of a more complex proof, you wouldn't need to be so explicit with every logical inference of something so simple and tangential, but then again, in a more complex proof, you would probably just take this as given. If you're doing this as an exercise in proofwriting, I'd recommend being more thorough.
