Theorem r12

Description: Value of the cumulative hierarchy of sets function at 2o . (Contributed by BTernaryTau, 25-Jan-2026)

	Ref	Expression
Assertion	r12	$$⊢R_1\left(2_{𝑜}\right)=2_{𝑜}$$

Proof

Step	Hyp	Ref	Expression
1		df-2o	$$⊢2_{𝑜}=\mathrm{suc}{1}_{𝑜}$$
2	1	fveq2i	$$⊢R_1\left(2_{𝑜}\right)=R_1\left(\mathrm{suc}{1}_{𝑜}\right)$$
3		r1dmlim	$$⊢\mathrm{Lim}\mathrm{dom}{R}_1$$
4		1ellim	$$⊢\mathrm{Lim}\mathrm{dom}{R}_1\to 1_{𝑜}\in \mathrm{dom}{R}_1$$
5		r1sucg	$$⊢1_{𝑜}\in \mathrm{dom}{R}_1\to R_1\left(\mathrm{suc}{1}_{𝑜}\right)=𝒫R_1\left(1_{𝑜}\right)$$
6	3 4 5	mp2b	$$⊢R_1\left(\mathrm{suc}{1}_{𝑜}\right)=𝒫R_1\left(1_{𝑜}\right)$$
7		pwpw0	$$⊢𝒫\left\{\varnothing \right\}=\left\{\varnothing ,\left\{\varnothing \right\}\right\}$$
8		r11	$$⊢R_1\left(1_{𝑜}\right)=1_{𝑜}$$
9		df1o2	$$⊢1_{𝑜}=\left\{\varnothing \right\}$$
10	8 9	eqtri	$$⊢R_1\left(1_{𝑜}\right)=\left\{\varnothing \right\}$$
11	10	pweqi	$$⊢𝒫R_1\left(1_{𝑜}\right)=𝒫\left\{\varnothing \right\}$$
12		df2o2	$$⊢2_{𝑜}=\left\{\varnothing ,\left\{\varnothing \right\}\right\}$$
13	7 11 12	3eqtr4i	$$⊢𝒫R_1\left(1_{𝑜}\right)=2_{𝑜}$$
14	2 6 13	3eqtri	$$⊢R_1\left(2_{𝑜}\right)=2_{𝑜}$$