Metamath Proof Explorer

Theorem rankdmr1

Description: A rank is a member of the cumulative hierarchy. (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 r1funlim 
 |-  ( Fun R1 /\ Lim dom R1 )
5 4 simpri 
 |-  Lim dom R1
6 limsuc 
 |-  ( Lim dom R1 -> ( ( rank ` A ) e. dom R1 <-> suc ( rank ` A ) e. dom R1 ) )
7 5 6 ax-mp 
 |-  ( ( rank ` A ) e. dom R1 <-> suc ( rank ` A ) e. dom R1 )
8 3 7 sylibr 
 |-  ( A e. U. ( R1 " On ) -> ( rank ` A ) e. dom R1 )
9 rankvaln 
 |-  ( -. A e. U. ( R1 " On ) -> ( rank ` A ) = (/) )
10 limomss 
 |-  ( Lim dom R1 -> _om C_ dom R1 )
11 5 10 ax-mp 
 |-  _om C_ dom R1
12 peano1 
 |-  (/) e. _om
13 11 12 sselii 
 |-  (/) e. dom R1
14 9 13 eqeltrdi 
 |-  ( -. A e. U. ( R1 " On ) -> ( rank ` A ) e. dom R1 )
15 8 14 pm2.61i 
 |-  ( rank ` A ) e. dom R1