MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  uzss Structured version   Visualization version   GIF version

Theorem uzss 11906
Description: Subset relationship for two sets of upper integers. (Contributed by NM, 5-Sep-2005.)
Assertion
Ref Expression
uzss (𝑁 ∈ (ℤ𝑀) → (ℤ𝑁) ⊆ (ℤ𝑀))

Proof of Theorem uzss
Dummy variable 𝑘 is distinct from all other variables.
StepHypRef Expression
1 eluzle 11898 . . . . . 6 (𝑁 ∈ (ℤ𝑀) → 𝑀𝑁)
21adantr 472 . . . . 5 ((𝑁 ∈ (ℤ𝑀) ∧ 𝑘 ∈ ℤ) → 𝑀𝑁)
3 eluzel2 11890 . . . . . . 7 (𝑁 ∈ (ℤ𝑀) → 𝑀 ∈ ℤ)
4 eluzelz 11895 . . . . . . 7 (𝑁 ∈ (ℤ𝑀) → 𝑁 ∈ ℤ)
53, 4jca 507 . . . . . 6 (𝑁 ∈ (ℤ𝑀) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))
6 zletr 11667 . . . . . . 7 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑘 ∈ ℤ) → ((𝑀𝑁𝑁𝑘) → 𝑀𝑘))
763expa 1147 . . . . . 6 (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑘 ∈ ℤ) → ((𝑀𝑁𝑁𝑘) → 𝑀𝑘))
85, 7sylan 575 . . . . 5 ((𝑁 ∈ (ℤ𝑀) ∧ 𝑘 ∈ ℤ) → ((𝑀𝑁𝑁𝑘) → 𝑀𝑘))
92, 8mpand 686 . . . 4 ((𝑁 ∈ (ℤ𝑀) ∧ 𝑘 ∈ ℤ) → (𝑁𝑘𝑀𝑘))
109imdistanda 567 . . 3 (𝑁 ∈ (ℤ𝑀) → ((𝑘 ∈ ℤ ∧ 𝑁𝑘) → (𝑘 ∈ ℤ ∧ 𝑀𝑘)))
11 eluz1 11889 . . . 4 (𝑁 ∈ ℤ → (𝑘 ∈ (ℤ𝑁) ↔ (𝑘 ∈ ℤ ∧ 𝑁𝑘)))
124, 11syl 17 . . 3 (𝑁 ∈ (ℤ𝑀) → (𝑘 ∈ (ℤ𝑁) ↔ (𝑘 ∈ ℤ ∧ 𝑁𝑘)))
13 eluz1 11889 . . . 4 (𝑀 ∈ ℤ → (𝑘 ∈ (ℤ𝑀) ↔ (𝑘 ∈ ℤ ∧ 𝑀𝑘)))
143, 13syl 17 . . 3 (𝑁 ∈ (ℤ𝑀) → (𝑘 ∈ (ℤ𝑀) ↔ (𝑘 ∈ ℤ ∧ 𝑀𝑘)))
1510, 12, 143imtr4d 285 . 2 (𝑁 ∈ (ℤ𝑀) → (𝑘 ∈ (ℤ𝑁) → 𝑘 ∈ (ℤ𝑀)))
1615ssrdv 3766 1 (𝑁 ∈ (ℤ𝑀) → (ℤ𝑁) ⊆ (ℤ𝑀))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384  wcel 2155  wss 3731   class class class wbr 4808  cfv 6067  cle 10328  cz 11623  cuz 11885
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2069  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2349  ax-ext 2742  ax-sep 4940  ax-nul 4948  ax-pow 5000  ax-pr 5061  ax-un 7146  ax-cnex 10244  ax-resscn 10245  ax-pre-lttri 10262  ax-pre-lttrn 10263
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2062  df-mo 2564  df-eu 2581  df-clab 2751  df-cleq 2757  df-clel 2760  df-nfc 2895  df-ne 2937  df-nel 3040  df-ral 3059  df-rex 3060  df-rab 3063  df-v 3351  df-sbc 3596  df-csb 3691  df-dif 3734  df-un 3736  df-in 3738  df-ss 3745  df-nul 4079  df-if 4243  df-pw 4316  df-sn 4334  df-pr 4336  df-op 4340  df-uni 4594  df-br 4809  df-opab 4871  df-mpt 4888  df-id 5184  df-xp 5282  df-rel 5283  df-cnv 5284  df-co 5285  df-dm 5286  df-rn 5287  df-res 5288  df-ima 5289  df-iota 6030  df-fun 6069  df-fn 6070  df-f 6071  df-f1 6072  df-fo 6073  df-f1o 6074  df-fv 6075  df-ov 6844  df-er 7946  df-en 8160  df-dom 8161  df-sdom 8162  df-pnf 10329  df-mnf 10330  df-xr 10331  df-ltxr 10332  df-le 10333  df-neg 10522  df-z 11624  df-uz 11886
This theorem is referenced by:  uzin  11919  uznnssnn  11934  fzopth  12584  4fvwrd4  12666  fzouzsplit  12710  seqfeq2  13030  rexuzre  14378  cau3lem  14380  climsup  14686  isumsplit  14857  isumrpcl  14860  cvgrat  14899  clim2prod  14904  fprodntriv  14956  isprm3  15677  pcfac  15883  lmflf  22087  caucfil  23359  uniioombllem4  23643  mbflimsup  23723  ulmres  24432  ulmcaulem  24438  logfaclbnd  25237  axlowdimlem17  26128  clwwlkinwwlk  27251  fz2ssnn0  29930  poimirlem1  33766  poimirlem2  33767  poimirlem6  33771  poimirlem7  33772  poimirlem20  33785  uzssd  40203  climinf  40408  climsuse  40410  climresmpt  40461  climleltrp  40478  limsupequzlem  40524  supcnvlimsup  40542  ioodvbdlimc1lem1  40716  ioodvbdlimc1lem2  40717  ioodvbdlimc2lem  40719  meaiininclem  41272  smflimlem2  41552  smflimsuplem2  41599  smflimsuplem3  41600  smflimsuplem4  41601  smflimsuplem5  41602  smflimsuplem6  41603  smflimsuplem7  41604  fzoopth  42003
  Copyright terms: Public domain W3C validator