Theorem uzssz 12532

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 12514	. . . . 5 ⊢ ℤ≥:ℤ⟶𝒫 ℤ
2	1	ffvelrni 6942	. . . 4 ⊢ (𝑀 ∈ ℤ → (ℤ≥‘𝑀) ∈ 𝒫 ℤ)
3	2	elpwid 4541	. . 3 ⊢ (𝑀 ∈ ℤ → (ℤ≥‘𝑀) ⊆ ℤ)
4	1	fdmi 6596	. . 3 ⊢ dom ℤ≥ = ℤ
5	3, 4	eleq2s 2857	. 2 ⊢ (𝑀 ∈ dom ℤ≥ → (ℤ≥‘𝑀) ⊆ ℤ)
6		ndmfv 6786	. . 3 ⊢ (¬ 𝑀 ∈ dom ℤ≥ → (ℤ≥‘𝑀) = ∅)
7		0ss 4327	. . 3 ⊢ ∅ ⊆ ℤ
8	6, 7	eqsstrdi 3971	. 2 ⊢ (¬ 𝑀 ∈ dom ℤ≥ → (ℤ≥‘𝑀) ⊆ ℤ)
9	5, 8	pm2.61i 182	1 ⊢ (ℤ≥‘𝑀) ⊆ ℤ

Syntax hints:  ¬ wn 3   ∈ wcel 2108   ⊆ wss 3883  ∅c0 4253  𝒫 cpw 4530  dom cdm 5580  ‘cfv 6418  ℤcz 12249  ℤ_≥cuz 12511

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347  ax-cnex 10858  ax-resscn 10859

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-opab 5133  df-mpt 5154  df-id 5480  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-fv 6426  df-ov 7258  df-neg 11138  df-z 12250  df-uz 12512

This theorem is referenced by:  uzssre  12533  uzwo  12580  uzwo2  12581  infssuzle  12600  infssuzcl  12601  uzsupss  12609  uzwo3  12612  uzsup  13511  cau3  14995  caubnd  14998  limsupgre  15118  rlimclim  15183  climz  15186  climaddc1  15272  climmulc2  15274  climsubc1  15275  climsubc2  15276  climlec2  15298  isercolllem1  15304  isercolllem2  15305  isercoll  15307  caurcvg  15316  caucvg  15318  iseraltlem1  15321  iseraltlem2  15322  iseraltlem3  15323  summolem2a  15355  summolem2  15356  zsum  15358  fsumcvg3  15369  climfsum  15460  divcnvshft  15495  clim2prod  15528  ntrivcvg  15537  ntrivcvgfvn0  15539  ntrivcvgtail  15540  ntrivcvgmullem  15541  ntrivcvgmul  15542  prodrblem  15567  prodmolem2a  15572  prodmolem2  15573  zprod  15575  4sqlem11  16584  gsumval3  19423  lmbrf  22319  lmres  22359  uzrest  22956  uzfbas  22957  lmflf  23064  lmmbrf  24331  iscau4  24348  iscauf  24349  caucfil  24352  lmclimf  24373  mbfsup  24733  mbflimsup  24735  ig1pdvds  25246  ulmval  25444  ulmpm  25447  2sqlem6  26476  ballotlemfc0  32359  ballotlemfcc  32360  ballotlemiex  32368  ballotlemsima  32382  ballotlemrv2  32388  breprexplemc  32512  erdszelem4  33056  erdszelem8  33060  caures  35845  diophin  40510  irrapxlem1  40560  monotuz  40679  hashnzfzclim  41829  uzmptshftfval  41853  uzct  42500  uzfissfz  42755  ssuzfz  42778  uzssre2  42837  uzssz2  42886  uzinico2  42990  fnlimfvre  43105  climleltrp  43107  limsupequzmpt2  43149  limsupequzlem  43153  liminfequzmpt2  43222  ioodvbdlimc1lem2  43363  ioodvbdlimc2lem  43365  sge0isum  43855  smflimlem1  44193  smflimlem2  44194  smflim  44199