Metamath Proof Explorer


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