# Metamath Proof Explorer

## Theorem fzss2

Description: Subset relationship for finite sets of sequential integers. (Contributed by NM, 4-Oct-2005) (Revised by Mario Carneiro, 30-Apr-2015)

Ref Expression
Assertion fzss2 ${⊢}{N}\in {ℤ}_{\ge {K}}\to \left({M}\dots {K}\right)\subseteq \left({M}\dots {N}\right)$

### Proof

Step Hyp Ref Expression
1 elfzuz ${⊢}{k}\in \left({M}\dots {K}\right)\to {k}\in {ℤ}_{\ge {M}}$
2 1 adantl ${⊢}\left({N}\in {ℤ}_{\ge {K}}\wedge {k}\in \left({M}\dots {K}\right)\right)\to {k}\in {ℤ}_{\ge {M}}$
3 elfzuz3 ${⊢}{k}\in \left({M}\dots {K}\right)\to {K}\in {ℤ}_{\ge {k}}$
4 uztrn ${⊢}\left({N}\in {ℤ}_{\ge {K}}\wedge {K}\in {ℤ}_{\ge {k}}\right)\to {N}\in {ℤ}_{\ge {k}}$
5 3 4 sylan2 ${⊢}\left({N}\in {ℤ}_{\ge {K}}\wedge {k}\in \left({M}\dots {K}\right)\right)\to {N}\in {ℤ}_{\ge {k}}$
6 elfzuzb ${⊢}{k}\in \left({M}\dots {N}\right)↔\left({k}\in {ℤ}_{\ge {M}}\wedge {N}\in {ℤ}_{\ge {k}}\right)$
7 2 5 6 sylanbrc ${⊢}\left({N}\in {ℤ}_{\ge {K}}\wedge {k}\in \left({M}\dots {K}\right)\right)\to {k}\in \left({M}\dots {N}\right)$
8 7 ex ${⊢}{N}\in {ℤ}_{\ge {K}}\to \left({k}\in \left({M}\dots {K}\right)\to {k}\in \left({M}\dots {N}\right)\right)$
9 8 ssrdv ${⊢}{N}\in {ℤ}_{\ge {K}}\to \left({M}\dots {K}\right)\subseteq \left({M}\dots {N}\right)$