Metamath Proof Explorer


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 ( 𝜑 → ∀ 𝑥 ∈ ℝ ∃ 𝑘 ∈ ( 𝑥 (,) +∞ ) 𝑘𝑍 )