Theorem r12

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

	Ref	Expression
Assertion	r12	⊢ ( 𝑅1 ‘ 2o ) = 2o

Proof

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