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	$$⊢{\mathbb{Z}}_{\ge M}\subseteq \mathbb{Z}$$

Proof

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