Theorem omenps

Description: Omega is equinumerous to a proper subset of itself. Example 13.2(4) of Eisenberg p. 216. (Contributed by NM, 30-Jul-2003)

	Ref	Expression
Assertion	omenps	$$⊢\mathrm{\omega }\approx \left(\mathrm{\omega }\setminus \left\{\varnothing \right\}\right)$$

Proof

Step	Hyp	Ref	Expression
1		omex	$$⊢\mathrm{\omega }\in \mathrm{V}$$
2		limom	$$⊢\mathrm{Lim}\mathrm{\omega }$$
3	2	limenpsi	$$⊢\mathrm{\omega }\in \mathrm{V}\to \mathrm{\omega }\approx \left(\mathrm{\omega }\setminus \left\{\varnothing \right\}\right)$$
4	1 3	ax-mp	$$⊢\mathrm{\omega }\approx \left(\mathrm{\omega }\setminus \left\{\varnothing \right\}\right)$$