Theorem uzn0

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

	Ref	Expression
Assertion	uzn0	⊢ ( 𝑀 ∈ ran ℤ≥ → 𝑀 ≠ ∅ )

Proof

Step	Hyp	Ref	Expression
1		uzf	⊢ ℤ≥ : ℤ ⟶ 𝒫 ℤ
2		ffn	⊢ ( ℤ≥ : ℤ ⟶ 𝒫 ℤ → ℤ≥ Fn ℤ )
3		fvelrnb	⊢ ( ℤ≥ Fn ℤ → ( 𝑀 ∈ ran ℤ≥ ↔ ∃ 𝑘 ∈ ℤ ( ℤ≥ ‘ 𝑘 ) = 𝑀 ) )
4	1 2 3	mp2b	⊢ ( 𝑀 ∈ ran ℤ≥ ↔ ∃ 𝑘 ∈ ℤ ( ℤ≥ ‘ 𝑘 ) = 𝑀 )
5		uzid	⊢ ( 𝑘 ∈ ℤ → 𝑘 ∈ ( ℤ≥ ‘ 𝑘 ) )
6	5	ne0d	⊢ ( 𝑘 ∈ ℤ → ( ℤ≥ ‘ 𝑘 ) ≠ ∅ )
7		neeq1	⊢ ( ( ℤ≥ ‘ 𝑘 ) = 𝑀 → ( ( ℤ≥ ‘ 𝑘 ) ≠ ∅ ↔ 𝑀 ≠ ∅ ) )
8	6 7	syl5ibcom	⊢ ( 𝑘 ∈ ℤ → ( ( ℤ≥ ‘ 𝑘 ) = 𝑀 → 𝑀 ≠ ∅ ) )
9	8	rexlimiv	⊢ ( ∃ 𝑘 ∈ ℤ ( ℤ≥ ‘ 𝑘 ) = 𝑀 → 𝑀 ≠ ∅ )
10	4 9	sylbi	⊢ ( 𝑀 ∈ ran ℤ≥ → 𝑀 ≠ ∅ )