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