This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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