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