Suppose that $X$ is non-empty strictly ordered set, and that $X$ has no maximal element in a sense that for every $x\in X$ there exist $y\in X$ such that $x<y$. By using AC, show that there exists a function from $\omega$ to $ X$ such that $f(n)<f(n^{+})$ for all $n\in \omega$:
I think it's intuitively clear that such function exist. Since $X$ is non-empty we can pick an element $x_0\in X$. Then maximality condition asserts that there exist $x_1$ such that $x_0<x_1$, and iteratively we can find $x_0<x_1<x_2<\cdots$. So (informally?) defining $f(n)=x_n$ will do.
However, I do not see why above argument requires axiom of choice. What part of it invokes AC/or what part of it is not rigourosly correct?
In order to simplify my answer, let us assume that $\operatorname{ZF}$ is consistent.
The axiom of dependent choice (DC) is the following statement:
Whenever $X$ is a nonempty set and $\prec \subseteq X \times X$ is a relation such that for all $x \in X$ there is some $y \in X$ with $x \prec y$, then there is a function $f \colon \omega \to X$ such that for all $n < \omega \colon f(n) \prec f(n+1)$.
It's an easy exercise to prove that $\operatorname{ZFC}$ proves $DC$. On the other hand, one can show that $\operatorname{ZF}$ doesn't prove $DC$ and also that $\operatorname{ZF + DC}$ doesn't prove the axiom of choice. Thus $DC$ can be regarded as "a weak form of choice".
Instead of only considering total orders, I want to allow partial orders as well.
Let $(X, \prec)$ be a strict (partial) order without maximal element. Then $\prec \subseteq X \times X$ satisfies the requirements of $(DC)$. Thus, if $DC$ is true, there is a function $f \colon \omega \to X$ such that $f(n) \prec f(n+1)$ for all $n < \omega$.
I claim that $DC$ is necessary in order to obtain this result in general: Suppose that $DC$ fails. Let $X$ be a nonempty set and let $\prec \subseteq X \times X$ be a relation such that for all $x \in X$ there is some $y \in X$ with $x \prec y$, but there is no function $f \colon \omega \to X$ with $f(n) \prec f(n+1)$ for all $n < \omega$. Let $Y$ be the set of all functions $g \colon k \to X$ such that $k < \omega$ and $g(n) \prec g(n+1)$ for all $n+1 < k$. Then $(Y, \subsetneq)$ is a strict partial partial order without maximal element. By our assumption there is a function $h \colon \omega \to Y$ such that $h(n) \subsetneq h(n+1)$ for all $n < \omega$. Let $x_n$ be the last element of $h(n)$. So if $h(n) \colon k \to X$, then $x_n = h(n)(k-1)$. Now $f \colon \omega \to X, n \mapsto x_n$ satisfies $f(n) \prec f(n+1)$ for all $n < \omega$ - contradicting our choice of $(X, \prec)$.
Therefore the assumption that every strict partial order $(X, \prec)$ without maximal element admits a function $f \colon \omega \to X$ with $f(n) \prec f(n+1)$ for all $n < \omega$ implies the axiom of dependent choice.