Metamath Proof Explorer


Theorem omelon2

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

Ref Expression
Assertion omelon2 ω V ω On

Proof

Step Hyp Ref Expression
1 omon ω On ω = On
2 1 ori ¬ ω On ω = On
3 onprc ¬ On V
4 eleq1 ω = On ω V On V
5 3 4 mtbiri ω = On ¬ ω V
6 2 5 syl ¬ ω On ¬ ω V
7 6 con4i ω V ω On