Metamath Proof Explorer


Theorem 3on

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

Ref Expression
Assertion 3on 3 𝑜 On

Proof

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