Theorem rankvalb

Description: Value of the rank function. Definition 9.14 of TakeutiZaring p. 79 (proved as a theorem from our definition). This variant of rankval does not use Regularity, and so requires the assumption that A is in the range of R1 . (Contributed by NM, 11-Oct-2003) (Revised by Mario Carneiro, 10-Sep-2013)

	Ref	Expression
Assertion	rankvalb	|- ( A e. U. ( R1 " On ) -> ( rank ` A ) = |^| { x e. On | A e. ( R1 ` suc x ) } )

Proof

Step	Hyp	Ref	Expression
1		df-rank	|- rank = ( y e. _V |-> |^| { x e. On | y e. ( R1 ` suc x ) } )
2		eleq1	|- ( y = A -> ( y e. ( R1 ` suc x ) <-> A e. ( R1 ` suc x ) ) )
3	2	rabbidv	|- ( y = A -> { x e. On | y e. ( R1 ` suc x ) } = { x e. On | A e. ( R1 ` suc x ) } )
4	3	inteqd	|- ( y = A -> |^| { x e. On | y e. ( R1 ` suc x ) } = |^| { x e. On | A e. ( R1 ` suc x ) } )
5		elex	|- ( A e. U. ( R1 " On ) -> A e. _V )
6		rankwflemb	|- ( A e. U. ( R1 " On ) <-> E. x e. On A e. ( R1 ` suc x ) )
7		intexrab	|- ( E. x e. On A e. ( R1 ` suc x ) <-> |^| { x e. On | A e. ( R1 ` suc x ) } e. _V )
8	6 7	sylbb	|- ( A e. U. ( R1 " On ) -> |^| { x e. On | A e. ( R1 ` suc x ) } e. _V )
9	1 4 5 8	fvmptd3	|- ( A e. U. ( R1 " On ) -> ( rank ` A ) = |^| { x e. On | A e. ( R1 ` suc x ) } )