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	$⊢ A \in On \to suc A \in On$

Proof

Step	Hyp	Ref	Expression
1		sucexg	$⊢ A \in On \to suc A \in V$
2		sucexeloni	$⊢ (A \in On \land suc A \in V) \to suc A \in On$
3	1 2	mpdan	$⊢ A \in On \to suc A \in On$