Metamath Proof Explorer

Theorem r11

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

Ref Expression
Assertion r11 
|- ( R1 ` 1o ) = 1o

Proof

Step Hyp Ref Expression
1 df-1o 
 |-  1o = suc (/)
2 1 fveq2i 
 |-  ( R1 ` 1o ) = ( R1 ` suc (/) )
3 r1funlim 
 |-  ( Fun R1 /\ Lim dom R1 )
4 3 simpri 
 |-  Lim dom R1
5 0ellim 
 |-  ( Lim dom R1 -> (/) e. dom R1 )
6 r1sucg 
 |-  ( (/) e. dom R1 -> ( R1 ` suc (/) ) = ~P ( R1 ` (/) ) )
7 4 5 6 mp2b 
 |-  ( R1 ` suc (/) ) = ~P ( R1 ` (/) )
8 pw0 
 |-  ~P (/) = { (/) }
9 r10 
 |-  ( R1 ` (/) ) = (/)
10 9 pweqi 
 |-  ~P ( R1 ` (/) ) = ~P (/)
11 df1o2 
 |-  1o = { (/) }
12 8 10 11 3eqtr4i 
 |-  ~P ( R1 ` (/) ) = 1o
13 2 7 12 3eqtri 
 |-  ( R1 ` 1o ) = 1o