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	|- ( 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 )