This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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