Theorem 3on

Description: Ordinal 3 is an ordinal number. (Contributed by Mario Carneiro, 5-Jan-2016)

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

Proof

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