Metamath Proof Explorer

Theorem ssfz12

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

Ref Expression
Assertion ssfz12 
|- ( ( K e. ZZ /\ L e. ZZ /\ K <_ L ) -> ( ( K ... L ) C_ ( M ... N ) -> ( M <_ K /\ L <_ N ) ) )

Proof

Step Hyp Ref Expression
1 eluz 
 |-  ( ( K e. ZZ /\ L e. ZZ ) -> ( L e. ( ZZ>= ` K ) <-> K <_ L ) )
2 1 biimp3ar 
 |-  ( ( K e. ZZ /\ L e. ZZ /\ K <_ L ) -> L e. ( ZZ>= ` K ) )
3 eluzfz1 
 |-  ( L e. ( ZZ>= ` K ) -> K e. ( K ... L ) )
4 2 3 syl 
 |-  ( ( K e. ZZ /\ L e. ZZ /\ K <_ L ) -> K e. ( K ... L ) )
5 eluzfz2 
 |-  ( L e. ( ZZ>= ` K ) -> L e. ( K ... L ) )
6 2 5 syl 
 |-  ( ( K e. ZZ /\ L e. ZZ /\ K <_ L ) -> L e. ( K ... L ) )
7 ssel2 
 |-  ( ( ( K ... L ) C_ ( M ... N ) /\ K e. ( K ... L ) ) -> K e. ( M ... N ) )
8 ssel2 
 |-  ( ( ( K ... L ) C_ ( M ... N ) /\ L e. ( K ... L ) ) -> L e. ( M ... N ) )
9 elfzuz3 
 |-  ( L e. ( M ... N ) -> N e. ( ZZ>= ` L ) )
10 eluz2 
 |-  ( K e. ( ZZ>= ` M ) <-> ( M e. ZZ /\ K e. ZZ /\ M <_ K ) )
11 eluz2 
 |-  ( N e. ( ZZ>= ` L ) <-> ( L e. ZZ /\ N e. ZZ /\ L <_ N ) )
12 pm3.21 
 |-  ( L <_ N -> ( M <_ K -> ( M <_ K /\ L <_ N ) ) )
13 12 3ad2ant3 
 |-  ( ( L e. ZZ /\ N e. ZZ /\ L <_ N ) -> ( M <_ K -> ( M <_ K /\ L <_ N ) ) )
14 11 13 sylbi 
 |-  ( N e. ( ZZ>= ` L ) -> ( M <_ K -> ( M <_ K /\ L <_ N ) ) )
15 14 a1i 
 |-  ( ( K e. ZZ /\ L e. ZZ /\ K <_ L ) -> ( N e. ( ZZ>= ` L ) -> ( M <_ K -> ( M <_ K /\ L <_ N ) ) ) )
16 15 com13 
 |-  ( M <_ K -> ( N e. ( ZZ>= ` L ) -> ( ( K e. ZZ /\ L e. ZZ /\ K <_ L ) -> ( M <_ K /\ L <_ N ) ) ) )
17 16 3ad2ant3 
 |-  ( ( M e. ZZ /\ K e. ZZ /\ M <_ K ) -> ( N e. ( ZZ>= ` L ) -> ( ( K e. ZZ /\ L e. ZZ /\ K <_ L ) -> ( M <_ K /\ L <_ N ) ) ) )
18 10 17 sylbi 
 |-  ( K e. ( ZZ>= ` M ) -> ( N e. ( ZZ>= ` L ) -> ( ( K e. ZZ /\ L e. ZZ /\ K <_ L ) -> ( M <_ K /\ L <_ N ) ) ) )
19 elfzuz 
 |-  ( K e. ( M ... N ) -> K e. ( ZZ>= ` M ) )
20 18 19 syl11 
 |-  ( N e. ( ZZ>= ` L ) -> ( K e. ( M ... N ) -> ( ( K e. ZZ /\ L e. ZZ /\ K <_ L ) -> ( M <_ K /\ L <_ N ) ) ) )
21 8 9 20 3syl 
 |-  ( ( ( K ... L ) C_ ( M ... N ) /\ L e. ( K ... L ) ) -> ( K e. ( M ... N ) -> ( ( K e. ZZ /\ L e. ZZ /\ K <_ L ) -> ( M <_ K /\ L <_ N ) ) ) )
22 21 ex 
 |-  ( ( K ... L ) C_ ( M ... N ) -> ( L e. ( K ... L ) -> ( K e. ( M ... N ) -> ( ( K e. ZZ /\ L e. ZZ /\ K <_ L ) -> ( M <_ K /\ L <_ N ) ) ) ) )
23 22 com4t 
 |-  ( K e. ( M ... N ) -> ( ( K e. ZZ /\ L e. ZZ /\ K <_ L ) -> ( ( K ... L ) C_ ( M ... N ) -> ( L e. ( K ... L ) -> ( M <_ K /\ L <_ N ) ) ) ) )
24 7 23 syl 
 |-  ( ( ( K ... L ) C_ ( M ... N ) /\ K e. ( K ... L ) ) -> ( ( K e. ZZ /\ L e. ZZ /\ K <_ L ) -> ( ( K ... L ) C_ ( M ... N ) -> ( L e. ( K ... L ) -> ( M <_ K /\ L <_ N ) ) ) ) )
25 24 ex 
 |-  ( ( K ... L ) C_ ( M ... N ) -> ( K e. ( K ... L ) -> ( ( K e. ZZ /\ L e. ZZ /\ K <_ L ) -> ( ( K ... L ) C_ ( M ... N ) -> ( L e. ( K ... L ) -> ( M <_ K /\ L <_ N ) ) ) ) ) )
26 25 com24 
 |-  ( ( K ... L ) C_ ( M ... N ) -> ( ( K ... L ) C_ ( M ... N ) -> ( ( K e. ZZ /\ L e. ZZ /\ K <_ L ) -> ( K e. ( K ... L ) -> ( L e. ( K ... L ) -> ( M <_ K /\ L <_ N ) ) ) ) ) )
27 26 pm2.43i 
 |-  ( ( K ... L ) C_ ( M ... N ) -> ( ( K e. ZZ /\ L e. ZZ /\ K <_ L ) -> ( K e. ( K ... L ) -> ( L e. ( K ... L ) -> ( M <_ K /\ L <_ N ) ) ) ) )
28 27 com14 
 |-  ( L e. ( K ... L ) -> ( ( K e. ZZ /\ L e. ZZ /\ K <_ L ) -> ( K e. ( K ... L ) -> ( ( K ... L ) C_ ( M ... N ) -> ( M <_ K /\ L <_ N ) ) ) ) )
29 6 28 mpcom 
 |-  ( ( K e. ZZ /\ L e. ZZ /\ K <_ L ) -> ( K e. ( K ... L ) -> ( ( K ... L ) C_ ( M ... N ) -> ( M <_ K /\ L <_ N ) ) ) )
30 4 29 mpd 
 |-  ( ( K e. ZZ /\ L e. ZZ /\ K <_ L ) -> ( ( K ... L ) C_ ( M ... N ) -> ( M <_ K /\ L <_ N ) ) )