Metamath Proof Explorer


Definition df-har

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

Traditionally, the Hartogs number of a set is written aleph ( X ) and the cardinal successor X + ; 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 .

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)

Ref Expression
Assertion df-har har = x V y On | y x

Detailed syntax breakdown

Step Hyp Ref Expression
0 char class har
1 vx setvar x
2 cvv class V
3 vy setvar y
4 con0 class On
5 3 cv setvar y
6 cdom class
7 1 cv setvar x
8 5 7 6 wbr wff y x
9 8 3 4 crab class y On | y x
10 1 2 9 cmpt class x V y On | y x
11 0 10 wceq wff har = x V y On | y x