![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > df-har | Structured version Visualization version GIF version |
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 8804. 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.) |
Ref | Expression |
---|---|
df-har | ⊢ har = (𝑥 ∈ V ↦ {𝑦 ∈ On ∣ 𝑦 ≼ 𝑥}) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | char 8502 | . 2 class har | |
2 | vx | . . 3 setvar 𝑥 | |
3 | cvv 3231 | . . 3 class V | |
4 | vy | . . . . . 6 setvar 𝑦 | |
5 | 4 | cv 1522 | . . . . 5 class 𝑦 |
6 | 2 | cv 1522 | . . . . 5 class 𝑥 |
7 | cdom 7995 | . . . . 5 class ≼ | |
8 | 5, 6, 7 | wbr 4685 | . . . 4 wff 𝑦 ≼ 𝑥 |
9 | con0 5761 | . . . 4 class On | |
10 | 8, 4, 9 | crab 2945 | . . 3 class {𝑦 ∈ On ∣ 𝑦 ≼ 𝑥} |
11 | 2, 3, 10 | cmpt 4762 | . 2 class (𝑥 ∈ V ↦ {𝑦 ∈ On ∣ 𝑦 ≼ 𝑥}) |
12 | 1, 11 | wceq 1523 | 1 wff har = (𝑥 ∈ V ↦ {𝑦 ∈ On ∣ 𝑦 ≼ 𝑥}) |
Colors of variables: wff setvar class |
This definition is referenced by: harf 8506 harval 8508 |
Copyright terms: Public domain | W3C validator |