Choice-function well-ordering construction
= Choice-function well-ordering construction
Given a choice function on all nonempty subsets of $X$, recursively choose the next point from the complement of all earlier choices. <Hartogs theorem> forces the recursion to exhaust $X$ before it defines an injection from $h(X)$ into $X$, producing a bijection from an ordinal to $X$.