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 K M K M N

Proof

Step Hyp Ref Expression
1 elfzuz k M K k M
2 1 adantl N K k M K k M
3 elfzuz3 k M K K k
4 uztrn N K K k N k
5 3 4 sylan2 N K k M K N k
6 elfzuzb k M N k M N k
7 2 5 6 sylanbrc N K k M K k M N
8 7 ex N K k M K k M N
9 8 ssrdv N K M K M N