Theorem uzubioo2

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

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

Proof

Step	Hyp	Ref	Expression
1		uzubioo2.1	$$⊢\phi \to M\in \mathbb{Z}$$
2		uzubioo2.2	$$⊢Z={\mathbb{Z}}_{\ge M}$$
3	1	adantr	$$⊢\left(\phi \wedge y\in ℝ\right)\to M\in \mathbb{Z}$$
4		simpr	$$⊢\left(\phi \wedge y\in ℝ\right)\to y\in ℝ$$
5	3 2 4	uzubioo	$$⊢\left(\phi \wedge y\in ℝ\right)\to \exists k\in \left(y,\mathrm{+\infty }\right)k\in Z$$
6	5	ralrimiva	$$⊢\phi \to \forall y\in ℝ\exists k\in \left(y,\mathrm{+\infty }\right)k\in Z$$
7		oveq1	$$⊢x=y\to \left(x,\mathrm{+\infty }\right)=\left(y,\mathrm{+\infty }\right)$$
8	7	rexeqdv	$$⊢x=y\to \left(\exists k\in \left(x,\mathrm{+\infty }\right)k\in Z\leftrightarrow \exists k\in \left(y,\mathrm{+\infty }\right)k\in Z\right)$$
9	8	cbvralvw	$$⊢\forall x\in ℝ\exists k\in \left(x,\mathrm{+\infty }\right)k\in Z\leftrightarrow \forall y\in ℝ\exists k\in \left(y,\mathrm{+\infty }\right)k\in Z$$
10	6 9	sylibr	$$⊢\phi \to \forall x\in ℝ\exists k\in \left(x,\mathrm{+\infty }\right)k\in Z$$