Theorem r11

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

	Ref	Expression
Assertion	r11	⊢ ( 𝑅1 ‘ 1o ) = 1o

Proof

Step	Hyp	Ref	Expression
1		df-1o	⊢ 1o = suc ∅
2	1	fveq2i	⊢ ( 𝑅1 ‘ 1o ) = ( 𝑅1 ‘ suc ∅ )
3		r1funlim	⊢ ( Fun 𝑅1 ∧ Lim dom 𝑅1 )
4	3	simpri	⊢ Lim dom 𝑅1
5		0ellim	⊢ ( Lim dom 𝑅1 → ∅ ∈ dom 𝑅1 )
6		r1sucg	⊢ ( ∅ ∈ dom 𝑅1 → ( 𝑅1 ‘ suc ∅ ) = 𝒫 ( 𝑅1 ‘ ∅ ) )
7	4 5 6	mp2b	⊢ ( 𝑅1 ‘ suc ∅ ) = 𝒫 ( 𝑅1 ‘ ∅ )
8		pw0	⊢ 𝒫 ∅ = { ∅ }
9		r10	⊢ ( 𝑅1 ‘ ∅ ) = ∅
10	9	pweqi	⊢ 𝒫 ( 𝑅1 ‘ ∅ ) = 𝒫 ∅
11		df1o2	⊢ 1o = { ∅ }
12	8 10 11	3eqtr4i	⊢ 𝒫 ( 𝑅1 ‘ ∅ ) = 1o
13	2 7 12	3eqtri	⊢ ( 𝑅1 ‘ 1o ) = 1o