The smallest infinity and the axiom of choice The short version of this question is: which (natural) axiom should be added to ZF so that the statement "$\aleph_{0}$ is the smallest infinity" becomes true?
A set $A$ is called infinite if it can be put in bijection with a proper subset of itself, or, equivalently, if there exists an injection $\phi \colon A \hookrightarrow A$ that is not a bijection. Consider the following proof that the cardinality of the natural numbers, $\aleph_{0}$, is the 'smallest' infinity.
It is enough to show that for every infinite set $A$ there is an injection $\mathbb{N} \hookrightarrow A$. It is simple to prove that if $A$ is in bijection with a set $B$, then $B$ is also infinite. Define $A_{0} = A$, and let $\phi_{0} \colon A_{0} \rightarrow A_{0}$ be an injection that is not a bijection.
Denote $A_{1} = \phi(A_{0})$, and $B_{1} = A_{0} - A_{1}$. By definition of $\phi_{0}$, we have $B_{1} \ne \emptyset$.
Since $A_{1}$ is also infinite (as $\phi$ restricts to a bijection between $A_{0}$ and $A_{1}$), we can repeat this process with a non-bijective injection $\phi_{1} \colon A_{1} \rightarrow A_{1}$, and define 
$A_{2} = \phi_{1}(A_{1})$ and $B_{2} = A_{1} - A_{2}$, with $B_{2} \ne \emptyset$.
Continuing in this manner we obtain an infinite descending chain of proper subsets $$A_{0} \supsetneq A_{1} \supsetneq A_{2} \supsetneq A_{3} \supsetneq A_{4} \supsetneq \cdots$$
and a countably infinite family $\{B_{n}\}_{n \in \mathbb{N}}$ of mutually disjoint subsets of $A$. Choosing a $b_{i}$ from each $B_{i}$, we obtain an infinite sequence of elements of $A$ without repetitions $$b_{1}, b_{2}, b_{3}, b_{4}, \dots,$$
which is exactly an injection $\mathbb{N} \hookrightarrow A$.
It seems clear to me that the above argument uses the axiom of choice in choosing the sequence $\{ b_{n} \}_{n \in \mathbb{N}}$. It also seems clear that without something like AC one cannot guarantee that $\aleph_{0}$ is the smallest infinity. However I've also been told that people often mistakenly use the axiom of choice, or use the full axiom when a weaker variant would do. Since here I have an ordered, countably infinite collection of sets to make a choice from, it seems like this might be the case.
I am no set theorist, so I don't know how to answer these questions (and maybe even how to ask them), but roughly: are there commonly used axioms that imply '$\aleph_{0}$ is the smallest infinity', but are weaker than AC? Is there a minimal such axiom? Can one adopt '$\aleph_{0}$ is the smallest infinity' as an axiom, or would this cause problems?
EDIT: I am informed below that no version of the axiom of choice is necessary with this definition of 'infinite set'. So what about when we use the 'usual' definition of an infinite set: a set that is not in bijection with any natural number.
Supplementary question: why is the 'usual' definition preferable to the 'bijective with proper subset' definition? The latter seems more natural to me, seeing as it only mentions sets and doesn't require numbers to be defined.
 A: The "most natural axiom" to add is perhaps the axiom of countable choice which asserts the existence of a choice function for every countable family of non-empty sets.
I'd even argue that the true "natural axiom" would be the principle of dependent choice, which is a slight (but significant) strengthening of countable choice which posits that recursive definitions work as they should. 
The reason that the latter is "more natural" is that it allows the usual proof to go through. If $A$ is infinite, let $a_0\in A$, then if $a_0,\ldots,a_n$ were chosen, we choose $a_{n+1}\in A\setminus\{a_0,\ldots,a_n\}$. We can transform this proof to only use countable choice, but the proof is inherently different since we are not allowed to use such recursive selection (where each choice depends on the previous ones, thus the name "dependent choice").
(Note, by the way, that the definition of "finite" or "infinite" branch out without the axiom of choice. Being equipotent with a bounded set of natural numbers is not the same as having no self-injection which is not surjective, without assuming some amount of choice. In fact, that is just the point of infinite sets without countably infinite subsets.)
Addressing the edit.
You are asking why is the usual definition of finiteness is the most natural one. Well, there are two points here:


*

*We can define the natural numbers via pure set theoretic means, so the statement "equipotent with a bounded set of natural numbers" mentions only sets and no numbers at all.

*There are other definitions which provably give you the same definition of finiteness. For example: $A$ is finite if and only if every non-empty $U\subseteq\mathcal P(A)$ has a $\subseteq$-minimal element (or, $\mathcal P(A)$ is well-founded with $\subseteq$).
So why is this the natural definition? Well, thinking outside of set theory, this is how we think about finite sets. And where the definition of Dedekind (the one you originally cited) gives us some notion of finiteness, it turns out that we need to use the axiom of choice to prove the equivalence. This, to me, says that philosophically we sort of miss the target there.
As it turns out there is a nice hierarchy (which is mostly linear) of definition of finiteness which branch and differ without the axiom of choice. But they all have the same two properties:


*

*Nothing is worthy of being finite if it is not Dedekind-finite (or, a set cannot be called finite if there is an injection from $\Bbb N$ into the set). And


2.The "true" definition of finite must satisfy whatever we define as finiteness. Otherwise we miss the point of the definition (because the definition comes to model our intuition, and not vice versa).
A: You can indeed adopt the axiom "every infinite set has a countably infinite subset", i.e., "every set that is not equipotent to a natural number (=finite ordinal) has a subset equipotent to the set $\omega = \mathbb{N}$ of natural numbers".  This can also be reformulated as "every D-finite set is finite", where a D[edekind]-finite set is one that does not contain a countably infinite subset.
This is weaker than the full axiom of choice: for example, it is implied by the axiom of countable choice (proof is on previously linked Wikipedia article) and is even weaker than it (reference there).  It is not, however, a very useful form of the axiom of choice: weak forms of AC are generally chosen because they have interesting useful consequences (typically, the axiom of dependent choice), whereas "every D-finite set is finite" is not terribly productive.
A: With your definition of "infinite set" (which is Dedekind's definition, not the usual one), no axioms beyond ZF are needed to prove that $\aleph_0$ is the smallest infinite cardinal.
Let $A$ be an infinite set, and let $\phi:A\to A$ be an injection which is not a bijection. Choose an element $a\in A\setminus\phi(A).$ Then $a,\phi(a),\phi(\phi(a)),\phi(\phi(\phi(a)))\dots$ is an infinite sequence of distinct elements of $A$, showing that $|A|\ge\aleph_0.$
Your question would be more interesting if you defined "infinite set" in the usual way, namely, a set $A$ is infinite if there is no bijection between $A$ and any natural number.
