Metamath Proof Explorer

Theorem suceloni

Description: The successor of an ordinal number is an ordinal number. Proposition 7.24 of TakeutiZaring p. 41. (Contributed by NM, 6-Jun-1994) (Proof shortened by BTernaryTau, 30-Nov-2024)

Ref Expression
Assertion suceloni 
|- ( A e. On -> suc A e. On )

Proof

Step Hyp Ref Expression
1 sucexg 
 |-  ( A e. On -> suc A e. _V )
2 sucexeloni 
 |-  ( ( A e. On /\ suc A e. _V ) -> suc A e. On )
3 1 2 mpdan 
 |-  ( A e. On -> suc A e. On )