Theorem uzssz 12800

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 12782	. . . . 5 ⊢ ℤ≥:ℤ⟶𝒫 ℤ
2	1	ffvelcdmi 7024	. . . 4 ⊢ (𝑀 ∈ ℤ → (ℤ≥‘𝑀) ∈ 𝒫 ℤ)
3	2	elpwid 4538	. . 3 ⊢ (𝑀 ∈ ℤ → (ℤ≥‘𝑀) ⊆ ℤ)
4	1	fdmi 6666	. . 3 ⊢ dom ℤ≥ = ℤ
5	3, 4	eleq2s 2857	. 2 ⊢ (𝑀 ∈ dom ℤ≥ → (ℤ≥‘𝑀) ⊆ ℤ)
6		ndmfv 6859	. . 3 ⊢ (¬ 𝑀 ∈ dom ℤ≥ → (ℤ≥‘𝑀) = ∅)
7		0ss 4328	. . 3 ⊢ ∅ ⊆ ℤ
8	6, 7	eqsstrdi 3959	. 2 ⊢ (¬ 𝑀 ∈ dom ℤ≥ → (ℤ≥‘𝑀) ⊆ ℤ)
9	5, 8	pm2.61i 183	1 ⊢ (ℤ≥‘𝑀) ⊆ ℤ

Syntax hints:  ¬ wn 3   ∈ wcel 2119   ⊆ wss 3883  ∅c0 4261  𝒫 cpw 4529  dom cdm 5618  ‘cfv 6485  ℤcz 12515  ℤ_≥cuz 12779

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-sep 5218  ax-nul 5228  ax-pr 5362  ax-cnex 11085  ax-resscn 11086

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ne 2935  df-ral 3054  df-rex 3064  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4262  df-if 4455  df-pw 4531  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-br 5073  df-opab 5135  df-mpt 5154  df-id 5513  df-xp 5624  df-rel 5625  df-cnv 5626  df-co 5627  df-dm 5628  df-rn 5629  df-res 5630  df-ima 5631  df-iota 6441  df-fun 6487  df-fn 6488  df-f 6489  df-fv 6493  df-ov 7359  df-neg 11371  df-z 12516  df-uz 12780

This theorem is referenced by:  uzssre  12801  uzwo  12852  uzwo2  12853  infssuzle  12872  infssuzcl  12873  uzsupss  12881  uzwo3  12884  uzsup  13813  cau3  15309  caubnd  15312  limsupgre  15434  rlimclim  15499  climz  15502  climaddc1  15588  climmulc2  15590  climsubc1  15591  climsubc2  15592  climlec2  15612  isercolllem1  15618  isercolllem2  15619  isercoll  15621  caurcvg  15630  caucvg  15632  iseraltlem1  15635  iseraltlem2  15636  iseraltlem3  15637  summolem2a  15668  summolem2  15669  zsum  15671  fsumcvg3  15682  climfsum  15774  divcnvshft  15811  clim2prod  15844  ntrivcvg  15853  ntrivcvgfvn0  15855  ntrivcvgtail  15856  ntrivcvgmullem  15857  ntrivcvgmul  15858  prodrblem  15885  prodmolem2a  15890  prodmolem2  15891  zprod  15893  4sqlem11  16917  gsumval3  19873  lmbrf  23243  lmres  23283  uzrest  23880  uzfbas  23881  lmflf  23988  lmmbrf  25247  iscau4  25264  iscauf  25265  caucfil  25268  lmclimf  25289  mbfsup  25649  mbflimsup  25651  ig1pdvds  26163  ulmval  26363  ulmpm  26366  2sqlem6  27404  ballotlemfc0  34677  ballotlemfcc  34678  ballotlemiex  34686  ballotlemsima  34700  ballotlemrv2  34706  breprexplemc  34816  erdszelem4  35422  erdszelem8  35426  caures  38127  diophin  43221  irrapxlem1  43267  monotuz  43386  hashnzfzclim  44766  uzmptshftfval  44790  uzct  45511  uzfissfz  45771  ssuzfz  45794  uzssre2  45850  uzssz2  45899  uzinico2  46006  fnlimfvre  46117  climleltrp  46119  limsupequzmpt2  46161  limsupequzlem  46165  liminfequzmpt2  46234  ioodvbdlimc1lem2  46375  ioodvbdlimc2lem  46377  sge0isum  46870  smflimlem1  47214  smflimlem2  47215  smflim  47220