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.