Metamath Proof Explorer


Theorem sucexeloni

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)

Ref Expression
Assertion sucexeloni A On suc A V suc A On

Proof

Step Hyp Ref Expression
1 eloni A On Ord A
2 ordsuci Ord A Ord suc A
3 1 2 syl A On Ord suc A
4 elex suc A V suc A V
5 elong suc A V suc A On Ord suc A
6 5 biimparc Ord suc A suc A V suc A On
7 3 4 6 syl2an A On suc A V suc A On