![]() |
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 9811, rankval2 9813, rankval3 9835, or rankval4 9862 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 9828 illustrates the "inverse" concept. Another nice theorem showing the relationship is rankr1a 9831. (Contributed by NM, 11-Oct-2003.) |
Ref | Expression |
---|---|
df-rank | ⊢ rank = (𝑥 ∈ V ↦ ∩ {𝑦 ∈ On ∣ 𝑥 ∈ (𝑅1‘suc 𝑦)}) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | crnk 9758 | . 2 class rank | |
2 | vx | . . 3 setvar 𝑥 | |
3 | cvv 3475 | . . 3 class V | |
4 | 2 | cv 1541 | . . . . . 6 class 𝑥 |
5 | vy | . . . . . . . . 9 setvar 𝑦 | |
6 | 5 | cv 1541 | . . . . . . . 8 class 𝑦 |
7 | 6 | csuc 6367 | . . . . . . 7 class suc 𝑦 |
8 | cr1 9757 | . . . . . . 7 class 𝑅1 | |
9 | 7, 8 | cfv 6544 | . . . . . 6 class (𝑅1‘suc 𝑦) |
10 | 4, 9 | wcel 2107 | . . . . 5 wff 𝑥 ∈ (𝑅1‘suc 𝑦) |
11 | con0 6365 | . . . . 5 class On | |
12 | 10, 5, 11 | crab 3433 | . . . 4 class {𝑦 ∈ On ∣ 𝑥 ∈ (𝑅1‘suc 𝑦)} |
13 | 12 | cint 4951 | . . 3 class ∩ {𝑦 ∈ On ∣ 𝑥 ∈ (𝑅1‘suc 𝑦)} |
14 | 2, 3, 13 | cmpt 5232 | . 2 class (𝑥 ∈ V ↦ ∩ {𝑦 ∈ On ∣ 𝑥 ∈ (𝑅1‘suc 𝑦)}) |
15 | 1, 14 | wceq 1542 | 1 wff rank = (𝑥 ∈ V ↦ ∩ {𝑦 ∈ On ∣ 𝑥 ∈ (𝑅1‘suc 𝑦)}) |
Colors of variables: wff setvar class |
This definition is referenced by: rankf 9789 rankvalb 9792 |
Copyright terms: Public domain | W3C validator |