uzn0

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

		Ref	Expression
	Assertion	uzn0	$⊢ M \in ran ℤ_{\geq} \to M \neq \emptyset$

Step	Hyp	Ref	Expression
1		uzf	$⊢ ℤ_{\geq} : ℤ ⟶ 𝒫 ℤ$
2		ffn	$⊢ ℤ_{\geq} : ℤ ⟶ 𝒫 ℤ \to ℤ_{\geq} Fn ℤ$
3		fvelrnb	$⊢ ℤ_{\geq} Fn ℤ \to (M \in ran ℤ_{\geq} \leftrightarrow \exists k \in ℤ ℤ_{\geq k} = M)$
4	1 2 3	mp2b	$⊢ M \in ran ℤ_{\geq} \leftrightarrow \exists k \in ℤ ℤ_{\geq k} = M$
5		uzid	$⊢ k \in ℤ \to k \in ℤ_{\geq k}$
6	5	ne0d	$⊢ k \in ℤ \to ℤ_{\geq k} \neq \emptyset$
7		neeq1	$⊢ ℤ_{\geq k} = M \to (ℤ_{\geq k} \neq \emptyset \leftrightarrow M \neq \emptyset)$
8	6 7	syl5ibcom	$⊢ k \in ℤ \to (ℤ_{\geq k} = M \to M \neq \emptyset)$
9	8	rexlimiv	$⊢ \exists k \in ℤ ℤ_{\geq k} = M \to M \neq \emptyset$
10	4 9	sylbi	$⊢ M \in ran ℤ_{\geq} \to M \neq \emptyset$

Metamath Proof Explorer