Definition df-rank 4790

Description: Define the rank function. See rankval 4814, rankval2 4816, rankval3 4827, or rankval4 4848 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 4818 illustrates the "inverse" concept. Another nice theorem showing the relationship is rankr1a 4823.

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 4788	. 2 class rank
2		vy	. . . . 5 set y
3	2	cv 991	. . . 4 class y
4		vx	. . . . . . . 8 set x
5	4	cv 991	. . . . . . 7 class x
6		vz	. . . . . . . . . 10 set z
7	6	cv 991	. . . . . . . . 9 class z
8	7	csuc 2977	. . . . . . . 8 class suc z
9		cr1 4787	. . . . . . . 8 class R1
10	8, 9	cfv 3263	. . . . . . 7 class (R1` suc z)
11	5, 10	wcel 994	. . . . . 6 wff x e. (R1` suc z)
12		con0 2975	. . . . . 6 class On
13	11, 6, 12	crab 1694	. . . . 5 class {z e. On | x e. (R1` suc z)}
14	13	cint 2600	. . . 4 class |^|{z e. On | x e. (R1` suc z)}
15	3, 14	wceq 992	. . 3 wff y = |^|{z e. On | x e. (R1` suc z)}
16	15, 4, 2	copab 2740	. 2 class {<.x, y>. | y = |^|{z e. On | x e. (R1` suc z)}}
17	1, 16	wceq 992	1 wff rank = {<.x, y>. | y = |^|{z e. On | x e. (R1` suc z)}}

This definition is referenced by:  rankval 4814

Copyright terms: Public domain