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

Theorem uzssz 11583
Description: An upper set of integers is a subset of all integers. (Contributed by NM, 2-Sep-2005.) (Revised by Mario Carneiro, 3-Nov-2013.)
Assertion
Ref Expression
uzssz (ℤ𝑀) ⊆ ℤ

Proof of Theorem uzssz
StepHypRef Expression
1 uzf 11566 . . . . 5 :ℤ⟶𝒫 ℤ
21ffvelrni 6266 . . . 4 (𝑀 ∈ ℤ → (ℤ𝑀) ∈ 𝒫 ℤ)
32elpwid 4118 . . 3 (𝑀 ∈ ℤ → (ℤ𝑀) ⊆ ℤ)
41fdmi 5965 . . 3 dom ℤ = ℤ
53, 4eleq2s 2706 . 2 (𝑀 ∈ dom ℤ → (ℤ𝑀) ⊆ ℤ)
6 ndmfv 6128 . . 3 𝑀 ∈ dom ℤ → (ℤ𝑀) = ∅)
7 0ss 3924 . . 3 ∅ ⊆ ℤ
86, 7syl6eqss 3618 . 2 𝑀 ∈ dom ℤ → (ℤ𝑀) ⊆ ℤ)
95, 8pm2.61i 175 1 (ℤ𝑀) ⊆ ℤ
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wcel 1977  wss 3540  c0 3874  𝒫 cpw 4108  dom cdm 5038  cfv 5804  cz 11254  cuz 11563
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-cnex 9871  ax-resscn 9872
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-sbc 3403  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-opab 4644  df-mpt 4645  df-id 4953  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-fv 5812  df-ov 6552  df-neg 10148  df-z 11255  df-uz 11564
This theorem is referenced by:  uzwo  11627  uzwo2  11628  infssuzle  11647  infssuzcl  11648  uzsupss  11656  uzwo3  11659  fzof  12336  uzsup  12524  cau3  13943  caubnd  13946  limsupgre  14060  rlimclim  14125  climz  14128  climaddc1  14213  climmulc2  14215  climsubc1  14216  climsubc2  14217  climlec2  14237  isercolllem1  14243  isercolllem2  14244  isercoll  14246  caurcvg  14255  caucvg  14257  iseraltlem1  14260  iseraltlem2  14261  iseraltlem3  14262  summolem2a  14293  summolem2  14294  zsum  14296  fsumcvg3  14307  climfsum  14393  divcnvshft  14426  clim2prod  14459  ntrivcvg  14468  ntrivcvgfvn0  14470  ntrivcvgtail  14471  ntrivcvgmullem  14472  ntrivcvgmul  14473  prodrblem  14498  prodmolem2a  14503  prodmolem2  14504  zprod  14506  4sqlem11  15497  gsumval3  18131  lmbrf  20874  lmres  20914  uzrest  21511  uzfbas  21512  lmflf  21619  lmmbrf  22868  iscau4  22885  iscauf  22886  caucfil  22889  lmclimf  22910  mbfsup  23237  mbflimsup  23239  ig1pdvds  23740  ulmval  23938  ulmpm  23941  2sqlem6  24948  ballotlemfc0  29881  ballotlemfcc  29882  ballotlemiex  29890  ballotlemsdom  29900  ballotlemsima  29904  ballotlemrv2  29910  erdszelem4  30430  erdszelem8  30434  caures  32726  diophin  36354  irrapxlem1  36404  monotuz  36524  hashnzfzclim  37543  uzmptshftfval  37567  uzct  38257  uzfissfz  38483  ssuzfz  38506  fnlimfvre  38741  climleltrp  38743  ioodvbdlimc1lem2  38822  ioodvbdlimc2lem  38824  sge0isum  39320  smflimlem1  39657  smflimlem2  39658  smflim  39663
  Copyright terms: Public domain W3C validator