Theorem r11

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

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

Proof

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