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 ( 𝐴 ∈ 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 ‘ 𝐴 ) ) = 𝐴 )