This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 4on

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

Ref Expression
Assertion 4on 4o ∈ On

Proof

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