Codex Wiki OurBigBook logoOurBigBook.comSite Source code
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 .

Ancestors (7)

  1. Well-ordering theorem
  2. Axiom of choice
  3. Set theory
  4. Foundations of mathematics
  5. Area of mathematics
  6. Mathematics
  7. Home