uzubioo2

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

	Ref	Expression
Hypotheses	uzubioo2.1	$⊢ φ \to M \in ℤ$
	uzubioo2.2	$⊢ Z = ℤ_{\geq M}$
Assertion	uzubioo2	$⊢ φ \to \forall x \in ℝ \exists k \in (x, +∞) k \in Z$

Step	Hyp	Ref	Expression
1		uzubioo2.1	$⊢ φ \to M \in ℤ$
2		uzubioo2.2	$⊢ Z = ℤ_{\geq M}$
3	1	adantr	$⊢ (φ \land y \in ℝ) \to M \in ℤ$
4		simpr	$⊢ (φ \land y \in ℝ) \to y \in ℝ$
5	3 2 4	uzubioo	$⊢ (φ \land y \in ℝ) \to \exists k \in (y, +∞) k \in Z$
6	5	ralrimiva	$⊢ φ \to \forall y \in ℝ \exists k \in (y, +∞) k \in Z$
7		oveq1	$⊢ x = y \to (x, +∞) = (y, +∞)$
8	7	rexeqdv	$⊢ x = y \to (\exists k \in (x, +∞) k \in Z \leftrightarrow \exists k \in (y, +∞) k \in Z)$
9	8	cbvralvw	$⊢ \forall x \in ℝ \exists k \in (x, +∞) k \in Z \leftrightarrow \forall y \in ℝ \exists k \in (y, +∞) k \in Z$
10	6 9	sylibr	$⊢ φ \to \forall x \in ℝ \exists k \in (x, +∞) k \in Z$

Metamath Proof Explorer