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

Theorem uzssz 11168
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 11152 . . . . 5  |-  ZZ>= : ZZ --> ~P ZZ
21ffvelrni 6005 . . . 4  |-  ( M  e.  ZZ  ->  ( ZZ>=
`  M )  e. 
~P ZZ )
32elpwid 3929 . . 3  |-  ( M  e.  ZZ  ->  ( ZZ>=
`  M )  C_  ZZ )
41fdmi 5717 . . 3  |-  dom  ZZ>=  =  ZZ
53, 4eleq2s 2548 . 2  |-  ( M  e.  dom  ZZ>=  ->  ( ZZ>=
`  M )  C_  ZZ )
6 ndmfv 5872 . . 3  |-  ( -.  M  e.  dom  ZZ>=  -> 
( ZZ>= `  M )  =  (/) )
7 0ss 3731 . . 3  |-  (/)  C_  ZZ
86, 7syl6eqss 3450 . 2  |-  ( -.  M  e.  dom  ZZ>=  -> 
( ZZ>= `  M )  C_  ZZ )
95, 8pm2.61i 169 1  |-  ( ZZ>= `  M )  C_  ZZ
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    e. wcel 1891    C_ wss 3372   (/)c0 3699   ~Pcpw 3919   dom cdm 4812   ` cfv 5561   ZZcz 10927   ZZ>=cuz 11149
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1673  ax-4 1686  ax-5 1762  ax-6 1809  ax-7 1855  ax-8 1893  ax-9 1900  ax-10 1919  ax-11 1924  ax-12 1937  ax-13 2092  ax-ext 2432  ax-sep 4497  ax-nul 4506  ax-pow 4554  ax-pr 4612  ax-cnex 9582  ax-resscn 9583
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 987  df-3an 988  df-tru 1451  df-ex 1668  df-nf 1672  df-sb 1802  df-eu 2304  df-mo 2305  df-clab 2439  df-cleq 2445  df-clel 2448  df-nfc 2582  df-ne 2624  df-ral 2742  df-rex 2743  df-rab 2746  df-v 3015  df-sbc 3236  df-dif 3375  df-un 3377  df-in 3379  df-ss 3386  df-nul 3700  df-if 3850  df-pw 3921  df-sn 3937  df-pr 3939  df-op 3943  df-uni 4169  df-br 4375  df-opab 4434  df-mpt 4435  df-id 4727  df-xp 4818  df-rel 4819  df-cnv 4820  df-co 4821  df-dm 4822  df-rn 4823  df-res 4824  df-ima 4825  df-iota 5525  df-fun 5563  df-fn 5564  df-f 5565  df-fv 5569  df-ov 6279  df-neg 9850  df-z 10928  df-uz 11150
This theorem is referenced by:  uzwo  11212  uzwo2  11213  uzinfmiOLD  11229  infssuzle  11234  infssuzcl  11235  infmssuzleOLD  11236  infmssuzclOLD  11237  uzsupss  11246  uzwo3  11249  fzof  11910  uzsup  12084  cau3  13429  caubnd  13432  limsupgre  13553  limsupgreOLD  13554  rlimclim  13621  climz  13624  climaddc1  13709  climmulc2  13711  climsubc1  13712  climsubc2  13713  climlec2  13733  isercolllem1  13739  isercolllem2  13740  isercoll  13742  caurcvg  13753  caurcvgOLD  13754  caucvg  13756  iseraltlem1  13759  iseraltlem2  13760  iseraltlem3  13761  summolem2a  13792  summolem2  13793  zsum  13795  fsumcvg3  13806  climfsum  13891  divcnvshft  13924  clim2prod  13955  ntrivcvg  13964  ntrivcvgfvn0  13966  ntrivcvgtail  13967  ntrivcvgmullem  13968  ntrivcvgmul  13969  prodrblem  13994  prodmolem2a  13999  prodmolem2  14000  zprod  14002  4sqlem11  14910  gsumval3  17552  lmbrf  20287  lmres  20327  uzrest  20923  uzfbas  20924  lmflf  21031  lmmbrf  22243  iscau4  22260  iscauf  22261  caucfil  22264  lmclimf  22284  mbfsup  22632  mbflimsup  22635  mbflimsupOLD  22636  ig1pdvds  23140  ig1pdvdsOLD  23146  ulmval  23347  ulmpm  23350  2sqlem6  24309  ballotlemfc0  29331  ballotlemfcc  29332  ballotlemiex  29340  ballotlemsdom  29350  ballotlemsima  29354  ballotlemrv2  29360  ballotlemiexOLD  29378  ballotlemsdomOLD  29388  ballotlemsimaOLD  29392  ballotlemrv2OLD  29398  erdszelem4  29923  erdszelem8  29927  caures  32091  diophin  35617  irrapxlem1  35668  monotuz  35791  hashnzfzclim  36672  uzmptshftfval  36696  uzct  37399  uzfissfz  37580  ssuzfz  37603  ioodvbdlimc1lem2  37846  ioodvbdlimc1lem2OLD  37848  ioodvbdlimc2lem  37850  ioodvbdlimc2lemOLD  37851  sge0isum  38328
  Copyright terms: Public domain W3C validator