Theorem fzssp1

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

	Ref	Expression
Assertion	fzssp1	|- ( M ... N ) C_ ( M ... ( N + 1 ) )

Proof

Step	Hyp	Ref	Expression
1		elfzel2	|- ( k e. ( M ... N ) -> N e. ZZ )
2		uzid	|- ( N e. ZZ -> N e. ( ZZ>= ` N ) )
3		peano2uz	|- ( N e. ( ZZ>= ` N ) -> ( N + 1 ) e. ( ZZ>= ` N ) )
4		fzss2	|- ( ( N + 1 ) e. ( ZZ>= ` N ) -> ( M ... N ) C_ ( M ... ( N + 1 ) ) )
5	1 2 3 4	4syl	|- ( k e. ( M ... N ) -> ( M ... N ) C_ ( M ... ( N + 1 ) ) )
6		id	|- ( k e. ( M ... N ) -> k e. ( M ... N ) )
7	5 6	sseldd	|- ( k e. ( M ... N ) -> k e. ( M ... ( N + 1 ) ) )
8	7	ssriv	|- ( M ... N ) C_ ( M ... ( N + 1 ) )