Theorem uzssd3

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

	Ref	Expression
Hypothesis	uzssd3.1	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
Assertion	uzssd3	⊢ ( 𝑁 ∈ 𝑍 → ( ℤ≥ ‘ 𝑁 ) ⊆ 𝑍 )

Proof

Step	Hyp	Ref	Expression
1		uzssd3.1	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2		id	⊢ ( 𝑁 ∈ 𝑍 → 𝑁 ∈ 𝑍 )
3	1 2	uzssd2	⊢ ( 𝑁 ∈ 𝑍 → ( ℤ≥ ‘ 𝑁 ) ⊆ 𝑍 )