Infinite set always has a countably infinite subset I'm trying to show that one infinite always has a countably infinite subset, but I'm confused with something on the proof. Let $S$ be one infinite set. In that case, to show it has one countably infinite subset means to find a subset $S_0\subset S$ such that there is a bijection between $S_0$ and $\mathbb{N}$.
The procedure I considered is: pick one arbitrary $a_0\in S$ and consider $S\ \setminus \{a_0\}$. This new set will also be infinite, so we can pick $a_1\in S\setminus \{a_0\}$ and consider $S\setminus \{a_0,a_1\}$. This new set is again infinite. We can repeat this procedure $n$ times, for every $n\in \mathbb{N}$ and thus construct a set $\{a_0,a_1,\dots\}$ which will clearly be in bijection to $\mathbb{N}$.
Now there is a point I'm quite unsure. This idea that: we pick $a_0$ from $S$ then we pick $a_1$ from $S\setminus \{a_0\}$ and so forth. It seems to me that in the way I wrote, this is not fully rigorous.
Is that the case? If so, how can this idea be made rigorous?
 A: There is good reason for your worry: you are using a certain amount of the axiom of choice. As a matter of fact, the statement "every infinite set has a countably infinite subset" is not provable in ZF alone(!), so this isn't something you can avoid. There are lots of questions on this site about the possible weird behavior of infinite sets without choice, such as Infinite Set is Disjoint Union of Two Infinite Sets? Have a look around!
That said, your proof - even granting choice - is not quite rigorous. You need to show how you can use the axiom of choice to extract the sequence $a_0, a_1, . . . $ "all at once." In particular, the phrase "we can repeat this procedure $n$ times" is on the right track, but isn't yet all the way there. One way to prove the claim is to use the well-ordering theorem - well-order the set, then look at the first $\omega$-many elements.
A: If by infinite, you mean Dedekind-infinite, then there exists an injective function $f:S\to S$ such that $f$ is not surjective. Since $f$ is not surjective, there exists $a_0\in S$ such that, for all $x\in S$ we have $f(x)\neq a_0$. Then the set $\{a_0, f(a_0), f(f(a_0)) \cdots \}$ can be shown to be order-isomorphic to $N$. No need for AC.
A: Welcome to the wormhole.
A set which has a countably infinite subset is called Dedekind Infinite.  It is not provable within Zermelo-Fraenkel set theory (ZF) that every infinite set is Dedekind infinite.  This was demonstrated by Paul Cohen, who exhibited a model of ZF in which there is an infinite, Dedekind-finite set of real numbers.  See Asaf's answer to my question for implications of this statement in analysis.
You do not need any form of the axiom of choice to prove that infinite equals Dedekind infinite, in the sense that one can construct models of ZF in which all infinite sets have countably infinite subsets but no form of the axiom of choice holds.  However, if we do have some form of the axiom of choice available, even a weak form, then we can prove your statement.
Let me explain.  The axiom of choice states that, given any collection $(A_i\;\colon\; i\in I)$ of nonempty sets, indexed by some set $I$, there exists a choice function picking out, for each $i\in I$, an element $a_i\in A_i$.  In other words, we have a function $f\colon I\to\bigcup_iA_i$ such that $f(i)\in A_i$ for each $i$.
A well-known (but not easy to prove) consequence of the axiom of choice is the well-ordering theorem: given any set $A$, we can order the elements of $A$ in such a way that any nonempty subset of $A$ has a least element under the ordering.  In fact, the well-ordering theorem is equivalent to the axiom of choice, since, given $(A_i\;\colon\;i\in I)$, we can define $f(i)$ to be the least element of $A_i$, under this ordering, giving us a choice function.
With this form of the axiom of choice, one can prove your statement as follows: given your set $S$, order it according to the well-ordering theorem.  Then let $a_0$ be the least element of $S$, let $a_1$ be the least element of $S\setminus\{a_0\}$ and so on.  This process will never terminate; otherwise, $S$ would be equal to $\{a_0,\dots,a_n\}$ for some $n$ and therefore would be finite.
That's all well and good, but the well-ordering theorem is a non-obvious theorem in set theory, and certainly isn't implicit in your argument.  We shouldn't need to use it to prove this statement.
Thankfully, there is another way, and it actually involves a strictly weaker form of the axiom of choice.  The axiom of countable choice is the same as the axiom of choice, except that we require the set $I$ to be countable.  There are models of set theory in which the axiom of choice fails but still holds whenever the index set is countable, so countable choice is strictly weaker than full choice.

Here's how we prove your statement using only countable choice.  Let $S$ be an infinite set.  Then, for each $n=0,1,2,\dots$, let $S_n$ be the set of subsets of $S$ of size $2^n$.
We can show that each $S_n$ is non-empty using your argument (note that the axiom of choice is not required for a finite collection of sets, since we can proceed by induction): inductively pick elements $a_1,\dots,a_{2^n}$ from $S$; since $S$ is infinite, this process will not terminate and since we are only choosing finitely many elements, there are no dodgy set-theory issues.
Now, there are countably many $S_n$, so the axiom of countable choice tells us that there is a sequence $A_0,A_1,A_2,\dots$ of subsets of $S$ such that $A_n$ has size $2^n$ for each $n$.
Now, for each $n$, let $B_n$ be the set of elements of $A_n$ that are not contained in $A_0\cup\dots\cup A_{n-1}$.  Since $A_n$ has size $2^n$, and $A_0,\dots,A_{n-1}$ have at most $1+2+4+\dots+2^{n-1}=2^n-1$ distinct elements between them, $B_n$ must be non-empty.  By the axiom of countable choice again, we can choose a sequence $s_0,s_1,\dots$ with each $s_n\in B_n$.  In particular, the $s_n$ are distinct.  We have found a countably infinite subset of $S$.
A: I presented 3 different proofs.
Proof 1:

Let $(A_n \mid n \in \mathbb N)$ be a sequence of non-empty sets and $X=\bigcup_{n \in \mathbb N} A_n$. Then there exists a mapping $f: \mathbb N \to X$ such that $f(n) \in A_n$.
Lemma: The countable union of countable sets is countable. (I presented a proof here)

Let $A_n=\{g:\{1,\cdots,n \} \to S \mid f \text{ is injective} \}$, then $A_n \neq \emptyset$ for all $n \in \mathbb N$ since $S$ is infinite [We can prove this statement by induction on $n$].
By Axiom of Countable Choice, there exists a mapping $f: \mathbb N \to \bigcup_{n \in \mathbb N} A_n$ such that $f(n) \in A_n$. Then $ \operatorname{ran}f(n) \subseteq S$ is finite and thus countable for all $n \in \mathbb N$.
Let $Y=\bigcup_{n \in \mathbb N} \operatorname{ran}f(n)$, then $Y$ is the countable union of countable sets. Hence $Y \subseteq S$ is countable by Lemma. Furthermore, $Y$ is not finite (If not, there exists an element of $\operatorname{ran}f(k)$ not in $Y$ for some $k \in \mathbb N$). This completes the proof.
Proof 2:
Let $I_n=\{i \le n \mid i \in \mathbb N\}$ and $X=\{f:I_n \to S \mid n \in \mathbb N\}$ be the set of all finite sequences in $S$.
We define a mapping $\phi:X \to \mathcal P(X) \setminus \{\emptyset\}$ as follows: for $x=(s_0,\cdots,s_n) \in X$, let $\phi(x)=\{(s_0,\cdots,s_n,k) \mid k \in S \setminus\{s_0,\cdots,s_n\}\}$, then $\phi(x) \neq \emptyset$. Let $\bar{s}$ be an element of $S$.
By Axiom of Dependent Choice, there exists a sequence $(x_n \mid n \in \mathbb N)$ through $X$ such that $x_{n+1} \in \phi (x_n)$ for all $n \in \mathbb N$. Let $a_n$ be the $n^{th}$ element in $x_n$. By the construction $(a_n \mid n \in \mathbb N)$ is the required sequence.
Proof 3:

Let $(A_n \mid n \in \mathbb N)$ be a sequence of non-empty sets and $X=\bigcup_{n \in \mathbb N} A_n$. Then there exists a mapping $f: \mathbb N \to X$ such that $f(n) \in A_n$.
Lemma: The countable union of countable sets is countable. (I presented a proof here)

Let $A_n=\{g:\{1,\cdots,n \} \to S \mid f \text{ is injective} \}$, then $A_n \neq \emptyset$ for all $n \in \mathbb N$ since $S$ is infinite [We can prove this statement by induction on $n$].
By Axiom of Countable Choice, there exists a mapping $f: \mathbb N \to \bigcup_{n \in \mathbb N} A_n$ such that $f(n) \in A_n$. We define injection $h: \mathbb N \to S$ by $h(n)=f(n)(t)$ where $t=\min \{i \in \mathbb N \mid f(n)(i) \notin \{h(0),\cdots,h(n-1)\}\}$. Such $t$ always exists since $|\operatorname{ran}f(n)|=n>n-1$ for all $n \in \mathbb N$. This completes the proof.
A: Here is another construction that uses the Axiom of dependent choice, denoted by ${\displaystyle {\mathsf {DC}}}$.
Let $\mathcal F(S)$ denote the set of finite subsets of $S$.
Define the relation $R$ on $\mathcal F(S)$ by
$\quad a R b$ if the finite set $b$ is the union of the finite set $a$ with a singleton set disjoint from $a$.
Examples: $\{s,t\} R\{s,t,u\}, \{s,t\}R\{s,t,v\}, \{s,t\}R\{s,t,w\}$
Start with a singleton set $x_0 = \{s_0\}$ and so define the sequence $x_n$ where $x_n R x_{n+1}$.
We can define singleton sets, $y_n = x_n \text{∖} x_{n-1} \, \text{ for } n \ge 1$.
We can define ordered pairs $g_n = \{n\} \times y_n \, \text{ for } n \ge 1$.
We can define a function 
$\tag 1 f = \{(0,s_0)\} \; \cup \;\bigcup_{n \ge 1}\, g_n$
It is easy to see that the function $f$ is an injective mapping of $\mathbb N$ into $S$.
