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 
|- A e. _V
Assertion ranksuc 
|- ( rank ` suc A ) = suc ( rank ` A )

Proof

Step Hyp Ref Expression
1 rankr1b.1 
 |-  A e. _V
2 df-suc 
 |-  suc A = ( A u. { A } )
3 2 fveq2i 
 |-  ( rank ` suc A ) = ( rank ` ( A u. { A } ) )
4 snex 
 |-  { A } e. _V
5 1 4 rankun 
 |-  ( rank ` ( A u. { A } ) ) = ( ( rank ` A ) u. ( rank ` { A } ) )
6 1 ranksn 
 |-  ( rank ` { A } ) = suc ( rank ` A )
7 6 uneq2i 
 |-  ( ( rank ` A ) u. ( rank ` { A } ) ) = ( ( rank ` A ) u. suc ( rank ` A ) )
8 sssucid 
 |-  ( rank ` A ) C_ suc ( rank ` A )
9 ssequn1 
 |-  ( ( rank ` A ) C_ suc ( rank ` A ) <-> ( ( rank ` A ) u. suc ( rank ` A ) ) = suc ( rank ` A ) )
10 8 9 mpbi 
 |-  ( ( rank ` A ) u. suc ( rank ` A ) ) = suc ( rank ` A )
11 7 10 eqtri 
 |-  ( ( rank ` A ) u. ( rank ` { A } ) ) = suc ( rank ` A )
12 5 11 eqtri 
 |-  ( rank ` ( A u. { A } ) ) = suc ( rank ` A )
13 3 12 eqtri 
 |-  ( rank ` suc A ) = suc ( rank ` A )