Metamath Proof Explorer


Theorem 4onn

Description: The ordinal 4 is a natural number. (Contributed by Mario Carneiro, 5-Jan-2016)

Ref Expression
Assertion 4onn 4 𝑜 ω

Proof

Step Hyp Ref Expression
1 df-4o 4 𝑜 = suc 3 𝑜
2 3onn 3 𝑜 ω
3 peano2 3 𝑜 ω suc 3 𝑜 ω
4 2 3 ax-mp suc 3 𝑜 ω
5 1 4 eqeltri 4 𝑜 ω