Theorem ssfz12

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

	Ref	Expression
Assertion	ssfz12	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ∧ 𝐾 ≤ 𝐿 ) → ( ( 𝐾 ... 𝐿 ) ⊆ ( 𝑀 ... 𝑁 ) → ( 𝑀 ≤ 𝐾 ∧ 𝐿 ≤ 𝑁 ) ) )

Proof

Step	Hyp	Ref	Expression
1		eluz	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → ( 𝐿 ∈ ( ℤ≥ ‘ 𝐾 ) ↔ 𝐾 ≤ 𝐿 ) )
2	1	biimp3ar	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ∧ 𝐾 ≤ 𝐿 ) → 𝐿 ∈ ( ℤ≥ ‘ 𝐾 ) )
3		eluzfz1	⊢ ( 𝐿 ∈ ( ℤ≥ ‘ 𝐾 ) → 𝐾 ∈ ( 𝐾 ... 𝐿 ) )
4	2 3	syl	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ∧ 𝐾 ≤ 𝐿 ) → 𝐾 ∈ ( 𝐾 ... 𝐿 ) )
5		eluzfz2	⊢ ( 𝐿 ∈ ( ℤ≥ ‘ 𝐾 ) → 𝐿 ∈ ( 𝐾 ... 𝐿 ) )
6	2 5	syl	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ∧ 𝐾 ≤ 𝐿 ) → 𝐿 ∈ ( 𝐾 ... 𝐿 ) )
7		ssel2	⊢ ( ( ( 𝐾 ... 𝐿 ) ⊆ ( 𝑀 ... 𝑁 ) ∧ 𝐾 ∈ ( 𝐾 ... 𝐿 ) ) → 𝐾 ∈ ( 𝑀 ... 𝑁 ) )
8		ssel2	⊢ ( ( ( 𝐾 ... 𝐿 ) ⊆ ( 𝑀 ... 𝑁 ) ∧ 𝐿 ∈ ( 𝐾 ... 𝐿 ) ) → 𝐿 ∈ ( 𝑀 ... 𝑁 ) )
9		elfzuz3	⊢ ( 𝐿 ∈ ( 𝑀 ... 𝑁 ) → 𝑁 ∈ ( ℤ≥ ‘ 𝐿 ) )
10		eluz2	⊢ ( 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) ↔ ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑀 ≤ 𝐾 ) )
11		eluz2	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝐿 ) ↔ ( 𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐿 ≤ 𝑁 ) )
12		pm3.21	⊢ ( 𝐿 ≤ 𝑁 → ( 𝑀 ≤ 𝐾 → ( 𝑀 ≤ 𝐾 ∧ 𝐿 ≤ 𝑁 ) ) )
13	12	3ad2ant3	⊢ ( ( 𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐿 ≤ 𝑁 ) → ( 𝑀 ≤ 𝐾 → ( 𝑀 ≤ 𝐾 ∧ 𝐿 ≤ 𝑁 ) ) )
14	11 13	sylbi	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝐿 ) → ( 𝑀 ≤ 𝐾 → ( 𝑀 ≤ 𝐾 ∧ 𝐿 ≤ 𝑁 ) ) )
15	14	a1i	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ∧ 𝐾 ≤ 𝐿 ) → ( 𝑁 ∈ ( ℤ≥ ‘ 𝐿 ) → ( 𝑀 ≤ 𝐾 → ( 𝑀 ≤ 𝐾 ∧ 𝐿 ≤ 𝑁 ) ) ) )
16	15	com13	⊢ ( 𝑀 ≤ 𝐾 → ( 𝑁 ∈ ( ℤ≥ ‘ 𝐿 ) → ( ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ∧ 𝐾 ≤ 𝐿 ) → ( 𝑀 ≤ 𝐾 ∧ 𝐿 ≤ 𝑁 ) ) ) )
17	16	3ad2ant3	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑀 ≤ 𝐾 ) → ( 𝑁 ∈ ( ℤ≥ ‘ 𝐿 ) → ( ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ∧ 𝐾 ≤ 𝐿 ) → ( 𝑀 ≤ 𝐾 ∧ 𝐿 ≤ 𝑁 ) ) ) )
18	10 17	sylbi	⊢ ( 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑁 ∈ ( ℤ≥ ‘ 𝐿 ) → ( ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ∧ 𝐾 ≤ 𝐿 ) → ( 𝑀 ≤ 𝐾 ∧ 𝐿 ≤ 𝑁 ) ) ) )
19		elfzuz	⊢ ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) → 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) )
20	18 19	syl11	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝐿 ) → ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) → ( ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ∧ 𝐾 ≤ 𝐿 ) → ( 𝑀 ≤ 𝐾 ∧ 𝐿 ≤ 𝑁 ) ) ) )
21	8 9 20	3syl	⊢ ( ( ( 𝐾 ... 𝐿 ) ⊆ ( 𝑀 ... 𝑁 ) ∧ 𝐿 ∈ ( 𝐾 ... 𝐿 ) ) → ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) → ( ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ∧ 𝐾 ≤ 𝐿 ) → ( 𝑀 ≤ 𝐾 ∧ 𝐿 ≤ 𝑁 ) ) ) )
22	21	ex	⊢ ( ( 𝐾 ... 𝐿 ) ⊆ ( 𝑀 ... 𝑁 ) → ( 𝐿 ∈ ( 𝐾 ... 𝐿 ) → ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) → ( ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ∧ 𝐾 ≤ 𝐿 ) → ( 𝑀 ≤ 𝐾 ∧ 𝐿 ≤ 𝑁 ) ) ) ) )
23	22	com4t	⊢ ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) → ( ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ∧ 𝐾 ≤ 𝐿 ) → ( ( 𝐾 ... 𝐿 ) ⊆ ( 𝑀 ... 𝑁 ) → ( 𝐿 ∈ ( 𝐾 ... 𝐿 ) → ( 𝑀 ≤ 𝐾 ∧ 𝐿 ≤ 𝑁 ) ) ) ) )
24	7 23	syl	⊢ ( ( ( 𝐾 ... 𝐿 ) ⊆ ( 𝑀 ... 𝑁 ) ∧ 𝐾 ∈ ( 𝐾 ... 𝐿 ) ) → ( ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ∧ 𝐾 ≤ 𝐿 ) → ( ( 𝐾 ... 𝐿 ) ⊆ ( 𝑀 ... 𝑁 ) → ( 𝐿 ∈ ( 𝐾 ... 𝐿 ) → ( 𝑀 ≤ 𝐾 ∧ 𝐿 ≤ 𝑁 ) ) ) ) )
25	24	ex	⊢ ( ( 𝐾 ... 𝐿 ) ⊆ ( 𝑀 ... 𝑁 ) → ( 𝐾 ∈ ( 𝐾 ... 𝐿 ) → ( ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ∧ 𝐾 ≤ 𝐿 ) → ( ( 𝐾 ... 𝐿 ) ⊆ ( 𝑀 ... 𝑁 ) → ( 𝐿 ∈ ( 𝐾 ... 𝐿 ) → ( 𝑀 ≤ 𝐾 ∧ 𝐿 ≤ 𝑁 ) ) ) ) ) )
26	25	com24	⊢ ( ( 𝐾 ... 𝐿 ) ⊆ ( 𝑀 ... 𝑁 ) → ( ( 𝐾 ... 𝐿 ) ⊆ ( 𝑀 ... 𝑁 ) → ( ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ∧ 𝐾 ≤ 𝐿 ) → ( 𝐾 ∈ ( 𝐾 ... 𝐿 ) → ( 𝐿 ∈ ( 𝐾 ... 𝐿 ) → ( 𝑀 ≤ 𝐾 ∧ 𝐿 ≤ 𝑁 ) ) ) ) ) )
27	26	pm2.43i	⊢ ( ( 𝐾 ... 𝐿 ) ⊆ ( 𝑀 ... 𝑁 ) → ( ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ∧ 𝐾 ≤ 𝐿 ) → ( 𝐾 ∈ ( 𝐾 ... 𝐿 ) → ( 𝐿 ∈ ( 𝐾 ... 𝐿 ) → ( 𝑀 ≤ 𝐾 ∧ 𝐿 ≤ 𝑁 ) ) ) ) )
28	27	com14	⊢ ( 𝐿 ∈ ( 𝐾 ... 𝐿 ) → ( ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ∧ 𝐾 ≤ 𝐿 ) → ( 𝐾 ∈ ( 𝐾 ... 𝐿 ) → ( ( 𝐾 ... 𝐿 ) ⊆ ( 𝑀 ... 𝑁 ) → ( 𝑀 ≤ 𝐾 ∧ 𝐿 ≤ 𝑁 ) ) ) ) )
29	6 28	mpcom	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ∧ 𝐾 ≤ 𝐿 ) → ( 𝐾 ∈ ( 𝐾 ... 𝐿 ) → ( ( 𝐾 ... 𝐿 ) ⊆ ( 𝑀 ... 𝑁 ) → ( 𝑀 ≤ 𝐾 ∧ 𝐿 ≤ 𝑁 ) ) ) )
30	4 29	mpd	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ∧ 𝐾 ≤ 𝐿 ) → ( ( 𝐾 ... 𝐿 ) ⊆ ( 𝑀 ... 𝑁 ) → ( 𝑀 ≤ 𝐾 ∧ 𝐿 ≤ 𝑁 ) ) )