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 r1funlim 
 |-  ( Fun R1 /\ Lim dom R1 )
4 3 simpri 
 |-  Lim dom R1
5 1ellim 
 |-  ( Lim dom R1 -> 1o e. dom R1 )
6 r1sucg 
 |-  ( 1o e. dom R1 -> ( R1 ` suc 1o ) = ~P ( R1 ` 1o ) )
7 4 5 6 mp2b 
 |-  ( R1 ` suc 1o ) = ~P ( R1 ` 1o )
8 pwpw0 
 |-  ~P { (/) } = { (/) , { (/) } }
9 r11 
 |-  ( R1 ` 1o ) = 1o
10 df1o2 
 |-  1o = { (/) }
11 9 10 eqtri 
 |-  ( R1 ` 1o ) = { (/) }
12 11 pweqi 
 |-  ~P ( R1 ` 1o ) = ~P { (/) }
13 df2o2 
 |-  2o = { (/) , { (/) } }
14 8 12 13 3eqtr4i 
 |-  ~P ( R1 ` 1o ) = 2o
15 2 7 14 3eqtri 
 |-  ( R1 ` 2o ) = 2o