Theorem fzss1

Description: Subset relationship for finite sets of sequential integers. (Contributed by NM, 28-Sep-2005) (Proof shortened by Mario Carneiro, 28-Apr-2015)

	Ref	Expression
Assertion	fzss1	⊢ ( 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝐾 ... 𝑁 ) ⊆ ( 𝑀 ... 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		elfzuz	⊢ ( 𝑘 ∈ ( 𝐾 ... 𝑁 ) → 𝑘 ∈ ( ℤ≥ ‘ 𝐾 ) )
2		id	⊢ ( 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) )
3		uztrn	⊢ ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝐾 ) ∧ 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) )
4	1 2 3	syl2anr	⊢ ( ( 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑘 ∈ ( 𝐾 ... 𝑁 ) ) → 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) )
5		elfzuz3	⊢ ( 𝑘 ∈ ( 𝐾 ... 𝑁 ) → 𝑁 ∈ ( ℤ≥ ‘ 𝑘 ) )
6	5	adantl	⊢ ( ( 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑘 ∈ ( 𝐾 ... 𝑁 ) ) → 𝑁 ∈ ( ℤ≥ ‘ 𝑘 ) )
7		elfzuzb	⊢ ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ↔ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑘 ) ) )
8	4 6 7	sylanbrc	⊢ ( ( 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑘 ∈ ( 𝐾 ... 𝑁 ) ) → 𝑘 ∈ ( 𝑀 ... 𝑁 ) )
9	8	ex	⊢ ( 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑘 ∈ ( 𝐾 ... 𝑁 ) → 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) )
10	9	ssrdv	⊢ ( 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝐾 ... 𝑁 ) ⊆ ( 𝑀 ... 𝑁 ) )