Theorem r1rankidb

Description: Any set is a subset of the hierarchy of its rank. (Contributed by Mario Carneiro, 3-Jun-2013) (Revised by Mario Carneiro, 17-Nov-2014)

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

Proof

Step	Hyp	Ref	Expression
1		ssid	|- ( rank ` A ) C_ ( rank ` A )
2		rankdmr1	|- ( rank ` A ) e. dom R1
3		rankr1bg	|- ( ( A e. U. ( R1 " On ) /\ ( rank ` A ) e. dom R1 ) -> ( A C_ ( R1 ` ( rank ` A ) ) <-> ( rank ` A ) C_ ( rank ` A ) ) )
4	2 3	mpan2	|- ( A e. U. ( R1 " On ) -> ( A C_ ( R1 ` ( rank ` A ) ) <-> ( rank ` A ) C_ ( rank ` A ) ) )
5	1 4	mpbiri	|- ( A e. U. ( R1 " On ) -> A C_ ( R1 ` ( rank ` A ) ) )