Metamath Proof Explorer


Theorem uzn0bi

Description: The upper integers function needs to be applied to an integer, in order to return a nonempty set. (Contributed by Glauco Siliprandi, 2-Jan-2022)

Ref Expression
Assertion uzn0bi MM

Proof

Step Hyp Ref Expression
1 uz0 ¬MM=
2 1 adantl M¬MM=
3 neneq M¬M=
4 3 adantr M¬M¬M=
5 2 4 condan MM
6 id MM
7 eqid M=M
8 6 7 uzn0d MM
9 5 8 impbii MM