Metamath Proof Explorer

Theorem rankvalg

Description: Value of the rank function. Definition 9.14 of TakeutiZaring p. 79 (proved as a theorem from our definition). This variant of rankval expresses the class existence requirement as an antecedent instead of a hypothesis. (Contributed by NM, 5-Oct-2003)

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

Proof

Step Hyp Ref Expression
1 fveq2 
 |-  ( y = A -> ( rank ` y ) = ( rank ` A ) )
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 1 4 eqeq12d 
 |-  ( y = A -> ( ( rank ` y ) = |^| { x e. On | y e. ( R1 ` suc x ) } <-> ( rank ` A ) = |^| { x e. On | A e. ( R1 ` suc x ) } ) )
6 vex 
 |-  y e. _V
7 6 rankval 
 |-  ( rank ` y ) = |^| { x e. On | y e. ( R1 ` suc x ) }
8 5 7 vtoclg 
 |-  ( A e. V -> ( rank ` A ) = |^| { x e. On | A e. ( R1 ` suc x ) } )