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

Metamath Proof Explorer

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