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