Theorem uzn0

Description: The upper integers are all nonempty. (Contributed by Mario Carneiro, 16-Jan-2014)

	Ref	Expression
Assertion	uzn0	$$⊢M\in \mathrm{ran}{\mathbb{Z}}_{\ge }\to M\ne \varnothing$$

Proof

Step	Hyp	Ref	Expression
1		uzf	$$⊢{\mathbb{Z}}_{\ge }:\mathbb{Z}⟶𝒫\mathbb{Z}$$
2		ffn	$$⊢{\mathbb{Z}}_{\ge }:\mathbb{Z}⟶𝒫\mathbb{Z}\to {\mathbb{Z}}_{\ge }Fn\mathbb{Z}$$
3		fvelrnb	$$⊢{\mathbb{Z}}_{\ge }Fn\mathbb{Z}\to \left(M\in \mathrm{ran}{\mathbb{Z}}_{\ge }\leftrightarrow \exists k\in \mathbb{Z}{\mathbb{Z}}_{\ge k}=M\right)$$
4	1 2 3	mp2b	$$⊢M\in \mathrm{ran}{\mathbb{Z}}_{\ge }\leftrightarrow \exists k\in \mathbb{Z}{\mathbb{Z}}_{\ge k}=M$$
5		uzid	$$⊢k\in \mathbb{Z}\to k\in {\mathbb{Z}}_{\ge k}$$
6	5	ne0d	$$⊢k\in \mathbb{Z}\to {\mathbb{Z}}_{\ge k}\ne \varnothing$$
7		neeq1	$$⊢{\mathbb{Z}}_{\ge k}=M\to \left({\mathbb{Z}}_{\ge k}\ne \varnothing \leftrightarrow M\ne \varnothing \right)$$
8	6 7	syl5ibcom	$$⊢k\in \mathbb{Z}\to \left({\mathbb{Z}}_{\ge k}=M\to M\ne \varnothing \right)$$
9	8	rexlimiv	$$⊢\exists k\in \mathbb{Z}{\mathbb{Z}}_{\ge k}=M\to M\ne \varnothing$$
10	4 9	sylbi	$$⊢M\in \mathrm{ran}{\mathbb{Z}}_{\ge }\to M\ne \varnothing$$