Description: Value of the cumulative hierarchy of sets function at 1o . (Contributed by BTernaryTau, 24-Jan-2026)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | r11 | |- ( R1 ` 1o ) = 1o |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | df-1o | |- 1o = suc (/) |
|
| 2 | 1 | fveq2i | |- ( R1 ` 1o ) = ( R1 ` suc (/) ) |
| 3 | r1dmlim | |- Lim dom R1 |
|
| 4 | 0ellim | |- ( Lim dom R1 -> (/) e. dom R1 ) |
|
| 5 | r1sucg | |- ( (/) e. dom R1 -> ( R1 ` suc (/) ) = ~P ( R1 ` (/) ) ) |
|
| 6 | 3 4 5 | mp2b | |- ( R1 ` suc (/) ) = ~P ( R1 ` (/) ) |
| 7 | pw0 | |- ~P (/) = { (/) } |
|
| 8 | r10 | |- ( R1 ` (/) ) = (/) |
|
| 9 | 8 | pweqi | |- ~P ( R1 ` (/) ) = ~P (/) |
| 10 | df1o2 | |- 1o = { (/) } |
|
| 11 | 7 9 10 | 3eqtr4i | |- ~P ( R1 ` (/) ) = 1o |
| 12 | 2 6 11 | 3eqtri | |- ( R1 ` 1o ) = 1o |