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	⊢ ( 𝐴 ∈ dom 𝑅1 ↔ ( rank ‘ ( 𝑅1 ‘ 𝐴 ) ) = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		ssid	⊢ ( 𝑅1 ‘ 𝐴 ) ⊆ ( 𝑅1 ‘ 𝐴 )
2		fvex	⊢ ( 𝑅1 ‘ 𝐴 ) ∈ V
3	2	pwid	⊢ ( 𝑅1 ‘ 𝐴 ) ∈ 𝒫 ( 𝑅1 ‘ 𝐴 )
4		r1sucg	⊢ ( 𝐴 ∈ dom 𝑅1 → ( 𝑅1 ‘ suc 𝐴 ) = 𝒫 ( 𝑅1 ‘ 𝐴 ) )
5	3 4	eleqtrrid	⊢ ( 𝐴 ∈ dom 𝑅1 → ( 𝑅1 ‘ 𝐴 ) ∈ ( 𝑅1 ‘ suc 𝐴 ) )
6		r1elwf	⊢ ( ( 𝑅1 ‘ 𝐴 ) ∈ ( 𝑅1 ‘ suc 𝐴 ) → ( 𝑅1 ‘ 𝐴 ) ∈ ∪ ( 𝑅1 “ On ) )
7	5 6	syl	⊢ ( 𝐴 ∈ dom 𝑅1 → ( 𝑅1 ‘ 𝐴 ) ∈ ∪ ( 𝑅1 “ On ) )
8		rankr1bg	⊢ ( ( ( 𝑅1 ‘ 𝐴 ) ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐴 ∈ dom 𝑅1 ) → ( ( 𝑅1 ‘ 𝐴 ) ⊆ ( 𝑅1 ‘ 𝐴 ) ↔ ( rank ‘ ( 𝑅1 ‘ 𝐴 ) ) ⊆ 𝐴 ) )
9	7 8	mpancom	⊢ ( 𝐴 ∈ dom 𝑅1 → ( ( 𝑅1 ‘ 𝐴 ) ⊆ ( 𝑅1 ‘ 𝐴 ) ↔ ( rank ‘ ( 𝑅1 ‘ 𝐴 ) ) ⊆ 𝐴 ) )
10	1 9	mpbii	⊢ ( 𝐴 ∈ dom 𝑅1 → ( rank ‘ ( 𝑅1 ‘ 𝐴 ) ) ⊆ 𝐴 )
11		rankonid	⊢ ( 𝐴 ∈ dom 𝑅1 ↔ ( rank ‘ 𝐴 ) = 𝐴 )
12	11	biimpi	⊢ ( 𝐴 ∈ dom 𝑅1 → ( rank ‘ 𝐴 ) = 𝐴 )
13		onssr1	⊢ ( 𝐴 ∈ dom 𝑅1 → 𝐴 ⊆ ( 𝑅1 ‘ 𝐴 ) )
14		rankssb	⊢ ( ( 𝑅1 ‘ 𝐴 ) ∈ ∪ ( 𝑅1 “ On ) → ( 𝐴 ⊆ ( 𝑅1 ‘ 𝐴 ) → ( rank ‘ 𝐴 ) ⊆ ( rank ‘ ( 𝑅1 ‘ 𝐴 ) ) ) )
15	7 13 14	sylc	⊢ ( 𝐴 ∈ dom 𝑅1 → ( rank ‘ 𝐴 ) ⊆ ( rank ‘ ( 𝑅1 ‘ 𝐴 ) ) )
16	12 15	eqsstrrd	⊢ ( 𝐴 ∈ dom 𝑅1 → 𝐴 ⊆ ( rank ‘ ( 𝑅1 ‘ 𝐴 ) ) )
17	10 16	eqssd	⊢ ( 𝐴 ∈ dom 𝑅1 → ( rank ‘ ( 𝑅1 ‘ 𝐴 ) ) = 𝐴 )
18		id	⊢ ( ( rank ‘ ( 𝑅1 ‘ 𝐴 ) ) = 𝐴 → ( rank ‘ ( 𝑅1 ‘ 𝐴 ) ) = 𝐴 )
19		rankdmr1	⊢ ( rank ‘ ( 𝑅1 ‘ 𝐴 ) ) ∈ dom 𝑅1
20	18 19	eqeltrrdi	⊢ ( ( rank ‘ ( 𝑅1 ‘ 𝐴 ) ) = 𝐴 → 𝐴 ∈ dom 𝑅1 )
21	17 20	impbii	⊢ ( 𝐴 ∈ dom 𝑅1 ↔ ( rank ‘ ( 𝑅1 ‘ 𝐴 ) ) = 𝐴 )