I think I finished the following problem with the axiom of dependent choice (a weaker form of AC but still stronger than AC$_\omega$). But I don't know if it is necessary.
Munkres Topology Sec. 10 Prob. 4(a):
Let $A$ be a simply ordered set. Show that $A$ fails to be well-ordered $\implies$ $A$ contains a subset having same order type as $\Bbb{Z}_-$.
PS. The complete problem is to show $\Leftrightarrow$ instead of $\Rightarrow$ , but $\Leftarrow$ is easy. Since $\Bbb{Z}_-$ does not have a least element, an ordered set $S$ which is order isomorphic to $\Bbb{Z}_-$ cannot have a least element. If $S \subseteq A$, then $A$ cannot be well ordered. So the problem is really $\Rightarrow$.
I am referring to the following as the axiom of dependent choice (DC):
If $X$ is a nonempty set and $R$ is an entire relation on $X$, then there is a sequence $(x_n)_{n \in \Bbb{Z}_+}$ in $X$ such that $x_n R x_{n+1}$ for each positive integer $n$.
, where a relation $R$ on $X$ is said to be entire if for all $x \in X$, there is $y \in X$ such that $x Ry$.
Here $\Bbb{Z}_+ = \{1,2,3, \ldots\}$ and $\Bbb{Z}_- = \{ -n \, |\, n \in \Bbb{Z}_+\}$.
Here is my work:
Suppose $(A,\leq)$ fails to be well ordered. Then there is a nonempty subset $S\subseteq A$ such that $S$ does not have a smallest element.
Then the relation $>$ is entire. Pick any $x \in S$. Since $x$ is not a least element of $S$, there is $y \in S$ such that $x > y$. By DC, there is a sequence $(x_n)_{n \in \Bbb{Z}_+}$ in $S$ such that $x_nRx_{n+1}$ for all $n \in \Bbb{Z}_+$.
Let $S'= \{x_n \, |\, n \in \Bbb{Z}_+\}$. $S' \subseteq S \subseteq A$. And I verified that the function $f: \Bbb{Z}_- \to S'$ defined by $f(n) = x_{-n}$, $\forall \ n \in \Bbb{Z}_-$ is an order isomorphism.
So my questions are:
(1) Is DC really necessary for this?
(2) Have I used DC correctly?
Thanks for reading this boring question:)
Yes, the proof you're presenting is in fact using $\sf DC$.
It is consistent that there is a linearly ordered set which is infinite and Dedekind finite. Such set cannot be well-ordered, so the linear order itself is not a well-order; however every countable subset is finite, so there is no copy of the negative integers inside that order.
As for your proof, you should limit $>$ to $S$ explicitly. Otherwise it is not necessarily the case that $>$ has the full domain. For example in $[0,1]$, $0$ is not in the domain of $>$ as it is in fact the minimum element.