Theorem rankval2

Description: Value of an alternate definition of the rank function. Definition of BellMachover p. 478. (Contributed by NM, 8-Oct-2003)

	Ref	Expression
Assertion	rankval2	|- ( A e. B -> ( rank ` A ) = |^| { x e. On | A C_ ( R1 ` x ) } )

Proof

Step	Hyp	Ref	Expression
1		rankvalg	|- ( A e. B -> ( rank ` A ) = |^| { x e. On | A e. ( R1 ` suc x ) } )
2		r1suc	|- ( x e. On -> ( R1 ` suc x ) = ~P ( R1 ` x ) )
3	2	eleq2d	|- ( x e. On -> ( A e. ( R1 ` suc x ) <-> A e. ~P ( R1 ` x ) ) )
4		fvex	|- ( R1 ` x ) e. _V
5	4	elpw2	|- ( A e. ~P ( R1 ` x ) <-> A C_ ( R1 ` x ) )
6	3 5	bitrdi	|- ( x e. On -> ( A e. ( R1 ` suc x ) <-> A C_ ( R1 ` x ) ) )
7	6	rabbiia	|- { x e. On | A e. ( R1 ` suc x ) } = { x e. On | A C_ ( R1 ` x ) }
8	7	inteqi	|- |^| { x e. On | A e. ( R1 ` suc x ) } = |^| { x e. On | A C_ ( R1 ` x ) }
9	1 8	eqtrdi	|- ( A e. B -> ( rank ` A ) = |^| { x e. On | A C_ ( R1 ` x ) } )