The smallest infinity and the axiom of choice

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.

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:

1. 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.

2. 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:

1. 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).

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.