![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > df-rank | Structured version Visualization version GIF version |
Description: Define the rank function. See rankval 9852, rankval2 9854, rankval3 9876, or rankval4 9903 its value. The rank is a kind of "inverse" of the cumulative hierarchy of sets function 𝑅1: given a set, it returns an ordinal number telling us the smallest layer of the hierarchy to which the set belongs. Based on Definition 9.14 of [TakeutiZaring] p. 79. Theorem rankid 9869 illustrates the "inverse" concept. Another nice theorem showing the relationship is rankr1a 9872. (Contributed by NM, 11-Oct-2003.) |
Ref | Expression |
---|---|
df-rank | ⊢ rank = (𝑥 ∈ V ↦ ∩ {𝑦 ∈ On ∣ 𝑥 ∈ (𝑅1‘suc 𝑦)}) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | crnk 9799 | . 2 class rank | |
2 | vx | . . 3 setvar 𝑥 | |
3 | cvv 3462 | . . 3 class V | |
4 | 2 | cv 1533 | . . . . . 6 class 𝑥 |
5 | vy | . . . . . . . . 9 setvar 𝑦 | |
6 | 5 | cv 1533 | . . . . . . . 8 class 𝑦 |
7 | 6 | csuc 6370 | . . . . . . 7 class suc 𝑦 |
8 | cr1 9798 | . . . . . . 7 class 𝑅1 | |
9 | 7, 8 | cfv 6546 | . . . . . 6 class (𝑅1‘suc 𝑦) |
10 | 4, 9 | wcel 2099 | . . . . 5 wff 𝑥 ∈ (𝑅1‘suc 𝑦) |
11 | con0 6368 | . . . . 5 class On | |
12 | 10, 5, 11 | crab 3419 | . . . 4 class {𝑦 ∈ On ∣ 𝑥 ∈ (𝑅1‘suc 𝑦)} |
13 | 12 | cint 4946 | . . 3 class ∩ {𝑦 ∈ On ∣ 𝑥 ∈ (𝑅1‘suc 𝑦)} |
14 | 2, 3, 13 | cmpt 5228 | . 2 class (𝑥 ∈ V ↦ ∩ {𝑦 ∈ On ∣ 𝑥 ∈ (𝑅1‘suc 𝑦)}) |
15 | 1, 14 | wceq 1534 | 1 wff rank = (𝑥 ∈ V ↦ ∩ {𝑦 ∈ On ∣ 𝑥 ∈ (𝑅1‘suc 𝑦)}) |
Colors of variables: wff setvar class |
This definition is referenced by: rankf 9830 rankvalb 9833 |
Copyright terms: Public domain | W3C validator |