ssfz12

Description: Subset relationship for finite sets of sequential integers. (Contributed by Alexander van der Vekens, 16-Mar-2018)

		Ref	Expression
	Assertion	ssfz12	$⊢ (K \in ℤ \land L \in ℤ \land K \leq L) \to ((K \dots L) \subseteq (M \dots N) \to (M \leq K \land L \leq N))$

Proof

Step	Hyp	Ref	Expression
1		eluz	$⊢ (K \in ℤ \land L \in ℤ) \to (L \in ℤ_{\geq K} \leftrightarrow K \leq L)$
2	1	biimp3ar	$⊢ (K \in ℤ \land L \in ℤ \land K \leq L) \to L \in ℤ_{\geq K}$
3		eluzfz1	$⊢ L \in ℤ_{\geq K} \to K \in (K \dots L)$
4	2 3	syl	$⊢ (K \in ℤ \land L \in ℤ \land K \leq L) \to K \in (K \dots L)$
5		eluzfz2	$⊢ L \in ℤ_{\geq K} \to L \in (K \dots L)$
6	2 5	syl	$⊢ (K \in ℤ \land L \in ℤ \land K \leq L) \to L \in (K \dots L)$
7		ssel2	$⊢ ((K \dots L) \subseteq (M \dots N) \land K \in (K \dots L)) \to K \in (M \dots N)$
8		ssel2	$⊢ ((K \dots L) \subseteq (M \dots N) \land L \in (K \dots L)) \to L \in (M \dots N)$
9		elfzuz3	$⊢ L \in (M \dots N) \to N \in ℤ_{\geq L}$
10		eluz2	$⊢ K \in ℤ_{\geq M} \leftrightarrow (M \in ℤ \land K \in ℤ \land M \leq K)$
11		eluz2	$⊢ N \in ℤ_{\geq L} \leftrightarrow (L \in ℤ \land N \in ℤ \land L \leq N)$
12		pm3.21	$⊢ L \leq N \to (M \leq K \to (M \leq K \land L \leq N))$
13	12	3ad2ant3	$⊢ (L \in ℤ \land N \in ℤ \land L \leq N) \to (M \leq K \to (M \leq K \land L \leq N))$
14	11 13	sylbi	$⊢ N \in ℤ_{\geq L} \to (M \leq K \to (M \leq K \land L \leq N))$
15	14	a1i	$⊢ (K \in ℤ \land L \in ℤ \land K \leq L) \to (N \in ℤ_{\geq L} \to (M \leq K \to (M \leq K \land L \leq N)))$
16	15	com13	$⊢ M \leq K \to (N \in ℤ_{\geq L} \to ((K \in ℤ \land L \in ℤ \land K \leq L) \to (M \leq K \land L \leq N)))$
17	16	3ad2ant3	$⊢ (M \in ℤ \land K \in ℤ \land M \leq K) \to (N \in ℤ_{\geq L} \to ((K \in ℤ \land L \in ℤ \land K \leq L) \to (M \leq K \land L \leq N)))$
18	10 17	sylbi	$⊢ K \in ℤ_{\geq M} \to (N \in ℤ_{\geq L} \to ((K \in ℤ \land L \in ℤ \land K \leq L) \to (M \leq K \land L \leq N)))$
19		elfzuz	$⊢ K \in (M \dots N) \to K \in ℤ_{\geq M}$
20	18 19	syl11	$⊢ N \in ℤ_{\geq L} \to (K \in (M \dots N) \to ((K \in ℤ \land L \in ℤ \land K \leq L) \to (M \leq K \land L \leq N)))$
21	8 9 20	3syl	$⊢ ((K \dots L) \subseteq (M \dots N) \land L \in (K \dots L)) \to (K \in (M \dots N) \to ((K \in ℤ \land L \in ℤ \land K \leq L) \to (M \leq K \land L \leq N)))$
22	21	ex	$⊢ (K \dots L) \subseteq (M \dots N) \to (L \in (K \dots L) \to (K \in (M \dots N) \to ((K \in ℤ \land L \in ℤ \land K \leq L) \to (M \leq K \land L \leq N))))$
23	22	com4t	$⊢ K \in (M \dots N) \to ((K \in ℤ \land L \in ℤ \land K \leq L) \to ((K \dots L) \subseteq (M \dots N) \to (L \in (K \dots L) \to (M \leq K \land L \leq N))))$
24	7 23	syl	$⊢ ((K \dots L) \subseteq (M \dots N) \land K \in (K \dots L)) \to ((K \in ℤ \land L \in ℤ \land K \leq L) \to ((K \dots L) \subseteq (M \dots N) \to (L \in (K \dots L) \to (M \leq K \land L \leq N))))$
25	24	ex	$⊢ (K \dots L) \subseteq (M \dots N) \to (K \in (K \dots L) \to ((K \in ℤ \land L \in ℤ \land K \leq L) \to ((K \dots L) \subseteq (M \dots N) \to (L \in (K \dots L) \to (M \leq K \land L \leq N)))))$
26	25	com24	$⊢ (K \dots L) \subseteq (M \dots N) \to ((K \dots L) \subseteq (M \dots N) \to ((K \in ℤ \land L \in ℤ \land K \leq L) \to (K \in (K \dots L) \to (L \in (K \dots L) \to (M \leq K \land L \leq N)))))$
27	26	pm2.43i	$⊢ (K \dots L) \subseteq (M \dots N) \to ((K \in ℤ \land L \in ℤ \land K \leq L) \to (K \in (K \dots L) \to (L \in (K \dots L) \to (M \leq K \land L \leq N))))$
28	27	com14	$⊢ L \in (K \dots L) \to ((K \in ℤ \land L \in ℤ \land K \leq L) \to (K \in (K \dots L) \to ((K \dots L) \subseteq (M \dots N) \to (M \leq K \land L \leq N))))$
29	6 28	mpcom	$⊢ (K \in ℤ \land L \in ℤ \land K \leq L) \to (K \in (K \dots L) \to ((K \dots L) \subseteq (M \dots N) \to (M \leq K \land L \leq N)))$
30	4 29	mpd	$⊢ (K \in ℤ \land L \in ℤ \land K \leq L) \to ((K \dots L) \subseteq (M \dots N) \to (M \leq K \land L \leq N))$

Metamath Proof Explorer

Theorem ssfz12

Proof