Formal proof that $N$ is the smallest infinite set [duplicate]

This question already has an answer here:

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.

marked as duplicate by Asaf Karagila♦ axiom-of-choice StackExchange.ready(function() { if (StackExchange.options.isMobile) return; $('.dupe-hammer-message-hover:not(.hover-bound)').each(function() { var$hover = $(this).addClass('hover-bound'),$msg = $hover.siblings('.dupe-hammer-message');$hover.hover( function() { $hover.showInfoMessage('', { messageElement:$msg.clone().show(), transient: false, position: { my: 'bottom left', at: 'top center', offsetTop: -7 }, dismissable: false, relativeToBody: true }); }, function() { StackExchange.helpers.removeMessages(); } ); }); }); Apr 8 '15 at 0:34

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$.
• Certainly in this case. Choose one element $a$ not in the range of $\phi$, then let $a_n=\phi^n(a)$. You can show this is an injection from the natural numbers into your infinite set. No choice was used, since we only chose one injection and one element. – Asaf Karagila Apr 8 '15 at 0:47