Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-har Structured version   Unicode version

Definition df-har 7555
 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-aleph 7858. 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.)
Assertion
Ref Expression
df-har har
Distinct variable group:   ,

Detailed syntax breakdown of Definition df-har
StepHypRef Expression
1 char 7553 . 2 har
2 vx . . 3
3 cvv 2962 . . 3
4 vy . . . . . 6
54cv 1652 . . . . 5
62cv 1652 . . . . 5
7 cdom 7136 . . . . 5
85, 6, 7wbr 4237 . . . 4
9 con0 4610 . . . 4
108, 4, 9crab 2715 . . 3
112, 3, 10cmpt 4291 . 2
121, 11wceq 1653 1 har
 Colors of variables: wff set class This definition is referenced by:  harf  7557  harval  7559
 Copyright terms: Public domain W3C validator