With Choice, is any linearly ordered set well-ordered if no subset has order type $\omega^*$? I've been fumbling around with order types and ordinals these past few days. I read about partial, total, and well-ordered structures, and I'm curious to see if a linearly ordered set has no subset with order type $\omega^*$, then it is in fact well ordered. Here $\omega^*$ is the order type of the negative integers.
My idea was this. Let $X$ be some totally ordered set such with subset with order type $\omega^*$. Take any nonempty subset $Y$ of $X$. If $Y$ is finite, it must have a least element, so assume $Y$ is infinite. By way of contradiction, I assume $Y$ has no least element. My strategy was to then somehow construct a subset of $Y$ which has order type $\omega^*$. I do this by first picking an element $a_0$ from $Y$. Since $Y$ has no least element, and since $Y$ is also totally ordered, there must be some other element $a_1\in Y$ such that $a_1\prec a_0$. Again, $a_1$ is not the least element of $Y$, so we can find an element $a_2\in Y$ such that $a_2\prec a_1\prec a_0$. Continuing along, I would eventually have a set $Z=\{\dots,a_3,a_2,a_1,a_0\}$, where I have written it in increasing order. But then $Z$ has order type $\omega^*$, a contradiction.
Does this argument hold up? If so, I feel it is a little handwavey, and the "continuing along" part needs to be formalized. Is there a way to do so with Choice or maybe (transfinite) recursion? I fear I may have written nonsense, as I've done many times in the past. Thanks for any criticism and insights.
 A: Yunone: 
Your argument is fine. The axiom of dependent choices (DC) is what you are using to "recursively" pick the members of your sequence. DC is a consequence of the axiom of choice, but it is strictly weaker. It says that if you have a relation $R$ on a set $X$ with the property that for any $a\in X$ there is a $b\in X$ with $a R b$, then there is a sequence $(a_n\mid n\in\omega)$ with $a_n R a_{n+1}$ for all $n$. 
If you have a set that is not well-ordered, and DC holds, you can pick a nonemepty $X$ subset of your set without a least element and set $aRb$ iff $b<a$. 
DC is strictly weaker than choice, because there are models where DC holds but full choice fails. For example, Shelah built a model of ZF+DC where all sets of reals have the property of Baire. But choice proves that some sets of reals don't have this property.
Actually, DC is an overkill for the result that you are interested in, but some form of choice is needed. The proposition you are considering (a linearly ordered set is well-ordered iff it has no subsets of type $\omega^*$) was first considered by Sierpiński in "L'axiome de M. Zermelo et son rôle dans la théorie des ensembles et l'analyse", Bull. Int. Acad. Sci. Cracovie Cl. Math. Nat., (1918), 97-152. 
This is form 77 in the book by Paul Howard and Jean E. Rubin, "Consequences of the axiom of choice", AMS Mathematical surveys and monographs, vol 59, 1998. The book also provides references to models where this form holds while form 43 (DC) fails, and models where form 77 fails. Another place where some of these examples are discussed is Jech's book "The axiom of choice" (recently reprinted by Dover in 2008). 
Let me point you to a great resource online for choice-related questions: There is a companion webpage to the Howard-Rubin book, Consequences of the Axiom of Choice Project Homepage,  (I have the Howard-Rubin book, but I usually consult the webpage first to identify the forms that I can then go and look for in the book).
A: Your argument is alright. There is nothing wrong with it. It's very common practice -when the axiom of choice is assumed- to say something along the lines of what you wrote. Having said that, here's a couple of ways to "formalize" your argument:
One thing you can do is use the Principle of Dependent Choices: What this says is that if we have a binary relation $E$ on a (nonempty) set $A$ and for every $a\in A$ there is a $b\in A$ such that $bEa$, then there is a sequence $a_0,\ldots,a_n,\ldots$ of elements of $A$ such that $a_{n+1}Ea_n$ for all $n\in\mathbb{N}$. Of course you can see how your argument can be formalized through this principle. Given a subset $Y\subset X$ with no least element of course for every $a\in Y$ there is a $b\in Y$ such that $b<a$. Then by the principle of dependent choice there exists a sequence that defines a set with order-type $\omega^*$.
But assume you just want to use the axiom of choice. We have that $\mathcal{P}(Y)\setminus\{\varnothing\}$ has a choice function $f$. Let $a_0=f(Y)$. Having defined $a_n$, let $Y_{n+1}=\{a\in Y : a<a_n\}$ (these are not empty since $Y$ doesn't have a least element). Then let $a_{n+1}=f(Y_{n+1})$. Every $a_n$ is well defined since $f$ is fixed. Thus the sequence is well defined, and thus the set with order type $\omega^*$ is well defined (these are all results of the recursion theorem).
As you see both "formalizations" are simple. This is why (as I said) your argument is perfectly valid and I am sure that you will encounter it in many books. I just wrote these in case you were curious as to how the axiom of choice leads to the part of your argument that you considered problematic.
