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