Metamath Proof Explorer


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 ) } )