Metamath Proof Explorer


Theorem onsuc

Description: The successor of an ordinal number is an ordinal number. Closed form of onsuci . Forward implication of onsucb . Proposition 7.24 of TakeutiZaring p. 41. Remark 1.5 of Schloeder p. 1. (Contributed by NM, 6-Jun-1994) (Proof shortened by BTernaryTau, 30-Nov-2024)

Ref Expression
Assertion onsuc ( 𝐴 ∈ On → suc 𝐴 ∈ On )

Proof

Step Hyp Ref Expression
1 sucexg ( 𝐴 ∈ On → suc 𝐴 ∈ V )
2 sucexeloni ( ( 𝐴 ∈ On ∧ suc 𝐴 ∈ V ) → suc 𝐴 ∈ On )
3 1 2 mpdan ( 𝐴 ∈ On → suc 𝐴 ∈ On )