Definition df-rank 4616

Description: Define the rank function. See rankval 4640, rankval2 4642, rankval3 4653, or rankval4 4674 its value. The rank is a kind of "inverse" of the cumulative hierarchy of sets function R1: 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 4644 illustrates the "inverse" concept. Another nice theorem showing the relationship is rankr1a 4649.

Assertion

Ref	Expression
df-rank	|- rank = {<.x, y>. | y = |^|{z e. On | x e. (R1` suc z)}}

Distinct variable group:   x,y,z

Detailed syntax breakdown of Definition df-rank

Step	Hyp	Ref	Expression
1		crnk 4614	. 2 class rank
2		vy	. . . . 5 set y
3	2	cv 952	. . . 4 class y
4		vx	. . . . . . . 8 set x
5	4	cv 952	. . . . . . 7 class x
6		vz	. . . . . . . . . 10 set z
7	6	cv 952	. . . . . . . . 9 class z
8	7	csuc 2940	. . . . . . . 8 class suc z
9		cr1 4613	. . . . . . . 8 class R1
10	8, 9	cfv 3172	. . . . . . 7 class (R1` suc z)
11	5, 10	wcel 955	. . . . . 6 wff x e. (R1` suc z)
12		con0 2938	. . . . . 6 class On
13	11, 6, 12	crab 1640	. . . . 5 class {z e. On | x e. (R1` suc z)}
14	13	cint 2523	. . . 4 class |^|{z e. On | x e. (R1` suc z)}
15	3, 14	wceq 953	. . 3 wff y = |^|{z e. On | x e. (R1` suc z)}
16	15, 4, 2	copab 2656	. 2 class {<.x, y>. | y = |^|{z e. On | x e. (R1` suc z)}}
17	1, 16	wceq 953	1 wff rank = {<.x, y>. | y = |^|{z e. On | x e. (R1` suc z)}}

This definition is referenced by:  rankval 4640

Copyright terms: Public domain