Formal proof that $N$ is the smallest infinite set I wish to write a formal proof of the following statement: For any infinite set $X$, there exists an injection $f:\mathbb{N}\to X$.

I'd like the proof to explicitly use the full axiom of choice (for every family of sets $\{S_\alpha\}$ there exists a family of elements $\{x_\alpha\}$ such that each $x_\alpha\in S_\alpha$). When this was asked before, none of the answers were explicit about where choice is invoked.

Motivation: I'm TAing a course in discrete math and was embarrassed to find that I can't prove this homework question.
A set $X$ is infinite if and only if there is an injection $\phi:X\to X$ that is not a surjection.  In other words, $\phi$ misses out a nonempty subset $S_1$ of $X$. Let, $X_1:=X\setminus S_1$.  $X_1$ must be infinite (because its bijectively related to $X$), hence there is a map $\phi_1:X_1\to X_1$ that is injective but not surjective, misses out nonempty $S_2\in X_1$, etc.  (Induction will make the argument rigorous, and shows that $X_k\cap X_j=\emptyset$ for all $j\leq k$.) Axiom of choice helps "picking" $f(i):=x_i\in S_i$.
A set $X$ is infinite if and only if there is an injection $\phi:X\to X$ that is not a surjection.  In other words, $\phi$ misses out a nonempty subset $S_1$ of $X$. Let, $X_1:=X\setminus S_1$.  $X_1$ must be infinite (because its bijectively related to $X$), hence there is a map $\phi_1:X_1\to X_1$ that is injective but not surjective, misses out nonempty $S_2\in X_1$, etc.  (Induction will make the argument rigorous, and shows that $X_k\cap X_j=\emptyset$ for all $j\leq k$.) Axiom of choice helps "picking" $f(i):=x_i\in S_i$.