Description: Define the Hartogs
function as mapping a set to the class of ordinals it
dominates. That class is an ordinal by hartogs 9312, which is used in
harf 9326.
The Hartogs number of a set is the least ordinal not dominated by
that
set. Theorem harval2 9764 proves that the Hartogs function actually
gives
the Hartogs number for well-orderable sets.
The Hartogs number of an ordinal is its cardinal successor. This is
proved for finite ordinal in harsucnn 9765.
Traditionally, the Hartogs number of a set 𝑋 is written
ℵ(𝑋), and its 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-aleph 9707.
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.) |