Theorem r1suc

Description: Value of the cumulative hierarchy of sets function at a successor ordinal. Use r1sucg (which does not require ax-rep ) when sufficient. Part of Definition 9.9 of TakeutiZaring p. 76. (Contributed by NM, 2-Sep-2003) (Revised by Mario Carneiro, 10-Sep-2013)

	Ref	Expression
Assertion	r1suc	$$⊢A\in \mathrm{On}\to R_1\left(\mathrm{suc}A\right)=𝒫R_1\left(A\right)$$

Proof

Step	Hyp	Ref	Expression
1		r1sucg	$$⊢A\in \mathrm{dom}{R}_1\to R_1\left(\mathrm{suc}A\right)=𝒫R_1\left(A\right)$$
2		r1fnon	$$⊢R_{1}Fn\mathrm{On}$$
3	2	fndmi	$$⊢\mathrm{dom}{R}_1=\mathrm{On}$$
4	3	eqcomi	$$⊢\mathrm{On}=\mathrm{dom}{R}_1$$
5	1 4	eleq2s	$$⊢A\in \mathrm{On}\to R_1\left(\mathrm{suc}A\right)=𝒫R_1\left(A\right)$$