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

Theorem uzssz 12261
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 12243 . . . . 5 :ℤ⟶𝒫 ℤ
21ffvelrni 6841 . . . 4 (𝑀 ∈ ℤ → (ℤ𝑀) ∈ 𝒫 ℤ)
32elpwid 4533 . . 3 (𝑀 ∈ ℤ → (ℤ𝑀) ⊆ ℤ)
41fdmi 6514 . . 3 dom ℤ = ℤ
53, 4eleq2s 2934 . 2 (𝑀 ∈ dom ℤ → (ℤ𝑀) ⊆ ℤ)
6 ndmfv 6691 . . 3 𝑀 ∈ dom ℤ → (ℤ𝑀) = ∅)
7 0ss 4333 . . 3 ∅ ⊆ ℤ
86, 7eqsstrdi 4007 . 2 𝑀 ∈ dom ℤ → (ℤ𝑀) ⊆ ℤ)
95, 8pm2.61i 185 1 (ℤ𝑀) ⊆ ℤ
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wcel 2115  wss 3919  c0 4276  𝒫 cpw 4522  dom cdm 5542  cfv 6343  cz 11978  cuz 12240
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796  ax-sep 5189  ax-nul 5196  ax-pow 5253  ax-pr 5317  ax-cnex 10591  ax-resscn 10592
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2624  df-eu 2655  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ne 3015  df-ral 3138  df-rex 3139  df-rab 3142  df-v 3482  df-sbc 3759  df-dif 3922  df-un 3924  df-in 3926  df-ss 3936  df-nul 4277  df-if 4451  df-pw 4524  df-sn 4551  df-pr 4553  df-op 4557  df-uni 4825  df-br 5053  df-opab 5115  df-mpt 5133  df-id 5447  df-xp 5548  df-rel 5549  df-cnv 5550  df-co 5551  df-dm 5552  df-rn 5553  df-res 5554  df-ima 5555  df-iota 6302  df-fun 6345  df-fn 6346  df-f 6347  df-fv 6351  df-ov 7152  df-neg 10871  df-z 11979  df-uz 12241
This theorem is referenced by:  uzwo  12308  uzwo2  12309  infssuzle  12328  infssuzcl  12329  uzsupss  12337  uzwo3  12340  uzsup  13235  cau3  14715  caubnd  14718  limsupgre  14838  rlimclim  14903  climz  14906  climaddc1  14991  climmulc2  14993  climsubc1  14994  climsubc2  14995  climlec2  15015  isercolllem1  15021  isercolllem2  15022  isercoll  15024  caurcvg  15033  caucvg  15035  iseraltlem1  15038  iseraltlem2  15039  iseraltlem3  15040  summolem2a  15072  summolem2  15073  zsum  15075  fsumcvg3  15086  climfsum  15175  divcnvshft  15210  clim2prod  15244  ntrivcvg  15253  ntrivcvgfvn0  15255  ntrivcvgtail  15256  ntrivcvgmullem  15257  ntrivcvgmul  15258  prodrblem  15283  prodmolem2a  15288  prodmolem2  15289  zprod  15291  4sqlem11  16289  gsumval3  19027  lmbrf  21871  lmres  21911  uzrest  22508  uzfbas  22509  lmflf  22616  lmmbrf  23872  iscau4  23889  iscauf  23890  caucfil  23893  lmclimf  23914  mbfsup  24274  mbflimsup  24276  ig1pdvds  24783  ulmval  24981  ulmpm  24984  2sqlem6  26013  ballotlemfc0  31810  ballotlemfcc  31811  ballotlemiex  31819  ballotlemsdom  31829  ballotlemsima  31833  ballotlemrv2  31839  breprexplemc  31963  erdszelem4  32501  erdszelem8  32505  caures  35146  diophin  39633  irrapxlem1  39683  monotuz  39802  hashnzfzclim  40950  uzmptshftfval  40974  uzct  41621  uzfissfz  41888  ssuzfz  41911  uzssre  41963  uzssre2  41974  uzssz2  42025  uzinico2  42129  fnlimfvre  42246  climleltrp  42248  limsupequzmpt2  42290  limsupequzlem  42294  liminfequzmpt2  42363  ioodvbdlimc1lem2  42504  ioodvbdlimc2lem  42506  sge0isum  42996  smflimlem1  43334  smflimlem2  43335  smflim  43340
  Copyright terms: Public domain W3C validator