Metamath Proof Explorer

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 \dots N) \subseteq (M \dots N + 1)$

Proof

Step	Hyp	Ref	Expression
1		elfzel2	$⊢ k \in (M \dots N) \to N \in ℤ$
2		uzid	$⊢ N \in ℤ \to N \in ℤ_{\geq N}$
3		peano2uz	$⊢ N \in ℤ_{\geq N} \to N + 1 \in ℤ_{\geq N}$
4		fzss2	$⊢ N + 1 \in ℤ_{\geq N} \to (M \dots N) \subseteq (M \dots N + 1)$
5	1 2 3 4	4syl	$⊢ k \in (M \dots N) \to (M \dots N) \subseteq (M \dots N + 1)$
6		id	$⊢ k \in (M \dots N) \to k \in (M \dots N)$
7	5 6	sseldd	$⊢ k \in (M \dots N) \to k \in (M \dots N + 1)$
8	7	ssriv	$⊢ (M \dots N) \subseteq (M \dots N + 1)$