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	|- 2o e. On

Proof

Step	Hyp	Ref	Expression
1		df-2o	|- 2o = suc 1o
2		1on	|- 1o e. On
3		2oex	|- 2o e. _V
4	1 3	eqeltrri	|- suc 1o e. _V
5		sucexeloni	|- ( ( 1o e. On /\ suc 1o e. _V ) -> suc 1o e. On )
6	2 4 5	mp2an	|- suc 1o e. On
7	1 6	eqeltri	|- 2o e. On