Theorem uzssz 12821

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 12803	. . . . 5 ⊢ ℤ≥:ℤ⟶𝒫 ℤ
2	1	ffvelcdmi 7058	. . . 4 ⊢ (𝑀 ∈ ℤ → (ℤ≥‘𝑀) ∈ 𝒫 ℤ)
3	2	elpwid 4575	. . 3 ⊢ (𝑀 ∈ ℤ → (ℤ≥‘𝑀) ⊆ ℤ)
4	1	fdmi 6702	. . 3 ⊢ dom ℤ≥ = ℤ
5	3, 4	eleq2s 2847	. 2 ⊢ (𝑀 ∈ dom ℤ≥ → (ℤ≥‘𝑀) ⊆ ℤ)
6		ndmfv 6896	. . 3 ⊢ (¬ 𝑀 ∈ dom ℤ≥ → (ℤ≥‘𝑀) = ∅)
7		0ss 4366	. . 3 ⊢ ∅ ⊆ ℤ
8	6, 7	eqsstrdi 3994	. 2 ⊢ (¬ 𝑀 ∈ dom ℤ≥ → (ℤ≥‘𝑀) ⊆ ℤ)
9	5, 8	pm2.61i 182	1 ⊢ (ℤ≥‘𝑀) ⊆ ℤ

Syntax hints:  ¬ wn 3   ∈ wcel 2109   ⊆ wss 3917  ∅c0 4299  𝒫 cpw 4566  dom cdm 5641  ‘cfv 6514  ℤcz 12536  ℤ_≥cuz 12800

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 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390  ax-cnex 11131  ax-resscn 11132

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-opab 5173  df-mpt 5192  df-id 5536  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-iota 6467  df-fun 6516  df-fn 6517  df-f 6518  df-fv 6522  df-ov 7393  df-neg 11415  df-z 12537  df-uz 12801

This theorem is referenced by:  uzssre  12822  uzwo  12877  uzwo2  12878  infssuzle  12897  infssuzcl  12898  uzsupss  12906  uzwo3  12909  uzsup  13832  cau3  15329  caubnd  15332  limsupgre  15454  rlimclim  15519  climz  15522  climaddc1  15608  climmulc2  15610  climsubc1  15611  climsubc2  15612  climlec2  15632  isercolllem1  15638  isercolllem2  15639  isercoll  15641  caurcvg  15650  caucvg  15652  iseraltlem1  15655  iseraltlem2  15656  iseraltlem3  15657  summolem2a  15688  summolem2  15689  zsum  15691  fsumcvg3  15702  climfsum  15793  divcnvshft  15828  clim2prod  15861  ntrivcvg  15870  ntrivcvgfvn0  15872  ntrivcvgtail  15873  ntrivcvgmullem  15874  ntrivcvgmul  15875  prodrblem  15902  prodmolem2a  15907  prodmolem2  15908  zprod  15910  4sqlem11  16933  gsumval3  19844  lmbrf  23154  lmres  23194  uzrest  23791  uzfbas  23792  lmflf  23899  lmmbrf  25169  iscau4  25186  iscauf  25187  caucfil  25190  lmclimf  25211  mbfsup  25572  mbflimsup  25574  ig1pdvds  26092  ulmval  26296  ulmpm  26299  2sqlem6  27341  ballotlemfc0  34491  ballotlemfcc  34492  ballotlemiex  34500  ballotlemsima  34514  ballotlemrv2  34520  breprexplemc  34630  erdszelem4  35188  erdszelem8  35192  caures  37761  diophin  42767  irrapxlem1  42817  monotuz  42937  hashnzfzclim  44318  uzmptshftfval  44342  uzct  45064  uzfissfz  45329  ssuzfz  45352  uzssre2  45410  uzssz2  45459  uzinico2  45566  fnlimfvre  45679  climleltrp  45681  limsupequzmpt2  45723  limsupequzlem  45727  liminfequzmpt2  45796  ioodvbdlimc1lem2  45937  ioodvbdlimc2lem  45939  sge0isum  46432  smflimlem1  46776  smflimlem2  46777  smflim  46782