Theorem uzssd

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

	Ref	Expression
Hypothesis	uzssd.1	|- ( ph -> N e. ( ZZ>= ` M ) )
Assertion	uzssd	|- ( ph -> ( ZZ>= ` N ) C_ ( ZZ>= ` M ) )

Proof

Step	Hyp	Ref	Expression
1		uzssd.1	|- ( ph -> N e. ( ZZ>= ` M ) )
2		uzss	|- ( N e. ( ZZ>= ` M ) -> ( ZZ>= ` N ) C_ ( ZZ>= ` M ) )
3	1 2	syl	|- ( ph -> ( ZZ>= ` N ) C_ ( ZZ>= ` M ) )