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 )