Definition df-har 8346

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

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 8344	. 2 class har
2		vx	. . 3 setvar 𝑥
3		cvv 3173	. . 3 class V
4		vy	. . . . . 6 setvar 𝑦
5	4	cv 1474	. . . . 5 class 𝑦
6	2	cv 1474	. . . . 5 class 𝑥
7		cdom 7839	. . . . 5 class ≼
8	5, 6, 7	wbr 4583	. . . 4 wff 𝑦 ≼ 𝑥
9		con0 5640	. . . 4 class On
10	8, 4, 9	crab 2900	. . 3 class {𝑦 ∈ On ∣ 𝑦 ≼ 𝑥}
11	2, 3, 10	cmpt 4643	. 2 class (𝑥 ∈ V ↦ {𝑦 ∈ On ∣ 𝑦 ≼ 𝑥})
12	1, 11	wceq 1475	1 wff har = (𝑥 ∈ V ↦ {𝑦 ∈ On ∣ 𝑦 ≼ 𝑥})

This definition is referenced by:  harf  8348  harval  8350