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
|- _om e. On

Proof

Step Hyp Ref Expression
1 omex
 |-  _om e. _V
2 omelon2
 |-  ( _om e. _V -> _om e. On )
3 1 2 ax-mp
 |-  _om e. On