Extracting an infinite subsequence Suppose that $\{a_i\}_{i\in\Bbb N}$ is a sequence of real numbers such that for any $i\in\Bbb N$, there exists $j\in\Bbb N$ with $j>i$ and $a_j>a_i$. How to prove that $\{a_i\}$ contains an infinite monotonically increasing subsequence?
The "standard" argument goes as follows: 

Fix arbitrarily $i_1\in\Bbb N$, then find $i_2>i_1$ with $a_{i_2}>a_{i_1}$ etc; the resulting sequence $\{a_{i_1},a_{i_2},\dotsc\}$ is monotonically increasing. 

While this sounds rather convincing, it does not seem rigorous to me. We actually have never constructed an infinite monotonic subsequence this way, the only thing achieved is constructing finite monotonic subsequences of arbitrary length. Is there a way to convert this argument to a rigorous proof?
I am not interested in alternative "topological" proofs (like using Bolzano-Weierstrass theorem) or deductions from known results (like the infinite Dilworth lemma). What I'd like to have is a direct proof, preferably a variation of that presented above. 
Thanks!
 A: Implicitly this seems to use a weak form of the Axiom of Choice, the (countable) Axiom of Dependent Choice:

(DC) For every set $X\ne\emptyset$ and every relation $R\subseteq X\times X$, if $(\forall x\in X)\,(\exists y)\, R(x,y)$ then there is a sequence $(x_n)_{n\in \Bbb N}$ of elements of $X$ such that $(\forall n\in \Bbb N)\,R(x_n, x_{n+1}).$ 

In the case of your proposition, $X=\Bbb N$, and $R(i,j) \iff a_i < a_j$. DC lets us conclude that there is a sequence $(n_k)_{k\in\Bbb N}$ in $\Bbb N$ such that for all $k$, $R(n_k, n_{k+1})$, which is to say, $a_{n_k}<a_{n_{k+1}}$.
However, DC isn't really needed in this case. Because $X=\Bbb N$, we can define the sequence $(n_k)$ by recursion, using the well-ordering property of $\Bbb N$ to define $n_{k+1}$:


*

*$n_0 = 0$;

*given $n_k$, let $n_{k+1} = $ least integer $j > n_k$ such that $a_j > a_{n_k}$.


Then once again, $(a_{n_k})_{k\in\Bbb N}$ is a monotone strictly increasing subsequence.
A: Note that an infinite sequence in some set $X$ is just a map $\mathbb{N} \to X$. Let $[1,n]$ denote the subset $\{1,2,\dots,n\}$ of $\mathbb{N}$. Now, you say that your proof gives you maps $f_n : [1,n] \to X$, that is, finite sequences, such that $f_n\!\mid_{[1,m]} = f_m$ for all $m \leq n$. But then the map $f: \mathbb{N} \to X$ with $f(n) = f_n(n)$ has the property $f\!\mid_{[1,n]} = f_n$. So in fact, your finite sequences patch together to form an infinite one.
