Metamath Proof Explorer

Theorem 1on

Description: Ordinal 1 is an ordinal number. (Contributed by NM, 29-Oct-1995) Avoid ax-un . (Revised by BTernaryTau, 30-Nov-2024)

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

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