Definition df-rank 8204

Description: Define the rank function. See rankval 8255, rankval2 8257, rankval3 8279, or rankval4 8306 its value. The rank is a kind of "inverse" of the cumulative hierarchy of sets function : 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 8272 illustrates the "inverse" concept. Another nice theorem showing the relationship is rankr1a 8275. (Contributed by NM, 11-Oct-2003.)

Assertion

Ref	Expression
df-rank

Distinct variable group:   ,

Detailed syntax breakdown of Definition df-rank

Step	Hyp	Ref	Expression
1		crnk 8202	. 2
2		vx	. . 3
3		cvv 3109	. . 3
4	2	cv 1394	. . . . . 6
5		vy	. . . . . . . . 9
6	5	cv 1394	. . . . . . . 8
7	6	csuc 4885	. . . . . . 7
8		cr1 8201	. . . . . . 7
9	7, 8	cfv 5593	. . . . . 6
10	4, 9	wcel 1818	. . . . 5
11		con0 4883	. . . . 5
12	10, 5, 11	crab 2811	. . . 4
13	12	cint 4286	. . 3
14	2, 3, 13	cmpt 4510	. 2
15	1, 14	wceq 1395	1

This definition is referenced by:  rankf  8233  rankvalb  8236