Theorem uzinf

Description: An upper integer set is infinite. (Contributed by Mario Carneiro, 12-Mar-2015) (Revised by Mario Carneiro, 26-Jun-2015)

	Ref	Expression
Hypothesis	uzinf.1	$$⊢Z={\mathbb{Z}}_{\ge M}$$
Assertion	uzinf	$$⊢M\in \mathbb{Z}\to \neg Z\in \mathrm{Fin}$$

Proof

Step	Hyp	Ref	Expression
1		uzinf.1	$$⊢Z={\mathbb{Z}}_{\ge M}$$
2		ominf	$$⊢\neg \mathrm{\omega }\in \mathrm{Fin}$$
3	1	uzenom	$$⊢M\in \mathbb{Z}\to Z\approx \mathrm{\omega }$$
4		enfi	$$⊢Z\approx \mathrm{\omega }\to \left(Z\in \mathrm{Fin}\leftrightarrow \mathrm{\omega }\in \mathrm{Fin}\right)$$
5	3 4	syl	$$⊢M\in \mathbb{Z}\to \left(Z\in \mathrm{Fin}\leftrightarrow \mathrm{\omega }\in \mathrm{Fin}\right)$$
6	2 5	mtbiri	$$⊢M\in \mathbb{Z}\to \neg Z\in \mathrm{Fin}$$