![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > fzss1 | Structured version Visualization version GIF version |
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 |
---|---|
fzss1 | ⊢ (𝐾 ∈ (ℤ≥‘𝑀) → (𝐾...𝑁) ⊆ (𝑀...𝑁)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elfzuz 13447 | . . . . 5 ⊢ (𝑘 ∈ (𝐾...𝑁) → 𝑘 ∈ (ℤ≥‘𝐾)) | |
2 | id 22 | . . . . 5 ⊢ (𝐾 ∈ (ℤ≥‘𝑀) → 𝐾 ∈ (ℤ≥‘𝑀)) | |
3 | uztrn 12790 | . . . . 5 ⊢ ((𝑘 ∈ (ℤ≥‘𝐾) ∧ 𝐾 ∈ (ℤ≥‘𝑀)) → 𝑘 ∈ (ℤ≥‘𝑀)) | |
4 | 1, 2, 3 | syl2anr 597 | . . . 4 ⊢ ((𝐾 ∈ (ℤ≥‘𝑀) ∧ 𝑘 ∈ (𝐾...𝑁)) → 𝑘 ∈ (ℤ≥‘𝑀)) |
5 | elfzuz3 13448 | . . . . 5 ⊢ (𝑘 ∈ (𝐾...𝑁) → 𝑁 ∈ (ℤ≥‘𝑘)) | |
6 | 5 | adantl 482 | . . . 4 ⊢ ((𝐾 ∈ (ℤ≥‘𝑀) ∧ 𝑘 ∈ (𝐾...𝑁)) → 𝑁 ∈ (ℤ≥‘𝑘)) |
7 | elfzuzb 13445 | . . . 4 ⊢ (𝑘 ∈ (𝑀...𝑁) ↔ (𝑘 ∈ (ℤ≥‘𝑀) ∧ 𝑁 ∈ (ℤ≥‘𝑘))) | |
8 | 4, 6, 7 | sylanbrc 583 | . . 3 ⊢ ((𝐾 ∈ (ℤ≥‘𝑀) ∧ 𝑘 ∈ (𝐾...𝑁)) → 𝑘 ∈ (𝑀...𝑁)) |
9 | 8 | ex 413 | . 2 ⊢ (𝐾 ∈ (ℤ≥‘𝑀) → (𝑘 ∈ (𝐾...𝑁) → 𝑘 ∈ (𝑀...𝑁))) |
10 | 9 | ssrdv 3953 | 1 ⊢ (𝐾 ∈ (ℤ≥‘𝑀) → (𝐾...𝑁) ⊆ (𝑀...𝑁)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 ∈ wcel 2106 ⊆ wss 3913 ‘cfv 6501 (class class class)co 7362 ℤ≥cuz 12772 ...cfz 13434 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2702 ax-sep 5261 ax-nul 5268 ax-pow 5325 ax-pr 5389 ax-un 7677 ax-cnex 11116 ax-resscn 11117 ax-pre-lttri 11134 ax-pre-lttrn 11135 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3or 1088 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2533 df-eu 2562 df-clab 2709 df-cleq 2723 df-clel 2809 df-nfc 2884 df-ne 2940 df-nel 3046 df-ral 3061 df-rex 3070 df-rab 3406 df-v 3448 df-sbc 3743 df-csb 3859 df-dif 3916 df-un 3918 df-in 3920 df-ss 3930 df-nul 4288 df-if 4492 df-pw 4567 df-sn 4592 df-pr 4594 df-op 4598 df-uni 4871 df-iun 4961 df-br 5111 df-opab 5173 df-mpt 5194 df-id 5536 df-xp 5644 df-rel 5645 df-cnv 5646 df-co 5647 df-dm 5648 df-rn 5649 df-res 5650 df-ima 5651 df-iota 6453 df-fun 6503 df-fn 6504 df-f 6505 df-f1 6506 df-fo 6507 df-f1o 6508 df-fv 6509 df-ov 7365 df-oprab 7366 df-mpo 7367 df-1st 7926 df-2nd 7927 df-er 8655 df-en 8891 df-dom 8892 df-sdom 8893 df-pnf 11200 df-mnf 11201 df-xr 11202 df-ltxr 11203 df-le 11204 df-neg 11397 df-z 12509 df-uz 12773 df-fz 13435 |
This theorem is referenced by: fzssnn 13495 fzp1ss 13502 ige2m1fz 13541 fzoss1 13609 fzossnn0 13613 sermono 13950 seqsplit 13951 seqf1olem2 13958 seqz 13966 seqcoll2 14376 swrdswrd 14605 swrdccatin2 14629 pfxccatin12lem2c 14630 pfxccatpfx2 14637 swrds2m 14842 mertenslem1 15780 reumodprminv 16687 prmgaplcmlem1 16934 structfn 17039 strleun 17040 cpmadugsumlemF 22262 ply1termlem 25601 dvply1 25681 ppisval2 26491 ppiltx 26563 chtlepsi 26591 chtublem 26596 chpub 26605 gausslemma2dlem3 26753 2lgslem1a 26776 chtppilimlem1 26858 pntlemq 26986 pntlemf 26990 axlowdimlem16 27969 axlowdimlem17 27970 axlowdim 27973 crctcshwlkn0lem3 28820 swrdrndisj 31881 esumpmono 32767 ballotlem2 33177 ballotlemfc0 33181 ballotlemfcc 33182 fsum2dsub 33309 chtvalz 33331 poimirlem1 36152 poimirlem2 36153 poimirlem4 36155 poimirlem6 36157 poimirlem7 36158 poimirlem15 36166 poimirlem16 36167 poimirlem19 36170 poimirlem20 36171 poimirlem23 36174 poimirlem27 36178 fdc 36277 jm2.23 41378 stoweidlem11 44372 elaa2lem 44594 iccpartgel 45741 |
Copyright terms: Public domain | W3C validator |