Theorem ominf4

Description: _om is Dedekind infinite. (Contributed by Stefan O'Rear, 30-Oct-2014) (Proof shortened by Mario Carneiro, 16-May-2015)

	Ref	Expression
Assertion	ominf4	$$⊢\neg \mathrm{\omega }\in {\mathrm{Fin}}^{\mathrm{IV}}$$

Proof

Step	Hyp	Ref	Expression
1		id	$$⊢\mathrm{\omega }\in {\mathrm{Fin}}^{\mathrm{IV}}\to \mathrm{\omega }\in {\mathrm{Fin}}^{\mathrm{IV}}$$
2		peano1	$$⊢\varnothing \in \mathrm{\omega }$$
3		difsnpss	$$⊢\varnothing \in \mathrm{\omega }\leftrightarrow \mathrm{\omega }\setminus \left\{\varnothing \right\}\subset \mathrm{\omega }$$
4	2 3	mpbi	$$⊢\mathrm{\omega }\setminus \left\{\varnothing \right\}\subset \mathrm{\omega }$$
5		limom	$$⊢\mathrm{Lim}\mathrm{\omega }$$
6	5	limenpsi	$$⊢\mathrm{\omega }\in {\mathrm{Fin}}^{\mathrm{IV}}\to \mathrm{\omega }\approx \left(\mathrm{\omega }\setminus \left\{\varnothing \right\}\right)$$
7	6	ensymd	$$⊢\mathrm{\omega }\in {\mathrm{Fin}}^{\mathrm{IV}}\to \left(\mathrm{\omega }\setminus \left\{\varnothing \right\}\right)\approx \mathrm{\omega }$$
8		fin4i	$$⊢\left(\mathrm{\omega }\setminus \left\{\varnothing \right\}\subset \mathrm{\omega }\wedge \left(\mathrm{\omega }\setminus \left\{\varnothing \right\}\right)\approx \mathrm{\omega }\right)\to \neg \mathrm{\omega }\in {\mathrm{Fin}}^{\mathrm{IV}}$$
9	4 7 8	sylancr	$$⊢\mathrm{\omega }\in {\mathrm{Fin}}^{\mathrm{IV}}\to \neg \mathrm{\omega }\in {\mathrm{Fin}}^{\mathrm{IV}}$$
10	1 9	pm2.65i	$$⊢\neg \mathrm{\omega }\in {\mathrm{Fin}}^{\mathrm{IV}}$$