Metamath Proof Explorer


Theorem rankidb

Description: Identity law for the rank function. (Contributed by NM, 3-Oct-2003) (Revised by Mario Carneiro, 22-Mar-2013)

Ref Expression
Assertion rankidb
|- ( A e. U. ( R1 " On ) -> A e. ( R1 ` suc ( rank ` A ) ) )

Proof

Step Hyp Ref Expression
1 rankwflemb
 |-  ( A e. U. ( R1 " On ) <-> E. x e. On A e. ( R1 ` suc x ) )
2 nfcv
 |-  F/_ x R1
3 nfrab1
 |-  F/_ x { x e. On | A e. ( R1 ` suc x ) }
4 3 nfint
 |-  F/_ x |^| { x e. On | A e. ( R1 ` suc x ) }
5 4 nfsuc
 |-  F/_ x suc |^| { x e. On | A e. ( R1 ` suc x ) }
6 2 5 nffv
 |-  F/_ x ( R1 ` suc |^| { x e. On | A e. ( R1 ` suc x ) } )
7 6 nfel2
 |-  F/ x A e. ( R1 ` suc |^| { x e. On | A e. ( R1 ` suc x ) } )
8 suceq
 |-  ( x = |^| { x e. On | A e. ( R1 ` suc x ) } -> suc x = suc |^| { x e. On | A e. ( R1 ` suc x ) } )
9 8 fveq2d
 |-  ( x = |^| { x e. On | A e. ( R1 ` suc x ) } -> ( R1 ` suc x ) = ( R1 ` suc |^| { x e. On | A e. ( R1 ` suc x ) } ) )
10 9 eleq2d
 |-  ( x = |^| { x e. On | A e. ( R1 ` suc x ) } -> ( A e. ( R1 ` suc x ) <-> A e. ( R1 ` suc |^| { x e. On | A e. ( R1 ` suc x ) } ) ) )
11 7 10 onminsb
 |-  ( E. x e. On A e. ( R1 ` suc x ) -> A e. ( R1 ` suc |^| { x e. On | A e. ( R1 ` suc x ) } ) )
12 1 11 sylbi
 |-  ( A e. U. ( R1 " On ) -> A e. ( R1 ` suc |^| { x e. On | A e. ( R1 ` suc x ) } ) )
13 rankvalb
 |-  ( A e. U. ( R1 " On ) -> ( rank ` A ) = |^| { x e. On | A e. ( R1 ` suc x ) } )
14 suceq
 |-  ( ( rank ` A ) = |^| { x e. On | A e. ( R1 ` suc x ) } -> suc ( rank ` A ) = suc |^| { x e. On | A e. ( R1 ` suc x ) } )
15 13 14 syl
 |-  ( A e. U. ( R1 " On ) -> suc ( rank ` A ) = suc |^| { x e. On | A e. ( R1 ` suc x ) } )
16 15 fveq2d
 |-  ( A e. U. ( R1 " On ) -> ( R1 ` suc ( rank ` A ) ) = ( R1 ` suc |^| { x e. On | A e. ( R1 ` suc x ) } ) )
17 12 16 eleqtrrd
 |-  ( A e. U. ( R1 " On ) -> A e. ( R1 ` suc ( rank ` A ) ) )