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 ‘ 𝐴 )