Metamath Proof Explorer


Theorem omelon

Description: Omega is an ordinal number. (Contributed by NM, 10-May-1998) (Revised by Mario Carneiro, 30-Jan-2013)

Ref Expression
Assertion omelon ω ∈ On

Proof

Step Hyp Ref Expression
1 omex ω ∈ V
2 omelon2 ( ω ∈ V → ω ∈ On )
3 1 2 ax-mp ω ∈ On