Definition df-har 9500

Description: Define the Hartogs function as mapping a set to the class of ordinals it dominates. That class is an ordinal by hartogs 9487, which is used in harf 9501.

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

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

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

Step	Hyp	Ref	Expression
1		char 9499	. 2 class har
2		vx	. . 3 setvar 𝑥
3		cvv 3453	. . 3 class V
4		vy	. . . . . 6 setvar 𝑦
5	4	cv 1558	. . . . 5 class 𝑦
6	2	cv 1558	. . . . 5 class 𝑥
7		cdom 8919	. . . . 5 class ≼
8	5, 6, 7	wbr 5099	. . . 4 wff 𝑦 ≼ 𝑥
9		con0 6340	. . . 4 class On
10	8, 4, 9	crab 3413	. . 3 class {𝑦 ∈ On ∣ 𝑦 ≼ 𝑥}
11	2, 3, 10	cmpt 5180	. 2 class (𝑥 ∈ V ↦ {𝑦 ∈ On ∣ 𝑦 ≼ 𝑥})
12	1, 11	wceq 1559	1 wff har = (𝑥 ∈ V ↦ {𝑦 ∈ On ∣ 𝑦 ≼ 𝑥})

This definition is referenced by:  harf  9501  harval  9503