Description: The domain of the cumulative hierarchy of sets function is a limit ordinal. This weak form of r1fnon avoids ax-rep . (Contributed by Mario Carneiro, 16-Nov-2014) Extract this statement from its conjunction with r1fun . (Revised by BJ, 27-Sep-2026)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | r1dmlim | |- Lim dom R1 |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | rdgdmlim | |- Lim dom rec ( ( x e. _V |-> ~P x ) , (/) ) |
|
| 2 | df-r1 | |- R1 = rec ( ( x e. _V |-> ~P x ) , (/) ) |
|
| 3 | 2 | dmeqi | |- dom R1 = dom rec ( ( x e. _V |-> ~P x ) , (/) ) |
| 4 | limeq | |- ( dom R1 = dom rec ( ( x e. _V |-> ~P x ) , (/) ) -> ( Lim dom R1 <-> Lim dom rec ( ( x e. _V |-> ~P x ) , (/) ) ) ) |
|
| 5 | 3 4 | ax-mp | |- ( Lim dom R1 <-> Lim dom rec ( ( x e. _V |-> ~P x ) , (/) ) ) |
| 6 | 1 5 | mpbir | |- Lim dom R1 |