Theorem uzubico

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

	Ref	Expression
Hypotheses	uzubico.1	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
	uzubico.2	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
	uzubico.3	⊢ ( 𝜑 → 𝑋 ∈ ℝ )
Assertion	uzubico	⊢ ( 𝜑 → ∃ 𝑘 ∈ ( 𝑋 [,) +∞ ) 𝑘 ∈ 𝑍 )

Proof

Step	Hyp	Ref	Expression
1		uzubico.1	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
2		uzubico.2	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
3		uzubico.3	⊢ ( 𝜑 → 𝑋 ∈ ℝ )
4	1 2 3	uzubioo	⊢ ( 𝜑 → ∃ 𝑘 ∈ ( 𝑋 (,) +∞ ) 𝑘 ∈ 𝑍 )
5		ioossico	⊢ ( 𝑋 (,) +∞ ) ⊆ ( 𝑋 [,) +∞ )
6		ssrexv	⊢ ( ( 𝑋 (,) +∞ ) ⊆ ( 𝑋 [,) +∞ ) → ( ∃ 𝑘 ∈ ( 𝑋 (,) +∞ ) 𝑘 ∈ 𝑍 → ∃ 𝑘 ∈ ( 𝑋 [,) +∞ ) 𝑘 ∈ 𝑍 ) )
7	5 6	ax-mp	⊢ ( ∃ 𝑘 ∈ ( 𝑋 (,) +∞ ) 𝑘 ∈ 𝑍 → ∃ 𝑘 ∈ ( 𝑋 [,) +∞ ) 𝑘 ∈ 𝑍 )
8	4 7	syl	⊢ ( 𝜑 → ∃ 𝑘 ∈ ( 𝑋 [,) +∞ ) 𝑘 ∈ 𝑍 )