Theorem fzp1ss

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

	Ref	Expression
Assertion	fzp1ss	|- ( M e. ZZ -> ( ( M + 1 ) ... N ) C_ ( M ... N ) )

Proof

Step	Hyp	Ref	Expression
1		uzid	|- ( M e. ZZ -> M e. ( ZZ>= ` M ) )
2		peano2uz	|- ( M e. ( ZZ>= ` M ) -> ( M + 1 ) e. ( ZZ>= ` M ) )
3		fzss1	|- ( ( M + 1 ) e. ( ZZ>= ` M ) -> ( ( M + 1 ) ... N ) C_ ( M ... N ) )
4	1 2 3	3syl	|- ( M e. ZZ -> ( ( M + 1 ) ... N ) C_ ( M ... N ) )