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

Metamath Proof Explorer

Theorem ranksuc

Description: The rank of a successor. (Contributed by NM, 18-Sep-2006)

Ref Expression
Hypothesis rankr1b.1 ⊢ 𝐴 ∈ V
Assertion ranksuc ( rank ‘ suc 𝐴 ) = suc ( rank ‘ 𝐴 )

Proof

Step Hyp Ref Expression
1 rankr1b.1 ⊢ 𝐴 ∈ V
2 df-suc ⊢ suc 𝐴 = ( 𝐴 ∪ { 𝐴 } )
3 2 fveq2i ⊢ ( rank ‘ suc 𝐴 ) = ( rank ‘ ( 𝐴 ∪ { 𝐴 } ) )
4 snex ⊢ { 𝐴 } ∈ V
5 1 4 rankun ⊢ ( rank ‘ ( 𝐴 ∪ { 𝐴 } ) ) = ( ( rank ‘ 𝐴 ) ∪ ( rank ‘ { 𝐴 } ) )
6 1 ranksn ⊢ ( rank ‘ { 𝐴 } ) = suc ( rank ‘ 𝐴 )
7 6 uneq2i ⊢ ( ( rank ‘ 𝐴 ) ∪ ( rank ‘ { 𝐴 } ) ) = ( ( rank ‘ 𝐴 ) ∪ suc ( rank ‘ 𝐴 ) )
8 sssucid ⊢ ( rank ‘ 𝐴 ) ⊆ suc ( rank ‘ 𝐴 )
9 ssequn1 ⊢ ( ( rank ‘ 𝐴 ) ⊆ suc ( rank ‘ 𝐴 ) ↔ ( ( rank ‘ 𝐴 ) ∪ suc ( rank ‘ 𝐴 ) ) = suc ( rank ‘ 𝐴 ) )
10 8 9 mpbi ⊢ ( ( rank ‘ 𝐴 ) ∪ suc ( rank ‘ 𝐴 ) ) = suc ( rank ‘ 𝐴 )
11 7 10 eqtri ⊢ ( ( rank ‘ 𝐴 ) ∪ ( rank ‘ { 𝐴 } ) ) = suc ( rank ‘ 𝐴 )
12 5 11 eqtri ⊢ ( rank ‘ ( 𝐴 ∪ { 𝐴 } ) ) = suc ( rank ‘ 𝐴 )
13 3 12 eqtri ⊢ ( rank ‘ suc 𝐴 ) = suc ( rank ‘ 𝐴 )