Theorem uzn0d

Description: The upper integers are all nonempty. (Contributed by Glauco Siliprandi, 23-Oct-2021)

	Ref	Expression
Hypotheses	uzn0d.1	$$⊢\phi \to M\in \mathbb{Z}$$
	uzn0d.2	$$⊢Z={\mathbb{Z}}_{\ge M}$$
Assertion	uzn0d	$$⊢\phi \to Z\ne \varnothing$$

Proof

Step	Hyp	Ref	Expression
1		uzn0d.1	$$⊢\phi \to M\in \mathbb{Z}$$
2		uzn0d.2	$$⊢Z={\mathbb{Z}}_{\ge M}$$
3	1 2	uzidd2	$$⊢\phi \to M\in Z$$
4	3	ne0d	$$⊢\phi \to Z\ne \varnothing$$