MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-rank Structured version   Visualization version   GIF version

Definition df-rank 8489
Description: Define the rank function. See rankval 8540, rankval2 8542, rankval3 8564, or rankval4 8591 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 8557 illustrates the "inverse" concept. Another nice theorem showing the relationship is rankr1a 8560. (Contributed by NM, 11-Oct-2003.)
Assertion
Ref Expression
df-rank rank = (𝑥 ∈ V ↦ {𝑦 ∈ On ∣ 𝑥 ∈ (𝑅1‘suc 𝑦)})
Distinct variable group:   𝑥,𝑦

Detailed syntax breakdown of Definition df-rank
StepHypRef Expression
1 crnk 8487 . 2 class rank
2 vx . . 3 setvar 𝑥
3 cvv 3172 . . 3 class V
42cv 1473 . . . . . 6 class 𝑥
5 vy . . . . . . . . 9 setvar 𝑦
65cv 1473 . . . . . . . 8 class 𝑦
76csuc 5628 . . . . . . 7 class suc 𝑦
8 cr1 8486 . . . . . . 7 class 𝑅1
97, 8cfv 5790 . . . . . 6 class (𝑅1‘suc 𝑦)
104, 9wcel 1976 . . . . 5 wff 𝑥 ∈ (𝑅1‘suc 𝑦)
11 con0 5626 . . . . 5 class On
1210, 5, 11crab 2899 . . . 4 class {𝑦 ∈ On ∣ 𝑥 ∈ (𝑅1‘suc 𝑦)}
1312cint 4404 . . 3 class {𝑦 ∈ On ∣ 𝑥 ∈ (𝑅1‘suc 𝑦)}
142, 3, 13cmpt 4637 . 2 class (𝑥 ∈ V ↦ {𝑦 ∈ On ∣ 𝑥 ∈ (𝑅1‘suc 𝑦)})
151, 14wceq 1474 1 wff rank = (𝑥 ∈ V ↦ {𝑦 ∈ On ∣ 𝑥 ∈ (𝑅1‘suc 𝑦)})
Colors of variables: wff setvar class
This definition is referenced by:  rankf  8518  rankvalb  8521
  Copyright terms: Public domain W3C validator