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) Avoid ax-un . (Revised by BTernaryTau, 30-Nov-2024)

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

Proof

Step	Hyp	Ref	Expression
1		df-2o	$⊢ 2_{𝑜} = suc 1_{𝑜}$
2		1on	$⊢ 1_{𝑜} \in On$
3		2oex	$⊢ 2_{𝑜} \in V$
4	1 3	eqeltrri	$⊢ suc 1_{𝑜} \in V$
5		sucexeloni	$⊢ (1_{𝑜} \in On \land suc 1_{𝑜} \in V) \to suc 1_{𝑜} \in On$
6	2 4 5	mp2an	$⊢ suc 1_{𝑜} \in On$
7	1 6	eqeltri	$⊢ 2_{𝑜} \in On$