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