Users' Mathboxes Mathbox for Alexander van der Vekens < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ssfz12 Structured version   Visualization version   GIF version

Theorem ssfz12 44479
Description: Subset relationship for finite sets of sequential integers. (Contributed by Alexander van der Vekens, 16-Mar-2018.)
Assertion
Ref Expression
ssfz12 ((𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ∧ 𝐾𝐿) → ((𝐾...𝐿) ⊆ (𝑀...𝑁) → (𝑀𝐾𝐿𝑁)))

Proof of Theorem ssfz12
StepHypRef Expression
1 eluz 12452 . . . 4 ((𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ) → (𝐿 ∈ (ℤ𝐾) ↔ 𝐾𝐿))
21biimp3ar 1472 . . 3 ((𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ∧ 𝐾𝐿) → 𝐿 ∈ (ℤ𝐾))
3 eluzfz1 13119 . . 3 (𝐿 ∈ (ℤ𝐾) → 𝐾 ∈ (𝐾...𝐿))
42, 3syl 17 . 2 ((𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ∧ 𝐾𝐿) → 𝐾 ∈ (𝐾...𝐿))
5 eluzfz2 13120 . . . 4 (𝐿 ∈ (ℤ𝐾) → 𝐿 ∈ (𝐾...𝐿))
62, 5syl 17 . . 3 ((𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ∧ 𝐾𝐿) → 𝐿 ∈ (𝐾...𝐿))
7 ssel2 3895 . . . . . . . 8 (((𝐾...𝐿) ⊆ (𝑀...𝑁) ∧ 𝐾 ∈ (𝐾...𝐿)) → 𝐾 ∈ (𝑀...𝑁))
8 ssel2 3895 . . . . . . . . . . 11 (((𝐾...𝐿) ⊆ (𝑀...𝑁) ∧ 𝐿 ∈ (𝐾...𝐿)) → 𝐿 ∈ (𝑀...𝑁))
9 elfzuz3 13109 . . . . . . . . . . 11 (𝐿 ∈ (𝑀...𝑁) → 𝑁 ∈ (ℤ𝐿))
10 eluz2 12444 . . . . . . . . . . . . 13 (𝐾 ∈ (ℤ𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑀𝐾))
11 eluz2 12444 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ (ℤ𝐿) ↔ (𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐿𝑁))
12 pm3.21 475 . . . . . . . . . . . . . . . . . 18 (𝐿𝑁 → (𝑀𝐾 → (𝑀𝐾𝐿𝑁)))
13123ad2ant3 1137 . . . . . . . . . . . . . . . . 17 ((𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐿𝑁) → (𝑀𝐾 → (𝑀𝐾𝐿𝑁)))
1411, 13sylbi 220 . . . . . . . . . . . . . . . 16 (𝑁 ∈ (ℤ𝐿) → (𝑀𝐾 → (𝑀𝐾𝐿𝑁)))
1514a1i 11 . . . . . . . . . . . . . . 15 ((𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ∧ 𝐾𝐿) → (𝑁 ∈ (ℤ𝐿) → (𝑀𝐾 → (𝑀𝐾𝐿𝑁))))
1615com13 88 . . . . . . . . . . . . . 14 (𝑀𝐾 → (𝑁 ∈ (ℤ𝐿) → ((𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ∧ 𝐾𝐿) → (𝑀𝐾𝐿𝑁))))
17163ad2ant3 1137 . . . . . . . . . . . . 13 ((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑀𝐾) → (𝑁 ∈ (ℤ𝐿) → ((𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ∧ 𝐾𝐿) → (𝑀𝐾𝐿𝑁))))
1810, 17sylbi 220 . . . . . . . . . . . 12 (𝐾 ∈ (ℤ𝑀) → (𝑁 ∈ (ℤ𝐿) → ((𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ∧ 𝐾𝐿) → (𝑀𝐾𝐿𝑁))))
19 elfzuz 13108 . . . . . . . . . . . 12 (𝐾 ∈ (𝑀...𝑁) → 𝐾 ∈ (ℤ𝑀))
2018, 19syl11 33 . . . . . . . . . . 11 (𝑁 ∈ (ℤ𝐿) → (𝐾 ∈ (𝑀...𝑁) → ((𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ∧ 𝐾𝐿) → (𝑀𝐾𝐿𝑁))))
218, 9, 203syl 18 . . . . . . . . . 10 (((𝐾...𝐿) ⊆ (𝑀...𝑁) ∧ 𝐿 ∈ (𝐾...𝐿)) → (𝐾 ∈ (𝑀...𝑁) → ((𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ∧ 𝐾𝐿) → (𝑀𝐾𝐿𝑁))))
2221ex 416 . . . . . . . . 9 ((𝐾...𝐿) ⊆ (𝑀...𝑁) → (𝐿 ∈ (𝐾...𝐿) → (𝐾 ∈ (𝑀...𝑁) → ((𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ∧ 𝐾𝐿) → (𝑀𝐾𝐿𝑁)))))
2322com4t 93 . . . . . . . 8 (𝐾 ∈ (𝑀...𝑁) → ((𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ∧ 𝐾𝐿) → ((𝐾...𝐿) ⊆ (𝑀...𝑁) → (𝐿 ∈ (𝐾...𝐿) → (𝑀𝐾𝐿𝑁)))))
247, 23syl 17 . . . . . . 7 (((𝐾...𝐿) ⊆ (𝑀...𝑁) ∧ 𝐾 ∈ (𝐾...𝐿)) → ((𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ∧ 𝐾𝐿) → ((𝐾...𝐿) ⊆ (𝑀...𝑁) → (𝐿 ∈ (𝐾...𝐿) → (𝑀𝐾𝐿𝑁)))))
2524ex 416 . . . . . 6 ((𝐾...𝐿) ⊆ (𝑀...𝑁) → (𝐾 ∈ (𝐾...𝐿) → ((𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ∧ 𝐾𝐿) → ((𝐾...𝐿) ⊆ (𝑀...𝑁) → (𝐿 ∈ (𝐾...𝐿) → (𝑀𝐾𝐿𝑁))))))
2625com24 95 . . . . 5 ((𝐾...𝐿) ⊆ (𝑀...𝑁) → ((𝐾...𝐿) ⊆ (𝑀...𝑁) → ((𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ∧ 𝐾𝐿) → (𝐾 ∈ (𝐾...𝐿) → (𝐿 ∈ (𝐾...𝐿) → (𝑀𝐾𝐿𝑁))))))
2726pm2.43i 52 . . . 4 ((𝐾...𝐿) ⊆ (𝑀...𝑁) → ((𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ∧ 𝐾𝐿) → (𝐾 ∈ (𝐾...𝐿) → (𝐿 ∈ (𝐾...𝐿) → (𝑀𝐾𝐿𝑁)))))
2827com14 96 . . 3 (𝐿 ∈ (𝐾...𝐿) → ((𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ∧ 𝐾𝐿) → (𝐾 ∈ (𝐾...𝐿) → ((𝐾...𝐿) ⊆ (𝑀...𝑁) → (𝑀𝐾𝐿𝑁)))))
296, 28mpcom 38 . 2 ((𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ∧ 𝐾𝐿) → (𝐾 ∈ (𝐾...𝐿) → ((𝐾...𝐿) ⊆ (𝑀...𝑁) → (𝑀𝐾𝐿𝑁))))
304, 29mpd 15 1 ((𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ∧ 𝐾𝐿) → ((𝐾...𝐿) ⊆ (𝑀...𝑁) → (𝑀𝐾𝐿𝑁)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399  w3a 1089  wcel 2110  wss 3866   class class class wbr 5053  cfv 6380  (class class class)co 7213  cle 10868  cz 12176  cuz 12438  ...cfz 13095
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2708  ax-sep 5192  ax-nul 5199  ax-pow 5258  ax-pr 5322  ax-un 7523  ax-cnex 10785  ax-resscn 10786  ax-pre-lttri 10803
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2071  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3410  df-sbc 3695  df-csb 3812  df-dif 3869  df-un 3871  df-in 3873  df-ss 3883  df-nul 4238  df-if 4440  df-pw 4515  df-sn 4542  df-pr 4544  df-op 4548  df-uni 4820  df-iun 4906  df-br 5054  df-opab 5116  df-mpt 5136  df-id 5455  df-xp 5557  df-rel 5558  df-cnv 5559  df-co 5560  df-dm 5561  df-rn 5562  df-res 5563  df-ima 5564  df-iota 6338  df-fun 6382  df-fn 6383  df-f 6384  df-f1 6385  df-fo 6386  df-f1o 6387  df-fv 6388  df-ov 7216  df-oprab 7217  df-mpo 7218  df-1st 7761  df-2nd 7762  df-er 8391  df-en 8627  df-dom 8628  df-sdom 8629  df-pnf 10869  df-mnf 10870  df-xr 10871  df-ltxr 10872  df-le 10873  df-neg 11065  df-z 12177  df-uz 12439  df-fz 13096
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator