Theorem ranksuc

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

	Ref	Expression
Hypothesis	rankr1b.1	$$⊢A\in \mathrm{V}$$
Assertion	ranksuc	$$⊢\mathrm{rank}\left(\mathrm{suc}A\right)=\mathrm{suc}\mathrm{rank}\left(A\right)$$

Proof

Step	Hyp	Ref	Expression
1		rankr1b.1	$$⊢A\in \mathrm{V}$$
2		df-suc	$$⊢\mathrm{suc}A=A\cup \left\{A\right\}$$
3	2	fveq2i	$$⊢\mathrm{rank}\left(\mathrm{suc}A\right)=\mathrm{rank}\left(A\cup \left\{A\right\}\right)$$
4		snex	$$⊢\left\{A\right\}\in \mathrm{V}$$
5	1 4	rankun	$$⊢\mathrm{rank}\left(A\cup \left\{A\right\}\right)=\mathrm{rank}\left(A\right)\cup \mathrm{rank}\left(\left\{A\right\}\right)$$
6	1	ranksn	$$⊢\mathrm{rank}\left(\left\{A\right\}\right)=\mathrm{suc}\mathrm{rank}\left(A\right)$$
7	6	uneq2i	$$⊢\mathrm{rank}\left(A\right)\cup \mathrm{rank}\left(\left\{A\right\}\right)=\mathrm{rank}\left(A\right)\cup \mathrm{suc}\mathrm{rank}\left(A\right)$$
8		sssucid	$$⊢\mathrm{rank}\left(A\right)\subseteq \mathrm{suc}\mathrm{rank}\left(A\right)$$
9		ssequn1	$$⊢\mathrm{rank}\left(A\right)\subseteq \mathrm{suc}\mathrm{rank}\left(A\right)\leftrightarrow \mathrm{rank}\left(A\right)\cup \mathrm{suc}\mathrm{rank}\left(A\right)=\mathrm{suc}\mathrm{rank}\left(A\right)$$
10	8 9	mpbi	$$⊢\mathrm{rank}\left(A\right)\cup \mathrm{suc}\mathrm{rank}\left(A\right)=\mathrm{suc}\mathrm{rank}\left(A\right)$$
11	7 10	eqtri	$$⊢\mathrm{rank}\left(A\right)\cup \mathrm{rank}\left(\left\{A\right\}\right)=\mathrm{suc}\mathrm{rank}\left(A\right)$$
12	5 11	eqtri	$$⊢\mathrm{rank}\left(A\cup \left\{A\right\}\right)=\mathrm{suc}\mathrm{rank}\left(A\right)$$
13	3 12	eqtri	$$⊢\mathrm{rank}\left(\mathrm{suc}A\right)=\mathrm{suc}\mathrm{rank}\left(A\right)$$