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 )