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

Theorem uzssz 11100
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 11084 . . . . 5  |-  ZZ>= : ZZ --> ~P ZZ
21ffvelrni 6019 . . . 4  |-  ( M  e.  ZZ  ->  ( ZZ>=
`  M )  e. 
~P ZZ )
32elpwid 4020 . . 3  |-  ( M  e.  ZZ  ->  ( ZZ>=
`  M )  C_  ZZ )
41fdmi 5735 . . 3  |-  dom  ZZ>=  =  ZZ
53, 4eleq2s 2575 . 2  |-  ( M  e.  dom  ZZ>=  ->  ( ZZ>=
`  M )  C_  ZZ )
6 ndmfv 5889 . . 3  |-  ( -.  M  e.  dom  ZZ>=  -> 
( ZZ>= `  M )  =  (/) )
7 0ss 3814 . . 3  |-  (/)  C_  ZZ
86, 7syl6eqss 3554 . 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 1767    C_ wss 3476   (/)c0 3785   ~Pcpw 4010   dom cdm 4999   ` cfv 5587   ZZcz 10863   ZZ>=cuz 11081
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4568  ax-nul 4576  ax-pow 4625  ax-pr 4686  ax-cnex 9547  ax-resscn 9548
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2819  df-rex 2820  df-rab 2823  df-v 3115  df-sbc 3332  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-pw 4012  df-sn 4028  df-pr 4030  df-op 4034  df-uni 4246  df-br 4448  df-opab 4506  df-mpt 4507  df-id 4795  df-xp 5005  df-rel 5006  df-cnv 5007  df-co 5008  df-dm 5009  df-rn 5010  df-res 5011  df-ima 5012  df-iota 5550  df-fun 5589  df-fn 5590  df-f 5591  df-fv 5595  df-ov 6286  df-neg 9807  df-z 10864  df-uz 11082
This theorem is referenced by:  uzwo  11143  uzwoOLD  11144  uzwo2  11145  uzinfmi  11160  infmssuzle  11163  infmssuzcl  11164  uzsupss  11173  uzwo3  11176  fzof  11793  uzsup  11957  seqshft  12880  cau3  13150  caubnd  13153  limsupgre  13266  rlimclim  13331  climz  13334  climaddc1  13419  climmulc2  13421  climsubc1  13422  climsubc2  13423  climlec2  13443  isercolllem1  13449  isercolllem2  13450  isercoll  13452  caurcvg  13461  caucvg  13463  iseraltlem1  13466  iseraltlem2  13467  iseraltlem3  13468  summolem2a  13499  summolem2  13500  zsum  13502  fsumcvg3  13513  climfsum  13596  4sqlem11  14331  gsumval3OLD  16708  gsumval3  16711  lmbrf  19543  lmres  19583  uzrest  20149  uzfbas  20150  lmflf  20257  lmmbrf  21452  iscau4  21469  iscauf  21470  caucfil  21473  lmclimf  21493  mbfsup  21822  mbflimsup  21824  ig1pdvds  22328  ulmval  22525  ulmpm  22528  2sqlem6  23388  ballotlemfc0  28087  ballotlemfcc  28088  ballotlemiex  28096  ballotlemsdom  28106  ballotlemsima  28110  ballotlemrv2  28116  erdszelem4  28294  erdszelem8  28298  divcnvshft  28610  clim2prod  28615  ntrivcvg  28624  ntrivcvgfvn0  28626  ntrivcvgtail  28627  ntrivcvgmullem  28628  ntrivcvgmul  28629  prodrblem  28654  prodmolem2a  28659  prodmolem2  28660  zprod  28662  caures  29872  diophin  30326  irrapxlem1  30378  monotuz  30497  hashnzfzclim  30843  ioodvbdlimc1lem2  31278  ioodvbdlimc2lem  31280
  Copyright terms: Public domain W3C validator