Proving that existence of injection $f : S\to \mathbb{N}$ implies $S$ is countable? How does one formally prove that if there exists an injective function $f:S \rightarrow \mathbb{N}$ then $S$ is countable? If there exists an injective function $f:S \rightarrow \mathbb{N}$ then there exists a bijection  $g:S \rightarrow f(S)$ and $f(S)\subseteq \mathbb{N}$ is a countable set. But the definition of countable set requires a bijection from $\mathbb{N}$ to $S$? What is missing here?
 A: The definition of countable is that a set is countable precisely when there is a bijective map from it to a subset of the natural numbers.  See for example wikipedia.
Therefore your question is answered immediately by definition.
The more interesting question, which is what I think you really mean to ask, is to show that any countable set is either finite, or there is a bijective correspondence between it and $\mathbb{N}$.
Suppose we have an injective map $f\colon S\to \mathbb{N}$.  Suppose that $S$ is not finite.  We will construct a bijection $g\colon  \mathbb{N}\to S$.
Firstly we describe an inductive process for picking elements $s_0,s_1,s_2,\cdots\in S$.
We know $f(S)$ is not empty, as $S$ is not finite (hence not empty), and given $s\in S$ we have $f(s)\in f(S)$.  By the well-ordering principle   we may pick $x\in S$ minimal in $f(S)$.  As $f$ injective, there is a unique $s_0\in S$ such that $f(s_0)=x$.
Once $s_0,s_1,\cdots,s_{i-1}\in S$ have been selected, we select $s_i\in S$ as follows.  The set: $$X_i=\{x\in f(S)| x>f(s_{i-1})\},$$ is non-empty, as otherwise the image of $f$ would be a finite set, so $S$ would be finite.  By the well-ordering principle we may pick $x\in X_i$ minimal.  As $f$ injective, there is a unique $s_i\in S$ with $f(s_i)=x$.
Now we claim the function $g\colon \mathbb{N}\to S$ mapping $i\mapsto s_i$ is bijective.
Note that by construction, for $i>0$ we have $f(s_i)\in  X_i$ so $f(s_i)> f(s_{i-1})$.  Then by induction on the size of $j-i$, we have if $j>i$ then $f(s_j)>f(s_i)$.  Thus $g$ must be injective.
Now pick an arbitrary $s\in S$.  To show that $g$ is surjective, we must show that $s=s_i$ for some $i\in \mathbb{N}$.  We know $f(s_i)$ is an increasing sequence, so for some $j\in\mathbb{N}$, we have $f(s_j)>f(s)$, so $f(s)\notin X_j$.
To complete our proof we will prove by induction that for $j>0$:$$f(S)=\{f(s_0),f(s_1),\cdots,f(s_{j-1})\}\cup X_j$$
Thus we have that $f(s)=f(s_i)$ for some $i<j$ and $s=s_i$.
We selected $f(s_0)$ minimal in $f(S)$, so for every element $x\in f(S)$, either $x=f(s_0)$ or $x>f(s_0)$ so $x\in X_1$:$$f(S)=\{f(s_{0})\}\cup X_1$$
For the inductive step, we need only note that we selected $f(s_{i-1})$ minimal in $X_{i-1}$, so any element of $X_{i-1}$ is either $f(s_{i-1})$, or greater than $f(s_{i-1})$, so lies in $X_i$:
$$X_{i-1}=\{f(s_{i-1})\}\cup X_i\qquad\qquad (1)$$
Thus for $i\geq 2$: \begin{eqnarray*}f(S)&=&\{f(s_0),f(s_1),\cdots,f(s_{i-2})\}\cup X_{i-1}\\&=&\{f(s_0),f(s_1),\cdots,f(s_{i-2})\}\cup \{f(s_{i-1})\}\cup X_i\end{eqnarray*}
Here the first equality comes from the inductive hypothesis, and the second equality comes from $(1)$.
