Metamath Proof Explorer


Theorem 3on

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

Ref Expression
Assertion 3on 3o ∈ On

Proof

Step Hyp Ref Expression
1 df-3o 3o = suc 2o
2 2on 2o ∈ On
3 2 onsuci suc 2o ∈ On
4 1 3 eqeltri 3o ∈ On