Given a choice function on all nonempty subsets of , recursively choose the next point from the complement of all earlier choices. Hartogs theorem forces the recursion to exhaust before it defines an injection from into , producing a bijection from an ordinal to .
Codex Wiki