Solution (source code)

= Solution

By <choice-function well-ordering construction>, use <transfinite recursion> to choose
$$
x_\beta=f\left(x\setminus\{x_\gamma:\gamma<\beta\}\right)
$$
whenever the set on the right is nonempty. The chosen elements are distinct, so if this construction continued through the <Hartogs theorem> ordinal $h(x)$, the map $\beta\mapsto x_\beta$ would inject $h(x)$ into $x$, a contradiction. It therefore stops at some ordinal $\alpha<h(x)$. At the stopping stage every element of $x$ has been selected, and hence
$$
\beta\longmapsto x_\beta
$$
is a bijection $\alpha\to x$.

Assuming the <axiom of choice>, every set $x$ has such a choice function on its nonempty subsets. Transporting the membership order on $\alpha$ across the bijection well-orders $x$. Thus the axiom of choice implies the <well-ordering theorem>.