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 )