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

Metamath Proof Explorer

Theorem uzubico

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

Ref Expression
Hypotheses uzubico.1 ⊢ φ → M ∈ ℤ
uzubico.2 ⊢ Z = ℤ ≥ M
uzubico.3 ⊢ φ → X ∈ ℝ
Assertion uzubico ⊢ φ → ∃ k ∈ X +∞ k ∈ Z

Proof

Step Hyp Ref Expression
1 uzubico.1 ⊢ φ → M ∈ ℤ
2 uzubico.2 ⊢ Z = ℤ ≥ M
3 uzubico.3 ⊢ φ → X ∈ ℝ
4 1 2 3 uzubioo ⊢ φ → ∃ k ∈ X +∞ k ∈ Z
5 ioossico ⊢ X +∞ ⊆ X +∞
6 ssrexv ⊢ X +∞ ⊆ X +∞ → ∃ k ∈ X +∞ k ∈ Z → ∃ k ∈ X +∞ k ∈ Z
7 5 6 ax-mp ⊢ ∃ k ∈ X +∞ k ∈ Z → ∃ k ∈ X +∞ k ∈ Z
8 4 7 syl ⊢ φ → ∃ k ∈ X +∞ k ∈ Z