Description: If the successor of an ordinal number exists, it is an ordinal number. This variation of onsuc does not require ax-un . (Contributed by BTernaryTau, 30-Nov-2024) (Proof shortened by BJ, 11-Jan-2025)