Theorem uzssz

Description: An upper set of integers is a subset of all integers. (Contributed by NM, 2-Sep-2005) (Revised by Mario Carneiro, 3-Nov-2013)

	Ref	Expression
Assertion	uzssz	⊢ ( ℤ≥ ‘ 𝑀 ) ⊆ ℤ

Proof

Step	Hyp	Ref	Expression
1		uzf	⊢ ℤ≥ : ℤ ⟶ 𝒫 ℤ
2	1	ffvelcdmi	⊢ ( 𝑀 ∈ ℤ → ( ℤ≥ ‘ 𝑀 ) ∈ 𝒫 ℤ )
3	2	elpwid	⊢ ( 𝑀 ∈ ℤ → ( ℤ≥ ‘ 𝑀 ) ⊆ ℤ )
4	1	fdmi	⊢ dom ℤ≥ = ℤ
5	3 4	eleq2s	⊢ ( 𝑀 ∈ dom ℤ≥ → ( ℤ≥ ‘ 𝑀 ) ⊆ ℤ )
6		ndmfv	⊢ ( ¬ 𝑀 ∈ dom ℤ≥ → ( ℤ≥ ‘ 𝑀 ) = ∅ )
7		0ss	⊢ ∅ ⊆ ℤ
8	6 7	eqsstrdi	⊢ ( ¬ 𝑀 ∈ dom ℤ≥ → ( ℤ≥ ‘ 𝑀 ) ⊆ ℤ )
9	5 8	pm2.61i	⊢ ( ℤ≥ ‘ 𝑀 ) ⊆ ℤ