Theorem uzssz 12889

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

Step	Hyp	Ref	Expression
1		uzf 12871	. . . . 5 ⊢ ℤ≥:ℤ⟶𝒫 ℤ
2	1	ffvelcdmi 7078	. . . 4 ⊢ (𝑀 ∈ ℤ → (ℤ≥‘𝑀) ∈ 𝒫 ℤ)
3	2	elpwid 4570	. . 3 ⊢ (𝑀 ∈ ℤ → (ℤ≥‘𝑀) ⊆ ℤ)
4	1	fdmi 6717	. . 3 ⊢ dom ℤ≥ = ℤ
5	3, 4	eleq2s 2880	. 2 ⊢ (𝑀 ∈ dom ℤ≥ → (ℤ≥‘𝑀) ⊆ ℤ)
6		ndmfv 6913	. . 3 ⊢ (¬ 𝑀 ∈ dom ℤ≥ → (ℤ≥‘𝑀) = ∅)
7		0ss 4356	. . 3 ⊢ ∅ ⊆ ℤ
8	6, 7	eqsstrdi 3980	. 2 ⊢ (¬ 𝑀 ∈ dom ℤ≥ → (ℤ≥‘𝑀) ⊆ ℤ)
9	5, 8	pm2.61i 184	1 ⊢ (ℤ≥‘𝑀) ⊆ ℤ

This proof depends on syntax axioms:  ¬ wn 3   ∈ wcel 2142   ⊆ wss 3904  ∅c0 4285  𝒫 cpw 4561  dom cdm 5660  ‘cfv 6536  ℤcz 12597  ℤ_≥cuz 12868

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734  ax-sep 5256  ax-nul 5268  ax-pr 5403  ax-cnex 11162  ax-resscn 11163

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1103  df-3an 1104  df-tru 1572  df-fal 1582  df-ex 1809  df-nf 1813  df-sb 2096  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-ral 3079  df-rex 3089  df-rab 3416  df-v 3456  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4487  df-pw 4563  df-sn 4589  df-pr 4591  df-op 4595  df-uni 4872  df-br 5109  df-opab 5173  df-mpt 5192  df-id 5555  df-xp 5666  df-rel 5667  df-cnv 5668  df-co 5669  df-dm 5670  df-rn 5671  df-res 5672  df-ima 5673  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-fv 6544  df-ov 7415  df-neg 11450  df-z 12598  df-uz 12869

This theorem is used by:  uzssre  12890  uzwo  12941  uzwo2  12942  infssuzle  12961  infssuzcl  12962  uzsupss  12970  uzwo3  12973  uzsup  13903  cau3  15414  caubnd  15417  limsupgre  15539  rlimclim  15604  climz  15607  climaddc1  15693  climmulc2  15695  climsubc1  15696  climsubc2  15697  climlec2  15717  isercolllem1  15723  isercolllem2  15724  isercoll  15726  caurcvg  15735  caucvg  15737  iseraltlem1  15740  iseraltlem2  15741  iseraltlem3  15742  summolem2a  15773  summolem2  15774  zsum  15776  fsumcvg3  15787  climfsum  15879  divcnvshft  15916  clim2prod  15949  ntrivcvg  15958  ntrivcvgfvn0  15960  ntrivcvgtail  15961  ntrivcvgmullem  15962  ntrivcvgmul  15963  prodrblem  15990  prodmolem2a  15995  prodmolem2  15996  zprod  15998  4sqlem11  17021  gsumval3  19983  lmbrf  23428  lmres  23468  uzrest  24065  uzfbas  24066  lmflf  24173  lmmbrf  25432  iscau4  25449  iscauf  25450  caucfil  25453  lmclimf  25474  mbfsup  25834  mbflimsup  25836  ig1pdvds  26348  ulmval  26554  ulmpm  26557  2sqlem6  27598  ballotlemfc0  34892  ballotlemfcc  34893  ballotlemiex  34901  ballotlemsima  34915  ballotlemrv2  34921  breprexplemc  35028  erdszelem4  35694  erdszelem8  35698  caures  38439  diophin  43531  irrapxlem1  43577  monotuz  43696  hashnzfzclim  45060  uzmptshftfval  45084  uzct  45811  uzfissfz  46070  ssuzfz  46093  uzssre2  46149  uzssz2  46198  uzinico2  46305  fnlimfvre  46416  climleltrp  46418  limsupequzmpt2  46460  limsupequzlem  46464  liminfequzmpt2  46533  ioodvbdlimc1lem2  46674  ioodvbdlimc2lem  46676  sge0isum  47169  smflimlem1  47513  smflimlem2  47514  smflim  47519