Theorem uzubico2

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

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

Proof

Step	Hyp	Ref	Expression
1		uzubico2.1	$$⊢\phi \to M\in \mathbb{Z}$$
2		uzubico2.2	$$⊢Z={\mathbb{Z}}_{\ge M}$$
3	1 2	uzubioo2	$$⊢\phi \to \forall x\in ℝ\exists k\in \left(x,\mathrm{+\infty }\right)k\in Z$$
4		ioossico	$$⊢\left(x,\mathrm{+\infty }\right)\subseteq \left[x,\mathrm{+\infty }\right)$$
5		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)$$
6	4 5	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$$
7	6	ralimi	$$⊢\forall x\in ℝ\exists k\in \left(x,\mathrm{+\infty }\right)k\in Z\to \forall x\in ℝ\exists k\in \left[x,\mathrm{+\infty }\right)k\in Z$$
8	3 7	syl	$$⊢\phi \to \forall x\in ℝ\exists k\in \left[x,\mathrm{+\infty }\right)k\in Z$$