Metamath Proof Explorer

Theorem 2on

Description: Ordinal 2 is an ordinal number. (Contributed by NM, 18-Feb-2004) (Proof shortened by Andrew Salmon, 12-Aug-2011)

		Ref	Expression
	Assertion	2on	$⊢ 2_{𝑜} \in On$

Step	Hyp	Ref	Expression
1		df-2o	$⊢ 2_{𝑜} = suc 1_{𝑜}$
2		1on	$⊢ 1_{𝑜} \in On$
3	2	onsuci	$⊢ suc 1_{𝑜} \in On$
4	1 3	eqeltri	$⊢ 2_{𝑜} \in On$