Is well-ordered Dedekind-finite set finite?

In $$ZF$$ without any form of $$AC$$, is it true the following statement: "A well-ordered set $$S$$ is Dedekind-infinite iff it is finite" ?

I know that a finite set is always Dedekind-finite, and that if $$AC$$ (or countable choice) holds, then also the converse is true. What about if we have a well-order only on $$S$$?

I think that this is true, as I found here: (i) implies (iv) and in the answer here, but I am looking for a proof. I have the following one: can you confirm that it does not use (even indirectly) $$AC$$ in any point?

Let $$S$$ Dedekind-finite and well ordered. Then it is isomorphic through $$f$$ to a von Neumann ordinal $$\alpha$$. If $$\alpha$$ were not a finite ordinal, then it would contain the least infinite ordinal $$\mathbb{N}$$. But $$\mathbb{N}$$ is Dedekind-infinite and then, by the bijection $$f$$, $$S$$ would contain a Dedekind-infinite subset $$T$$. But this would imply that $$S$$ is Dedekind-infinite, since the non-surjective injection $$\varphi$$ of $$T$$ to all $$S$$ by posing $$\varphi(x)=x$$ for $$x \in S \setminus T$$.

• If $<$ well-orders $S,$ and $S$ is Dedekind-finite then any non-empty $T\subset S$ has a $<$-max member. Otherwise if $f(x)=\min_<\{y\in T: x<y\}$ when $x\in T,$ and $f(x)=x$ when $x \in S$ \ $T$ then $f:S\to S$ is injective with $\min_< T \not \in f[S].$ Commented Mar 27, 2020 at 8:30

For the other direction (which you don't need for this proof), let $$f$$ be a non-surjective injection $$S\to S$$ and let $$x\in S$$ not in its image, and then show that $$\{f^n(x): n\in \omega\}$$ is a countably infinite subset of $$S.$$