Theorem uzubioo2

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

	Ref	Expression
Hypotheses	uzubioo2.1	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
	uzubioo2.2	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
Assertion	uzubioo2	⊢ ( 𝜑 → ∀ 𝑥 ∈ ℝ ∃ 𝑘 ∈ ( 𝑥 (,) +∞ ) 𝑘 ∈ 𝑍 )

Proof

Step	Hyp	Ref	Expression
1		uzubioo2.1	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
2		uzubioo2.2	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
3	1	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → 𝑀 ∈ ℤ )
4		simpr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → 𝑦 ∈ ℝ )
5	3 2 4	uzubioo	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ∃ 𝑘 ∈ ( 𝑦 (,) +∞ ) 𝑘 ∈ 𝑍 )
6	5	ralrimiva	⊢ ( 𝜑 → ∀ 𝑦 ∈ ℝ ∃ 𝑘 ∈ ( 𝑦 (,) +∞ ) 𝑘 ∈ 𝑍 )
7		oveq1	⊢ ( 𝑥 = 𝑦 → ( 𝑥 (,) +∞ ) = ( 𝑦 (,) +∞ ) )
8	7	rexeqdv	⊢ ( 𝑥 = 𝑦 → ( ∃ 𝑘 ∈ ( 𝑥 (,) +∞ ) 𝑘 ∈ 𝑍 ↔ ∃ 𝑘 ∈ ( 𝑦 (,) +∞ ) 𝑘 ∈ 𝑍 ) )
9	8	cbvralvw	⊢ ( ∀ 𝑥 ∈ ℝ ∃ 𝑘 ∈ ( 𝑥 (,) +∞ ) 𝑘 ∈ 𝑍 ↔ ∀ 𝑦 ∈ ℝ ∃ 𝑘 ∈ ( 𝑦 (,) +∞ ) 𝑘 ∈ 𝑍 )
10	6 9	sylibr	⊢ ( 𝜑 → ∀ 𝑥 ∈ ℝ ∃ 𝑘 ∈ ( 𝑥 (,) +∞ ) 𝑘 ∈ 𝑍 )