Theorem uzubioo2

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

	Ref	Expression
Hypotheses	uzubioo2.1	|- ( ph -> M e. ZZ )
	uzubioo2.2	|- Z = ( ZZ>= ` M )
Assertion	uzubioo2	|- ( ph -> A. x e. RR E. k e. ( x (,) +oo ) k e. Z )

Proof

Step	Hyp	Ref	Expression
1		uzubioo2.1	|- ( ph -> M e. ZZ )
2		uzubioo2.2	|- Z = ( ZZ>= ` M )
3	1	adantr	|- ( ( ph /\ y e. RR ) -> M e. ZZ )
4		simpr	|- ( ( ph /\ y e. RR ) -> y e. RR )
5	3 2 4	uzubioo	|- ( ( ph /\ y e. RR ) -> E. k e. ( y (,) +oo ) k e. Z )
6	5	ralrimiva	|- ( ph -> A. y e. RR E. k e. ( y (,) +oo ) k e. Z )
7		oveq1	|- ( x = y -> ( x (,) +oo ) = ( y (,) +oo ) )
8	7	rexeqdv	|- ( x = y -> ( E. k e. ( x (,) +oo ) k e. Z <-> E. k e. ( y (,) +oo ) k e. Z ) )
9	8	cbvralvw	|- ( A. x e. RR E. k e. ( x (,) +oo ) k e. Z <-> A. y e. RR E. k e. ( y (,) +oo ) k e. Z )
10	6 9	sylibr	|- ( ph -> A. x e. RR E. k e. ( x (,) +oo ) k e. Z )