Theorem rankidn

Description: A relationship between the rank function and the cumulative hierarchy of sets function R1 . (Contributed by Mario Carneiro, 17-Nov-2014)

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

Proof

Step	Hyp	Ref	Expression
1		eqid	|- ( rank ` A ) = ( rank ` A )
2		rankr1c	|- ( A e. U. ( R1 " On ) -> ( ( rank ` A ) = ( rank ` A ) <-> ( -. A e. ( R1 ` ( rank ` A ) ) /\ A e. ( R1 ` suc ( rank ` A ) ) ) ) )
3	1 2	mpbii	|- ( A e. U. ( R1 " On ) -> ( -. A e. ( R1 ` ( rank ` A ) ) /\ A e. ( R1 ` suc ( rank ` A ) ) ) )
4	3	simpld	|- ( A e. U. ( R1 " On ) -> -. A e. ( R1 ` ( rank ` A ) ) )