Theorem uzssz 12756

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 12738	. . . . 5 ⊢ ℤ≥:ℤ⟶𝒫 ℤ
2	1	ffvelcdmi 7017	. . . 4 ⊢ (𝑀 ∈ ℤ → (ℤ≥‘𝑀) ∈ 𝒫 ℤ)
3	2	elpwid 4560	. . 3 ⊢ (𝑀 ∈ ℤ → (ℤ≥‘𝑀) ⊆ ℤ)
4	1	fdmi 6663	. . 3 ⊢ dom ℤ≥ = ℤ
5	3, 4	eleq2s 2846	. 2 ⊢ (𝑀 ∈ dom ℤ≥ → (ℤ≥‘𝑀) ⊆ ℤ)
6		ndmfv 6855	. . 3 ⊢ (¬ 𝑀 ∈ dom ℤ≥ → (ℤ≥‘𝑀) = ∅)
7		0ss 4351	. . 3 ⊢ ∅ ⊆ ℤ
8	6, 7	eqsstrdi 3980	. 2 ⊢ (¬ 𝑀 ∈ dom ℤ≥ → (ℤ≥‘𝑀) ⊆ ℤ)
9	5, 8	pm2.61i 182	1 ⊢ (ℤ≥‘𝑀) ⊆ ℤ

Syntax hints:  ¬ wn 3   ∈ wcel 2109   ⊆ wss 3903  ∅c0 4284  𝒫 cpw 4551  dom cdm 5619  ‘cfv 6482  ℤcz 12471  ℤ_≥cuz 12735

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 2701  ax-sep 5235  ax-nul 5245  ax-pr 5371  ax-cnex 11065  ax-resscn 11066

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 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3395  df-v 3438  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4285  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-opab 5155  df-mpt 5174  df-id 5514  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-iota 6438  df-fun 6484  df-fn 6485  df-f 6486  df-fv 6490  df-ov 7352  df-neg 11350  df-z 12472  df-uz 12736

This theorem is referenced by:  uzssre  12757  uzwo  12812  uzwo2  12813  infssuzle  12832  infssuzcl  12833  uzsupss  12841  uzwo3  12844  uzsup  13767  cau3  15263  caubnd  15266  limsupgre  15388  rlimclim  15453  climz  15456  climaddc1  15542  climmulc2  15544  climsubc1  15545  climsubc2  15546  climlec2  15566  isercolllem1  15572  isercolllem2  15573  isercoll  15575  caurcvg  15584  caucvg  15586  iseraltlem1  15589  iseraltlem2  15590  iseraltlem3  15591  summolem2a  15622  summolem2  15623  zsum  15625  fsumcvg3  15636  climfsum  15727  divcnvshft  15762  clim2prod  15795  ntrivcvg  15804  ntrivcvgfvn0  15806  ntrivcvgtail  15807  ntrivcvgmullem  15808  ntrivcvgmul  15809  prodrblem  15836  prodmolem2a  15841  prodmolem2  15842  zprod  15844  4sqlem11  16867  gsumval3  19786  lmbrf  23145  lmres  23185  uzrest  23782  uzfbas  23783  lmflf  23890  lmmbrf  25160  iscau4  25177  iscauf  25178  caucfil  25181  lmclimf  25202  mbfsup  25563  mbflimsup  25565  ig1pdvds  26083  ulmval  26287  ulmpm  26290  2sqlem6  27332  ballotlemfc0  34467  ballotlemfcc  34468  ballotlemiex  34476  ballotlemsima  34490  ballotlemrv2  34496  breprexplemc  34606  erdszelem4  35177  erdszelem8  35181  caures  37750  diophin  42755  irrapxlem1  42805  monotuz  42924  hashnzfzclim  44305  uzmptshftfval  44329  uzct  45051  uzfissfz  45316  ssuzfz  45339  uzssre2  45396  uzssz2  45445  uzinico2  45552  fnlimfvre  45665  climleltrp  45667  limsupequzmpt2  45709  limsupequzlem  45713  liminfequzmpt2  45782  ioodvbdlimc1lem2  45923  ioodvbdlimc2lem  45925  sge0isum  46418  smflimlem1  46762  smflimlem2  46763  smflim  46768