Theorem rankidn

Description: A relationship between the rank function and the cumulative hierarchy of sets function R1 . (Contributed by Mario Carneiro, 17-Nov-2014)

	Ref	Expression
Assertion	rankidn	$$⊢A\in \bigcup R_1\left[\mathrm{On}\right]\to \neg A\in R_1\left(\mathrm{rank}\left(A\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢\mathrm{rank}\left(A\right)=\mathrm{rank}\left(A\right)$$
2		rankr1c	$$⊢A\in \bigcup R_1\left[\mathrm{On}\right]\to \left(\mathrm{rank}\left(A\right)=\mathrm{rank}\left(A\right)\leftrightarrow \left(\neg A\in R_1\left(\mathrm{rank}\left(A\right)\right)\wedge A\in R_1\left(\mathrm{suc}\mathrm{rank}\left(A\right)\right)\right)\right)$$
3	1 2	mpbii	$$⊢A\in \bigcup R_1\left[\mathrm{On}\right]\to \left(\neg A\in R_1\left(\mathrm{rank}\left(A\right)\right)\wedge A\in R_1\left(\mathrm{suc}\mathrm{rank}\left(A\right)\right)\right)$$
4	3	simpld	$$⊢A\in \bigcup R_1\left[\mathrm{On}\right]\to \neg A\in R_1\left(\mathrm{rank}\left(A\right)\right)$$