Description: Define the Hartogs
function , which maps all sets to the smallest
ordinal that cannot be injected into the given set. In the important
special case where is an ordinal, this is the
cardinal successor
operation.

Traditionally, the Hartogs number of a set is written ()
and the cardinal successor ; we use functional
notation for
this, and cannot use the aleph symbol because it is taken for the
enumerating function of the infinite initial ordinals df-aleph8342.

Some authors define the Hartogs number of a set to be the least
*infinite* ordinal which does not inject into it, thus causing the range
to consist only of alephs. We use the simpler definition where the
value can be any successor cardinal. (Contributed by Stefan O'Rear,
11-Feb-2015.)