Theorem rankr1

Description: A relationship between the rank function and the cumulative hierarchy of sets function R1 . Proposition 9.15(2) of TakeutiZaring p. 79. (Contributed by NM, 6-Oct-2003) (Proof shortened by Mario Carneiro, 17-Nov-2014)

	Ref	Expression
Hypothesis	rankid.1	$$⊢A\in \mathrm{V}$$
Assertion	rankr1	$$⊢B=\mathrm{rank}\left(A\right)\leftrightarrow \left(\neg A\in R_1\left(B\right)\wedge A\in R_1\left(\mathrm{suc}B\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		rankid.1	$$⊢A\in \mathrm{V}$$
2		rankr1g	$$⊢A\in \mathrm{V}\to \left(B=\mathrm{rank}\left(A\right)\leftrightarrow \left(\neg A\in R_1\left(B\right)\wedge A\in R_1\left(\mathrm{suc}B\right)\right)\right)$$
3	1 2	ax-mp	$$⊢B=\mathrm{rank}\left(A\right)\leftrightarrow \left(\neg A\in R_1\left(B\right)\wedge A\in R_1\left(\mathrm{suc}B\right)\right)$$