Theorem uzssd3

Description: Subset relationship for two sets of upper integers. (Contributed by Glauco Siliprandi, 23-Oct-2021)

	Ref	Expression
Hypothesis	uzssd3.1	$$⊢Z={\mathbb{Z}}_{\ge M}$$
Assertion	uzssd3	$$⊢N\in Z\to {\mathbb{Z}}_{\ge N}\subseteq Z$$

Proof

Step	Hyp	Ref	Expression
1		uzssd3.1	$$⊢Z={\mathbb{Z}}_{\ge M}$$
2		id	$$⊢N\in Z\to N\in Z$$
3	1 2	uzssd2	$$⊢N\in Z\to {\mathbb{Z}}_{\ge N}\subseteq Z$$