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	|- ( K e. ( ZZ>= ` M ) -> ( K ... N ) C_ ( M ... N ) )

Proof

Step	Hyp	Ref	Expression
1		elfzuz	|- ( k e. ( K ... N ) -> k e. ( ZZ>= ` K ) )
2		id	|- ( K e. ( ZZ>= ` M ) -> K e. ( ZZ>= ` M ) )
3		uztrn	|- ( ( k e. ( ZZ>= ` K ) /\ K e. ( ZZ>= ` M ) ) -> k e. ( ZZ>= ` M ) )
4	1 2 3	syl2anr	|- ( ( K e. ( ZZ>= ` M ) /\ k e. ( K ... N ) ) -> k e. ( ZZ>= ` M ) )
5		elfzuz3	|- ( k e. ( K ... N ) -> N e. ( ZZ>= ` k ) )
6	5	adantl	|- ( ( K e. ( ZZ>= ` M ) /\ k e. ( K ... N ) ) -> N e. ( ZZ>= ` k ) )
7		elfzuzb	|- ( k e. ( M ... N ) <-> ( k e. ( ZZ>= ` M ) /\ N e. ( ZZ>= ` k ) ) )
8	4 6 7	sylanbrc	|- ( ( K e. ( ZZ>= ` M ) /\ k e. ( K ... N ) ) -> k e. ( M ... N ) )
9	8	ex	|- ( K e. ( ZZ>= ` M ) -> ( k e. ( K ... N ) -> k e. ( M ... N ) ) )
10	9	ssrdv	|- ( K e. ( ZZ>= ` M ) -> ( K ... N ) C_ ( M ... N ) )