This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 \in ℤ_{\geq M} \to (K \dots N) \subseteq (M \dots N)$

Proof

Step	Hyp	Ref	Expression
1		elfzuz	$⊢ k \in (K \dots N) \to k \in ℤ_{\geq K}$
2		id	$⊢ K \in ℤ_{\geq M} \to K \in ℤ_{\geq M}$
3		uztrn	$⊢ (k \in ℤ_{\geq K} \land K \in ℤ_{\geq M}) \to k \in ℤ_{\geq M}$
4	1 2 3	syl2anr	$⊢ (K \in ℤ_{\geq M} \land k \in (K \dots N)) \to k \in ℤ_{\geq M}$
5		elfzuz3	$⊢ k \in (K \dots N) \to N \in ℤ_{\geq k}$
6	5	adantl	$⊢ (K \in ℤ_{\geq M} \land k \in (K \dots N)) \to N \in ℤ_{\geq k}$
7		elfzuzb	$⊢ k \in (M \dots N) \leftrightarrow (k \in ℤ_{\geq M} \land N \in ℤ_{\geq k})$
8	4 6 7	sylanbrc	$⊢ (K \in ℤ_{\geq M} \land k \in (K \dots N)) \to k \in (M \dots N)$
9	8	ex	$⊢ K \in ℤ_{\geq M} \to (k \in (K \dots N) \to k \in (M \dots N))$
10	9	ssrdv	$⊢ K \in ℤ_{\geq M} \to (K \dots N) \subseteq (M \dots N)$