Theorem omelon2

Description: Omega is an ordinal number. (Contributed by Mario Carneiro, 30-Jan-2013)

	Ref	Expression
Assertion	omelon2	$$⊢\mathrm{\omega }\in \mathrm{V}\to \mathrm{\omega }\in \mathrm{On}$$

Proof

Step	Hyp	Ref	Expression
1		omon	$$⊢\left(\mathrm{\omega }\in \mathrm{On}\vee \mathrm{\omega }=\mathrm{On}\right)$$
2	1	ori	$$⊢\neg \mathrm{\omega }\in \mathrm{On}\to \mathrm{\omega }=\mathrm{On}$$
3		onprc	$$⊢\neg \mathrm{On}\in \mathrm{V}$$
4		eleq1	$$⊢\mathrm{\omega }=\mathrm{On}\to \left(\mathrm{\omega }\in \mathrm{V}\leftrightarrow \mathrm{On}\in \mathrm{V}\right)$$
5	3 4	mtbiri	$$⊢\mathrm{\omega }=\mathrm{On}\to \neg \mathrm{\omega }\in \mathrm{V}$$
6	2 5	syl	$$⊢\neg \mathrm{\omega }\in \mathrm{On}\to \neg \mathrm{\omega }\in \mathrm{V}$$
7	6	con4i	$$⊢\mathrm{\omega }\in \mathrm{V}\to \mathrm{\omega }\in \mathrm{On}$$