Metamath Proof Explorer

Theorem onsuci

Description: The successor of an ordinal number is an ordinal number. Corollary 7N(c) of Enderton p. 193. (Contributed by NM, 12-Jun-1994)

Ref Expression
Hypothesis onssi.1 A On
Assertion onsuci suc A On


Step Hyp Ref Expression
1 onssi.1 A On
2 suceloni A On suc A On
3 1 2 ax-mp suc A On