How do i formally write down a countable choice function? Let $A$ be an infinite set.
Then, we can construct an injective function $f:\omega \rightarrow A$. 
But how do i construct this via orginal statement of $AC_\omega$? (i.e. $\forall countable X, [\emptyset \notin X \Rightarrow \exists f:X\rightarrow \bigcup X \forall A\in X, f(A)\in A$)
So my question is:
(1) how do i prove that every infinite set has a countable subset?
(2) how do i write down a situation such as: "after choosing $x_1,...,x_k$, choosing $x_k$ satisfying a given condition. Continue this and form a sequence"
 A: You need to find a countable family of non-empty sets that you can choose from.
For the first statement, the answer would require you to find a countable family of subsets which are non-empty. For example $A_n=\{A\subseteq X\mid A\text{ has exactly }n\text{ elements}\}$ is non-empty for $n\in\omega$, because $X$ is assumed to be infinite.
Next we use $\sf AC_\omega$ to claim that there exists $f$ whose domain is $\omega$ such that $f(n)\in A_n$ for every $n>0$. Now we want to claim that the union, $\bigcup\{f(n)\mid n\in\omega\}$ is countably infinite, but this requires us to step through another argument, why is the countable union of finite sets countable. I will let you figure this one out, but let me give you the general hint:
Suppose that $A_n$, for $n\in\omega$ is a family of countable sets, let $F_n$ be the functions of all injections from $A_n$ into $\omega$. Choose $f_n$ from $A_n$, and map the union $\bigcup A_n$ into $\omega\times\omega$, by mapping $A_n$ into $\{n\}\times\omega$, using $f_n$ (note that we didn't assume the $A_n$'s are disjoint, and we don't need to, but this requires another small argument).
The second question, requires a choice principle which is strictly stronger than $\sf AC_\omega$. Namely, the choice of $x_{n+1}$ depends on the choice of $\{x_0,\ldots,x_n\}$. This principle is called Dependent Choice, or $\sf DC$ (or $\sf DC_\omega$ sometimes), and it is formulated in many different ways. One of them is the following:

Suppose that $X$ is a non-empty set and $R$ is a binary relation on $X$ such that $\operatorname{dom}(R)=X$. Then there exists a function $f\colon\omega\to X$ such that $f(n)\mathrel{R}f(n+1)$ for all $n$.

The principle $\sf DC$ is well investigated, it is strictly stronger than $\sf AC_\omega$, and is implied by $\sf AC$ itself, of course. This is essentially a principle allowing us to extend inductive definitions to the existence of a sequence satisfying the conditions we want. So often in contexts where the full axiom of choice is present, because it is so easy to use, we use $\sf DC$ to prove results which only require $\sf AC_\omega$.

Some reading material on these choice principles and finite-ness:
Online discussions:

*

*Infinite Set is Disjoint Union of Two Infinite Sets

*Equivalent of the countable axiom of choice?

*Books on Axiom of Dependent Choices?

*Stronger than ZF, weaker than ZFC

*All naturals are T-finite, all finite sets are T-finite
Research papers:
You may want to check out the references in the above links, but additionally these may come in handy.

*

*Truss, John. "Classes of Dedekind finite cardinals." Fundamenta Mathematicae vol. 84.3 (1974): 187-208.

*Herrlich, Horst. "The finite and the infinite." Appl. Categ. Structures 19 (2011), no. 2, 455–468.

A: Here's an alternative proof that countable choice implies that every infinite set has a countably infinite subset.  Assume countable choice, and let $A$ be an infinite set.  For each natural number $n$ (identified, as usual, with the set $\{0,1,\dots,n-1\}$), let $S_n$ be the set of all one-to-one maps from $n$ into $A$.  The assumption that $A$ is infinite implies (by induction on $n$) that $S_n\neq\varnothing$ for all $n$.  So by countable choice, there is a sequence $(s_n)_{n\in\omega}$ such that $s_n\in S_n$ for al $n$. Now build an infinite sequence of distinct elements of $A$ as the concatenation of sequences $t_n$, where $t_n$ consists of the elements in the range of $s_n$ that are not in the range of any $s_k$ with $k<n$; these elements are to be listed in $t_n$ in the same order as in $s_n$.  Some of the $t_n$ might be empty, but there are infinitely many $n$ for which $t_n$ is nonempty. (Proof: Otherwise, there would be an $m$ such that all $t_n$ for $n>m$ are empty, which means the ranges of all $s_n$'s are included in the union of the ranges of the $s_n$'s for $n\leq m$.  But that union is finite and once $n$ is larger than the cardinality of that union, the range of $s_n$ has too many elements to be included in that union.)  So the concatenation of all the $t_n$'s is an infinite sequence of distinct elements of $A$.
