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 \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$