Theorem omelon

Description: Omega is an ordinal number. Theorem 1.22 of Schloeder p. 3. (Contributed by NM, 10-May-1998) (Revised by Mario Carneiro, 30-Jan-2013)

	Ref	Expression
Assertion	omelon	⊢ ω ∈ On

Proof

Step	Hyp	Ref	Expression
1		omex	⊢ ω ∈ V
2		omelon2	⊢ ( ω ∈ V → ω ∈ On )
3	1 2	ax-mp	⊢ ω ∈ On