Description: The predecessor class over (/) is always (/) . (Contributed by Scott Fenton, 16-Apr-2011) (Proof shortened by AV, 11-Jun-2021)
Ref | Expression | ||
---|---|---|---|
Assertion | pred0 | |- Pred ( R , (/) , X ) = (/) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-pred | |- Pred ( R , (/) , X ) = ( (/) i^i ( `' R " { X } ) ) |
|
2 | 0in | |- ( (/) i^i ( `' R " { X } ) ) = (/) |
|
3 | 1 2 | eqtri | |- Pred ( R , (/) , X ) = (/) |