Theorem uzssd2

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

	Ref	Expression
Hypotheses	uzssd2.1	$$⊢Z={\mathbb{Z}}_{\ge M}$$
	uzssd2.2	$$⊢\phi \to N\in Z$$
Assertion	uzssd2	$$⊢\phi \to {\mathbb{Z}}_{\ge N}\subseteq Z$$

Proof

Step	Hyp	Ref	Expression
1		uzssd2.1	$$⊢Z={\mathbb{Z}}_{\ge M}$$
2		uzssd2.2	$$⊢\phi \to N\in Z$$
3	2 1	eleqtrdi	$$⊢\phi \to N\in {\mathbb{Z}}_{\ge M}$$
4	3	uzssd	$$⊢\phi \to {\mathbb{Z}}_{\ge N}\subseteq {\mathbb{Z}}_{\ge M}$$
5	4 1	sseqtrrdi	$$⊢\phi \to {\mathbb{Z}}_{\ge N}\subseteq Z$$