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 )