Set Theory - Prove that there is a function $f:\omega\to X$ such that $f(n)
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?
 A: 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.
A: (1). A binary relation on $S$ is any subset of $S\times S.$ When $B\subset S\times S$ then dom$(B)=\{x\in S:\exists y\; ((x,y)\in B\}.$ The Axiom of Dependent Choice,which is a corollary of the Axiom of Choice,is : When $B$ is a binary relation on $S$ with dom$(B)=S,$ and $x\in S,$ there exists a function $f:\omega\to S$ with $f(0)=x$ and $\forall n\in \omega\; (f(n),f(n+1))\in B).$
Applying this with $X=S$ and with $(x,y)\in B\iff x<y$ gives the answer immediately, since $<$ is transitive. 
(2). There are so many statements that have been shown to be equivalent to AC that different authors choose different versions. Kunen,in "Set Theory: An Introduction To Independence Proofs", uses "Every set can be well-ordered." 
Suppose $<_W$ is a well-order on $X.$ Let $x_0=\min_{<_W}X$ and let $x_{n+1}=\min_{<_W}\{y:x_n<_Wy\}.$ Note that although this uses recursion, and recursion does not require AC,  we cannot define the recursion  without $<_W,$ and we need AC to get $<_W .$  
