This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem rankr1id

Description: The rank of the hierarchy of an ordinal number is itself. (Contributed by NM, 14-Oct-2003) (Revised by Mario Carneiro, 17-Nov-2014)

Ref Expression
Assertion rankr1id 
|- ( A e. dom R1 <-> ( rank ` ( R1 ` A ) ) = A )

Proof

Step Hyp Ref Expression
1 ssid 
 |-  ( R1 ` A ) C_ ( R1 ` A )
2 fvex 
 |-  ( R1 ` A ) e. _V
3 2 pwid 
 |-  ( R1 ` A ) e. ~P ( R1 ` A )
4 r1sucg 
 |-  ( A e. dom R1 -> ( R1 ` suc A ) = ~P ( R1 ` A ) )
5 3 4 eleqtrrid 
 |-  ( A e. dom R1 -> ( R1 ` A ) e. ( R1 ` suc A ) )
6 r1elwf 
 |-  ( ( R1 ` A ) e. ( R1 ` suc A ) -> ( R1 ` A ) e. U. ( R1 " On ) )
7 5 6 syl 
 |-  ( A e. dom R1 -> ( R1 ` A ) e. U. ( R1 " On ) )
8 rankr1bg 
 |-  ( ( ( R1 ` A ) e. U. ( R1 " On ) /\ A e. dom R1 ) -> ( ( R1 ` A ) C_ ( R1 ` A ) <-> ( rank ` ( R1 ` A ) ) C_ A ) )
9 7 8 mpancom 
 |-  ( A e. dom R1 -> ( ( R1 ` A ) C_ ( R1 ` A ) <-> ( rank ` ( R1 ` A ) ) C_ A ) )
10 1 9 mpbii 
 |-  ( A e. dom R1 -> ( rank ` ( R1 ` A ) ) C_ A )
11 rankonid 
 |-  ( A e. dom R1 <-> ( rank ` A ) = A )
12 11 biimpi 
 |-  ( A e. dom R1 -> ( rank ` A ) = A )
13 onssr1 
 |-  ( A e. dom R1 -> A C_ ( R1 ` A ) )
14 rankssb 
 |-  ( ( R1 ` A ) e. U. ( R1 " On ) -> ( A C_ ( R1 ` A ) -> ( rank ` A ) C_ ( rank ` ( R1 ` A ) ) ) )
15 7 13 14 sylc 
 |-  ( A e. dom R1 -> ( rank ` A ) C_ ( rank ` ( R1 ` A ) ) )
16 12 15 eqsstrrd 
 |-  ( A e. dom R1 -> A C_ ( rank ` ( R1 ` A ) ) )
17 10 16 eqssd 
 |-  ( A e. dom R1 -> ( rank ` ( R1 ` A ) ) = A )
18 id 
 |-  ( ( rank ` ( R1 ` A ) ) = A -> ( rank ` ( R1 ` A ) ) = A )
19 rankdmr1 
 |-  ( rank ` ( R1 ` A ) ) e. dom R1
20 18 19 eqeltrrdi 
 |-  ( ( rank ` ( R1 ` A ) ) = A -> A e. dom R1 )
21 17 20 impbii 
 |-  ( A e. dom R1 <-> ( rank ` ( R1 ` A ) ) = A )