Theorem uzubico

Description: The upper integers are unbounded above. (Contributed by Glauco Siliprandi, 2-Jan-2022)

	Ref	Expression
Hypotheses	uzubico.1	$$⊢\phi \to M\in \mathbb{Z}$$
	uzubico.2	$$⊢Z={\mathbb{Z}}_{\ge M}$$
	uzubico.3	$$⊢\phi \to X\in ℝ$$
Assertion	uzubico	$$⊢\phi \to \exists k\in \left[X,\mathrm{+\infty }\right)k\in Z$$

Proof

Step	Hyp	Ref	Expression
1		uzubico.1	$$⊢\phi \to M\in \mathbb{Z}$$
2		uzubico.2	$$⊢Z={\mathbb{Z}}_{\ge M}$$
3		uzubico.3	$$⊢\phi \to X\in ℝ$$
4	1 2 3	uzubioo	$$⊢\phi \to \exists k\in \left(X,\mathrm{+\infty }\right)k\in Z$$
5		ioossico	$$⊢\left(X,\mathrm{+\infty }\right)\subseteq \left[X,\mathrm{+\infty }\right)$$
6		ssrexv	$$⊢\left(X,\mathrm{+\infty }\right)\subseteq \left[X,\mathrm{+\infty }\right)\to \left(\exists k\in \left(X,\mathrm{+\infty }\right)k\in Z\to \exists k\in \left[X,\mathrm{+\infty }\right)k\in Z\right)$$
7	5 6	ax-mp	$$⊢\exists k\in \left(X,\mathrm{+\infty }\right)k\in Z\to \exists k\in \left[X,\mathrm{+\infty }\right)k\in Z$$
8	4 7	syl	$$⊢\phi \to \exists k\in \left[X,\mathrm{+\infty }\right)k\in Z$$