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

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