Theorem r1sssuc

Description: The value of the cumulative hierarchy of sets function is a subset of its value at the successor. JFM CLASSES1 Th. 39. (Contributed by FL, 20-Apr-2011)

	Ref	Expression
Assertion	r1sssuc	$$⊢A\in \mathrm{On}\to R_1\left(A\right)\subseteq R_1\left(\mathrm{suc}A\right)$$

Proof

Step	Hyp	Ref	Expression
1		r1tr	$$⊢\mathrm{Tr}{R}_1\left(A\right)$$
2		dftr4	$$⊢\mathrm{Tr}{R}_1\left(A\right)\leftrightarrow R_1\left(A\right)\subseteq 𝒫R_1\left(A\right)$$
3	1 2	mpbi	$$⊢R_1\left(A\right)\subseteq 𝒫R_1\left(A\right)$$
4		r1suc	$$⊢A\in \mathrm{On}\to R_1\left(\mathrm{suc}A\right)=𝒫R_1\left(A\right)$$
5	3 4	sseqtrrid	$$⊢A\in \mathrm{On}\to R_1\left(A\right)\subseteq R_1\left(\mathrm{suc}A\right)$$