Metamath Proof Explorer

Theorem omelon2

Description: Omega is an ordinal number. (Contributed by Mario Carneiro, 30-Jan-2013)

Ref Expression
Assertion omelon2 
|- ( _om e. _V -> _om e. On )

Proof

Step Hyp Ref Expression
1 omon 
 |-  ( _om e. On \/ _om = On )
2 1 ori 
 |-  ( -. _om e. On -> _om = On )
3 onprc 
 |-  -. On e. _V
4 eleq1 
 |-  ( _om = On -> ( _om e. _V <-> On e. _V ) )
5 3 4 mtbiri 
 |-  ( _om = On -> -. _om e. _V )
6 2 5 syl 
 |-  ( -. _om e. On -> -. _om e. _V )
7 6 con4i 
 |-  ( _om e. _V -> _om e. On )