Theorem onsuci

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

	Ref	Expression
Hypothesis	onssi.1	$$⊢A\in \mathrm{On}$$
Assertion	onsuci	$$⊢\mathrm{suc}A\in \mathrm{On}$$

Proof

Step	Hyp	Ref	Expression
1		onssi.1	$$⊢A\in \mathrm{On}$$
2		onsuc	$$⊢A\in \mathrm{On}\to \mathrm{suc}A\in \mathrm{On}$$
3	1 2	ax-mp	$$⊢\mathrm{suc}A\in \mathrm{On}$$