Theorem uzubico2

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

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

Proof

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