Metamath Proof Explorer

Theorem rankdmr1

Description: A rank is a member of the cumulative hierarchy of sets. (Contributed by Mario Carneiro, 17-Nov-2014)

Ref Expression
Assertion rankdmr1 
|- ( rank ` A ) e. dom R1

Proof

Step Hyp Ref Expression
1 rankidb 
 |-  ( A e. U. ( R1 " On ) -> A e. ( R1 ` suc ( rank ` A ) ) )
2 elfvdm 
 |-  ( A e. ( R1 ` suc ( rank ` A ) ) -> suc ( rank ` A ) e. dom R1 )
3 1 2 syl 
 |-  ( A e. U. ( R1 " On ) -> suc ( rank ` A ) e. dom R1 )
4 r1dmlim 
 |-  Lim dom R1
5 limsuc 
 |-  ( Lim dom R1 -> ( ( rank ` A ) e. dom R1 <-> suc ( rank ` A ) e. dom R1 ) )
6 4 5 ax-mp 
 |-  ( ( rank ` A ) e. dom R1 <-> suc ( rank ` A ) e. dom R1 )
7 3 6 sylibr 
 |-  ( A e. U. ( R1 " On ) -> ( rank ` A ) e. dom R1 )
8 rankvaln 
 |-  ( -. A e. U. ( R1 " On ) -> ( rank ` A ) = (/) )
9 limomss 
 |-  ( Lim dom R1 -> _om C_ dom R1 )
10 4 9 ax-mp 
 |-  _om C_ dom R1
11 peano1 
 |-  (/) e. _om
12 10 11 sselii 
 |-  (/) e. dom R1
13 8 12 eqeltrdi 
 |-  ( -. A e. U. ( R1 " On ) -> ( rank ` A ) e. dom R1 )
14 7 13 pm2.61i 
 |-  ( rank ` A ) e. dom R1