Definition df-rank 5751

Description: Define the rank function. See rankval 5779, rankval2 5781, rankval3 5792, or rankval4 5813 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 5783 illustrates the "inverse" concept. Another nice theorem showing the relationship is rankr1a 5788.

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 5749	. 2 class rank
2		vy	. . . . 5 set y
3	2	cv 1297	. . . 4 class y
4		vx	. . . . . . . 8 set x
5	4	cv 1297	. . . . . . 7 class x
6		vz	. . . . . . . . . 10 set z
7	6	cv 1297	. . . . . . . . 9 class z
8	7	csuc 3659	. . . . . . . 8 class suc z
9		cr1 5748	. . . . . . . 8 class R1
10	8, 9	cfv 3998	. . . . . . 7 class (R1` suc z)
11	5, 10	wcel 1300	. . . . . 6 wff x e. (R1` suc z)
12		con0 3657	. . . . . 6 class On
13	11, 6, 12	crab 2108	. . . . 5 class {z e. On | x e. (R1` suc z)}
14	13	cint 3214	. . . 4 class |^|{z e. On | x e. (R1` suc z)}
15	3, 14	wceq 1298	. . 3 wff y = |^|{z e. On | x e. (R1` suc z)}
16	15, 4, 2	copab 3395	. 2 class {<.x, y>. | y = |^|{z e. On | x e. (R1` suc z)}}
17	1, 16	wceq 1298	1 wff rank = {<.x, y>. | y = |^|{z e. On | x e. (R1` suc z)}}

This definition is referenced by:  rankval 5779

Copyright terms: Public domain