Theorem rankval

Description: Value of the rank function. Definition 9.14 of TakeutiZaring p. 79 (proved as a theorem from our definition). (Contributed by NM, 24-Sep-2003) (Revised by Mario Carneiro, 10-Sep-2013)

	Ref	Expression
Hypothesis	rankval.1	|- A e. _V
Assertion	rankval	|- ( rank ` A ) = |^| { x e. On | A e. ( R1 ` suc x ) }

Proof

Step	Hyp	Ref	Expression
1		rankval.1	|- A e. _V
2		unir1	|- U. ( R1 " On ) = _V
3	1 2	eleqtrri	|- A e. U. ( R1 " On )
4		rankvalb	|- ( A e. U. ( R1 " On ) -> ( rank ` A ) = |^| { x e. On | A e. ( R1 ` suc x ) } )
5	3 4	ax-mp	|- ( rank ` A ) = |^| { x e. On | A e. ( R1 ` suc x ) }