Theorem uzubico

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

	Ref	Expression
Hypotheses	uzubico.1	|- ( ph -> M e. ZZ )
	uzubico.2	|- Z = ( ZZ>= ` M )
	uzubico.3	|- ( ph -> X e. RR )
Assertion	uzubico	|- ( ph -> E. k e. ( X [,) +oo ) k e. Z )

Proof

Step	Hyp	Ref	Expression
1		uzubico.1	|- ( ph -> M e. ZZ )
2		uzubico.2	|- Z = ( ZZ>= ` M )
3		uzubico.3	|- ( ph -> X e. RR )
4	1 2 3	uzubioo	|- ( ph -> E. k e. ( X (,) +oo ) k e. Z )
5		ioossico	|- ( X (,) +oo ) C_ ( X [,) +oo )
6		ssrexv	|- ( ( X (,) +oo ) C_ ( X [,) +oo ) -> ( E. k e. ( X (,) +oo ) k e. Z -> E. k e. ( X [,) +oo ) k e. Z ) )
7	5 6	ax-mp	|- ( E. k e. ( X (,) +oo ) k e. Z -> E. k e. ( X [,) +oo ) k e. Z )
8	4 7	syl	|- ( ph -> E. k e. ( X [,) +oo ) k e. Z )