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		r1dmlim	⊢ Lim dom 𝑅1
4		0ellim	⊢ ( Lim dom 𝑅1 → ∅ ∈ dom 𝑅1 )
5		r1sucg	⊢ ( ∅ ∈ dom 𝑅1 → ( 𝑅1 ‘ suc ∅ ) = 𝒫 ( 𝑅1 ‘ ∅ ) )
6	3 4 5	mp2b	⊢ ( 𝑅1 ‘ suc ∅ ) = 𝒫 ( 𝑅1 ‘ ∅ )
7		pw0	⊢ 𝒫 ∅ = { ∅ }
8		r10	⊢ ( 𝑅1 ‘ ∅ ) = ∅
9	8	pweqi	⊢ 𝒫 ( 𝑅1 ‘ ∅ ) = 𝒫 ∅
10		df1o2	⊢ 1o = { ∅ }
11	7 9 10	3eqtr4i	⊢ 𝒫 ( 𝑅1 ‘ ∅ ) = 1o
12	2 6 11	3eqtri	⊢ ( 𝑅1 ‘ 1o ) = 1o