Theorem uzssd2

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

	Ref	Expression
Hypotheses	uzssd2.1	|- Z = ( ZZ>= ` M )
	uzssd2.2	|- ( ph -> N e. Z )
Assertion	uzssd2	|- ( ph -> ( ZZ>= ` N ) C_ Z )

Proof

Step	Hyp	Ref	Expression
1		uzssd2.1	|- Z = ( ZZ>= ` M )
2		uzssd2.2	|- ( ph -> N e. Z )
3	2 1	eleqtrdi	|- ( ph -> N e. ( ZZ>= ` M ) )
4	3	uzssd	|- ( ph -> ( ZZ>= ` N ) C_ ( ZZ>= ` M ) )
5	4 1	sseqtrrdi	|- ( ph -> ( ZZ>= ` N ) C_ Z )