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	$⊢ ℤ_{\geq M} \subseteq ℤ$

Step	Hyp	Ref	Expression
1		uzf	$⊢ ℤ_{\geq} : ℤ ⟶ 𝒫 ℤ$
2	1	ffvelcdmi	$⊢ M \in ℤ \to ℤ_{\geq M} \in 𝒫 ℤ$
3	2	elpwid	$⊢ M \in ℤ \to ℤ_{\geq M} \subseteq ℤ$
4	1	fdmi	$⊢ dom ℤ_{\geq} = ℤ$
5	3 4	eleq2s	$⊢ M \in dom ℤ_{\geq} \to ℤ_{\geq M} \subseteq ℤ$
6		ndmfv	$⊢ \neg M \in dom ℤ_{\geq} \to ℤ_{\geq M} = \emptyset$
7		0ss	$⊢ \emptyset \subseteq ℤ$
8	6 7	eqsstrdi	$⊢ \neg M \in dom ℤ_{\geq} \to ℤ_{\geq M} \subseteq ℤ$
9	5 8	pm2.61i	$⊢ ℤ_{\geq M} \subseteq ℤ$

Metamath Proof Explorer