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

Definition df-har 9016
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 9363.

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 = (𝑥 ∈ V ↦ {𝑦 ∈ On ∣ 𝑦𝑥})
Distinct variable group:   𝑥,𝑦

Detailed syntax breakdown of Definition df-har
StepHypRef Expression
1 char 9014 . 2 class har
2 vx . . 3 setvar 𝑥
3 cvv 3500 . . 3 class V
4 vy . . . . . 6 setvar 𝑦
54cv 1529 . . . . 5 class 𝑦
62cv 1529 . . . . 5 class 𝑥
7 cdom 8501 . . . . 5 class
85, 6, 7wbr 5063 . . . 4 wff 𝑦𝑥
9 con0 6190 . . . 4 class On
108, 4, 9crab 3147 . . 3 class {𝑦 ∈ On ∣ 𝑦𝑥}
112, 3, 10cmpt 5143 . 2 class (𝑥 ∈ V ↦ {𝑦 ∈ On ∣ 𝑦𝑥})
121, 11wceq 1530 1 wff har = (𝑥 ∈ V ↦ {𝑦 ∈ On ∣ 𝑦𝑥})
Colors of variables: wff setvar class
This definition is referenced by:  harf  9018  harval  9020
  Copyright terms: Public domain W3C validator