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 9594
Description: Define the Hartogs function as mapping a set to the class of ordinals it dominates. That class is an ordinal by hartogs 9581, which is used in harf 9595.

The Hartogs number of a set is the least ordinal not dominated by that set. Theorem harval2 10034 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 10035.

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 9977.

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 9593 . 2 class har
2 vx . . 3 setvar 𝑥
3 cvv 3477 . . 3 class V
4 vy . . . . . 6 setvar 𝑦
54cv 1535 . . . . 5 class 𝑦
62cv 1535 . . . . 5 class 𝑥
7 cdom 8981 . . . . 5 class
85, 6, 7wbr 5147 . . . 4 wff 𝑦𝑥
9 con0 6385 . . . 4 class On
108, 4, 9crab 3432 . . 3 class {𝑦 ∈ On ∣ 𝑦𝑥}
112, 3, 10cmpt 5230 . 2 class (𝑥 ∈ V ↦ {𝑦 ∈ On ∣ 𝑦𝑥})
121, 11wceq 1536 1 wff har = (𝑥 ∈ V ↦ {𝑦 ∈ On ∣ 𝑦𝑥})
Colors of variables: wff setvar class
This definition is referenced by:  harf  9595  harval  9597
  Copyright terms: Public domain W3C validator