Theorem uzssz 12899

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 12881	. . . . 5 ⊢ ℤ≥:ℤ⟶𝒫 ℤ
2	1	ffvelcdmi 7103	. . . 4 ⊢ (𝑀 ∈ ℤ → (ℤ≥‘𝑀) ∈ 𝒫 ℤ)
3	2	elpwid 4609	. . 3 ⊢ (𝑀 ∈ ℤ → (ℤ≥‘𝑀) ⊆ ℤ)
4	1	fdmi 6747	. . 3 ⊢ dom ℤ≥ = ℤ
5	3, 4	eleq2s 2859	. 2 ⊢ (𝑀 ∈ dom ℤ≥ → (ℤ≥‘𝑀) ⊆ ℤ)
6		ndmfv 6941	. . 3 ⊢ (¬ 𝑀 ∈ dom ℤ≥ → (ℤ≥‘𝑀) = ∅)
7		0ss 4400	. . 3 ⊢ ∅ ⊆ ℤ
8	6, 7	eqsstrdi 4028	. 2 ⊢ (¬ 𝑀 ∈ dom ℤ≥ → (ℤ≥‘𝑀) ⊆ ℤ)
9	5, 8	pm2.61i 182	1 ⊢ (ℤ≥‘𝑀) ⊆ ℤ

Syntax hints:  ¬ wn 3   ∈ wcel 2108   ⊆ wss 3951  ∅c0 4333  𝒫 cpw 4600  dom cdm 5685  ‘cfv 6561  ℤcz 12613  ℤ_≥cuz 12878

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432  ax-cnex 11211  ax-resscn 11212

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-mpt 5226  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-fv 6569  df-ov 7434  df-neg 11495  df-z 12614  df-uz 12879

This theorem is referenced by:  uzssre  12900  uzwo  12953  uzwo2  12954  infssuzle  12973  infssuzcl  12974  uzsupss  12982  uzwo3  12985  uzsup  13903  cau3  15394  caubnd  15397  limsupgre  15517  rlimclim  15582  climz  15585  climaddc1  15671  climmulc2  15673  climsubc1  15674  climsubc2  15675  climlec2  15695  isercolllem1  15701  isercolllem2  15702  isercoll  15704  caurcvg  15713  caucvg  15715  iseraltlem1  15718  iseraltlem2  15719  iseraltlem3  15720  summolem2a  15751  summolem2  15752  zsum  15754  fsumcvg3  15765  climfsum  15856  divcnvshft  15891  clim2prod  15924  ntrivcvg  15933  ntrivcvgfvn0  15935  ntrivcvgtail  15936  ntrivcvgmullem  15937  ntrivcvgmul  15938  prodrblem  15965  prodmolem2a  15970  prodmolem2  15971  zprod  15973  4sqlem11  16993  gsumval3  19925  lmbrf  23268  lmres  23308  uzrest  23905  uzfbas  23906  lmflf  24013  lmmbrf  25296  iscau4  25313  iscauf  25314  caucfil  25317  lmclimf  25338  mbfsup  25699  mbflimsup  25701  ig1pdvds  26219  ulmval  26423  ulmpm  26426  2sqlem6  27467  ballotlemfc0  34495  ballotlemfcc  34496  ballotlemiex  34504  ballotlemsima  34518  ballotlemrv2  34524  breprexplemc  34647  erdszelem4  35199  erdszelem8  35203  caures  37767  diophin  42783  irrapxlem1  42833  monotuz  42953  hashnzfzclim  44341  uzmptshftfval  44365  uzct  45068  uzfissfz  45337  ssuzfz  45360  uzssre2  45418  uzssz2  45467  uzinico2  45575  fnlimfvre  45689  climleltrp  45691  limsupequzmpt2  45733  limsupequzlem  45737  liminfequzmpt2  45806  ioodvbdlimc1lem2  45947  ioodvbdlimc2lem  45949  sge0isum  46442  smflimlem1  46786  smflimlem2  46787  smflim  46792