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		r1funlim	$$⊢\left(\mathrm{Fun}{R}_1\wedge \mathrm{Lim}\mathrm{dom}{R}_1\right)$$
4	3	simpri	$$⊢\mathrm{Lim}\mathrm{dom}{R}_1$$
5		1ellim	$$⊢\mathrm{Lim}\mathrm{dom}{R}_1\to 1_{𝑜}\in \mathrm{dom}{R}_1$$
6		r1sucg	$$⊢1_{𝑜}\in \mathrm{dom}{R}_1\to R_1\left(\mathrm{suc}{1}_{𝑜}\right)=𝒫R_1\left(1_{𝑜}\right)$$
7	4 5 6	mp2b	$$⊢R_1\left(\mathrm{suc}{1}_{𝑜}\right)=𝒫R_1\left(1_{𝑜}\right)$$
8		pwpw0	$$⊢𝒫\left\{\varnothing \right\}=\left\{\varnothing ,\left\{\varnothing \right\}\right\}$$
9		r11	$$⊢R_1\left(1_{𝑜}\right)=1_{𝑜}$$
10		df1o2	$$⊢1_{𝑜}=\left\{\varnothing \right\}$$
11	9 10	eqtri	$$⊢R_1\left(1_{𝑜}\right)=\left\{\varnothing \right\}$$
12	11	pweqi	$$⊢𝒫R_1\left(1_{𝑜}\right)=𝒫\left\{\varnothing \right\}$$
13		df2o2	$$⊢2_{𝑜}=\left\{\varnothing ,\left\{\varnothing \right\}\right\}$$
14	8 12 13	3eqtr4i	$$⊢𝒫R_1\left(1_{𝑜}\right)=2_{𝑜}$$
15	2 7 14	3eqtri	$$⊢R_1\left(2_{𝑜}\right)=2_{𝑜}$$