Theorem omelon

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

	Ref	Expression
Assertion	omelon	$$⊢\mathrm{\omega }\in \mathrm{On}$$

Proof

Step	Hyp	Ref	Expression
1		omex	$$⊢\mathrm{\omega }\in \mathrm{V}$$
2		omelon2	$$⊢\mathrm{\omega }\in \mathrm{V}\to \mathrm{\omega }\in \mathrm{On}$$
3	1 2	ax-mp	$$⊢\mathrm{\omega }\in \mathrm{On}$$