This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )