Metamath Proof Explorer

Theorem r12

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

Ref Expression
Assertion r12 
|- ( R1 ` 2o ) = 2o

Proof

Step Hyp Ref Expression
1 df-2o 
 |-  2o = suc 1o
2 1 fveq2i 
 |-  ( R1 ` 2o ) = ( R1 ` suc 1o )
3 r1dmlim 
 |-  Lim dom R1
4 1ellim 
 |-  ( Lim dom R1 -> 1o e. dom R1 )
5 r1sucg 
 |-  ( 1o e. dom R1 -> ( R1 ` suc 1o ) = ~P ( R1 ` 1o ) )
6 3 4 5 mp2b 
 |-  ( R1 ` suc 1o ) = ~P ( R1 ` 1o )
7 pwpw0 
 |-  ~P { (/) } = { (/) , { (/) } }
8 r11 
 |-  ( R1 ` 1o ) = 1o
9 df1o2 
 |-  1o = { (/) }
10 8 9 eqtri 
 |-  ( R1 ` 1o ) = { (/) }
11 10 pweqi 
 |-  ~P ( R1 ` 1o ) = ~P { (/) }
12 df2o2 
 |-  2o = { (/) , { (/) } }
13 7 11 12 3eqtr4i 
 |-  ~P ( R1 ` 1o ) = 2o
14 2 6 13 3eqtri 
 |-  ( R1 ` 2o ) = 2o