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

Theorem uzssz 10892
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  |-  ( ZZ>= `  M )  C_  ZZ

Proof of Theorem uzssz
StepHypRef Expression
1 uzf 10876 . . . . 5  |-  ZZ>= : ZZ --> ~P ZZ
21ffvelrni 5854 . . . 4  |-  ( M  e.  ZZ  ->  ( ZZ>=
`  M )  e. 
~P ZZ )
32elpwid 3882 . . 3  |-  ( M  e.  ZZ  ->  ( ZZ>=
`  M )  C_  ZZ )
41fdmi 5576 . . 3  |-  dom  ZZ>=  =  ZZ
53, 4eleq2s 2535 . 2  |-  ( M  e.  dom  ZZ>=  ->  ( ZZ>=
`  M )  C_  ZZ )
6 ndmfv 5726 . . 3  |-  ( -.  M  e.  dom  ZZ>=  -> 
( ZZ>= `  M )  =  (/) )
7 0ss 3678 . . 3  |-  (/)  C_  ZZ
86, 7syl6eqss 3418 . 2  |-  ( -.  M  e.  dom  ZZ>=  -> 
( ZZ>= `  M )  C_  ZZ )
95, 8pm2.61i 164 1  |-  ( ZZ>= `  M )  C_  ZZ
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    e. wcel 1756    C_ wss 3340   (/)c0 3649   ~Pcpw 3872   dom cdm 4852   ` cfv 5430   ZZcz 10658   ZZ>=cuz 10873
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4425  ax-nul 4433  ax-pow 4482  ax-pr 4543  ax-cnex 9350  ax-resscn 9351
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-ne 2620  df-ral 2732  df-rex 2733  df-rab 2736  df-v 2986  df-sbc 3199  df-dif 3343  df-un 3345  df-in 3347  df-ss 3354  df-nul 3650  df-if 3804  df-pw 3874  df-sn 3890  df-pr 3892  df-op 3896  df-uni 4104  df-br 4305  df-opab 4363  df-mpt 4364  df-id 4648  df-xp 4858  df-rel 4859  df-cnv 4860  df-co 4861  df-dm 4862  df-rn 4863  df-res 4864  df-ima 4865  df-iota 5393  df-fun 5432  df-fn 5433  df-f 5434  df-fv 5438  df-ov 6106  df-neg 9610  df-z 10659  df-uz 10874
This theorem is referenced by:  uzwo  10929  uzwoOLD  10930  uzwo2  10931  uzinfmi  10946  infmssuzle  10949  infmssuzcl  10950  uzsupss  10959  uzwo3  10960  fzof  11562  uzsup  11714  seqshft  12586  cau3  12855  caubnd  12858  limsupgre  12971  rlimclim  13036  climz  13039  climaddc1  13124  climmulc2  13126  climsubc1  13127  climsubc2  13128  climlec2  13148  isercolllem1  13154  isercolllem2  13155  isercoll  13157  caurcvg  13166  caucvg  13168  iseraltlem1  13171  iseraltlem2  13172  iseraltlem3  13173  summolem2a  13204  summolem2  13205  zsum  13207  fsumcvg3  13218  climfsum  13295  4sqlem11  14028  gsumval3OLD  16394  gsumval3  16397  lmbrf  18876  lmres  18916  uzrest  19482  uzfbas  19483  lmflf  19590  lmmbrf  20785  iscau4  20802  iscauf  20803  caucfil  20806  lmclimf  20826  mbfsup  21154  mbflimsup  21156  ig1pdvds  21660  ulmval  21857  ulmpm  21860  2sqlem6  22720  ballotlemfc0  26887  ballotlemfcc  26888  ballotlemiex  26896  ballotlemsdom  26906  ballotlemsima  26910  ballotlemrv2  26916  erdszelem4  27094  erdszelem8  27098  divcnvshft  27410  clim2prod  27415  ntrivcvg  27424  ntrivcvgfvn0  27426  ntrivcvgtail  27427  ntrivcvgmullem  27428  ntrivcvgmul  27429  prodrblem  27454  prodmolem2a  27459  prodmolem2  27460  zprod  27462  caures  28668  diophin  29123  irrapxlem1  29175  monotuz  29294
  Copyright terms: Public domain W3C validator