Theorem uzssz 12986

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 12968	. . . . 5 ⊢ ℤ≥:ℤ⟶𝒫 ℤ
2	1	ffvelcdmi 7083	. . . 4 ⊢ (𝑀 ∈ ℤ → (ℤ≥‘𝑀) ∈ 𝒫 ℤ)
3	2	elpwid 4566	. . 3 ⊢ (𝑀 ∈ ℤ → (ℤ≥‘𝑀) ⊆ ℤ)
4	1	fdmi 6721	. . 3 ⊢ dom ℤ≥ = ℤ
5	3, 4	eleq2s 2879	. 2 ⊢ (𝑀 ∈ dom ℤ≥ → (ℤ≥‘𝑀) ⊆ ℤ)
6		ndmfv 6917	. . 3 ⊢ (¬ 𝑀 ∈ dom ℤ≥ → (ℤ≥‘𝑀) = ∅)
7		0ss 4350	. . 3 ⊢ ∅ ⊆ ℤ
8	6, 7	eqsstrdi 3975	. 2 ⊢ (¬ 𝑀 ∈ dom ℤ≥ → (ℤ≥‘𝑀) ⊆ ℤ)
9	5, 8	pm2.61i 184	1 ⊢ (ℤ≥‘𝑀) ⊆ ℤ

This proof depends on syntax axioms:  ¬ wn 3   ∈ wcel 2145   ⊆ wss 3899  ∅c0 4279  𝒫 cpw 4557  dom cdm 5651  ‘cfv 6538  ℤcz 12693  ℤ_≥cuz 12965

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pr 5391  ax-cnex 11256  ax-resscn 11257

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-fv 6546  df-ov 7423  df-neg 11544  df-z 12694  df-uz 12966

This theorem is used by:  uzssre  12987  uzwo  13038  uzwo2  13039  infssuzle  13058  infssuzcl  13059  uzsupss  13067  uzwo3  13070  uzsup  14003  cau3  15523  caubnd  15526  limsupgre  15648  rlimclim  15713  climz  15716  climaddc1  15802  climmulc2  15804  climsubc1  15805  climsubc2  15806  climlec2  15826  isercolllem1  15832  isercolllem2  15833  isercoll  15835  caurcvg  15844  caucvg  15846  iseraltlem1  15849  iseraltlem2  15850  iseraltlem3  15851  summolem2a  15881  summolem2  15882  zsum  15884  fsumcvg3  15895  climfsum  15987  divcnvshft  16024  clim2prod  16057  ntrivcvg  16066  ntrivcvgfvn0  16068  ntrivcvgtail  16069  ntrivcvgmullem  16070  ntrivcvgmul  16071  prodrblem  16096  prodmolem2a  16101  prodmolem2  16102  zprod  16104  4sqlem11  17133  gsumval3  20121  lmbrf  23578  lmres  23618  uzrest  24216  uzfbas  24217  lmflf  24324  lmmbrf  25583  iscau4  25600  iscauf  25601  caucfil  25604  lmclimf  25625  mbfsup  25985  mbflimsup  25987  ig1pdvds  26498  ulmval  26707  ulmpm  26710  2sqlem6  27750  ballotlemfc0  35125  ballotlemfcc  35126  ballotlemiex  35134  ballotlemsima  35148  ballotlemrv2  35154  breprexplemc  35261  erdszelem4  35959  erdszelem8  35963  caures  38694  diophin  43782  irrapxlem1  43828  monotuz  43947  hashnzfzclim  45305  uzmptshftfval  45329  uzct  46079  uzfissfz  46337  ssuzfz  46360  uzssre2  46416  uzssz2  46465  uzinico2  46572  fnlimfvre  46683  climleltrp  46685  limsupequzmpt2  46727  limsupequzlem  46731  liminfequzmpt2  46800  ioodvbdlimc1lem2  46941  ioodvbdlimc2lem  46943  sge0isum  47436  smflimlem1  47780  smflimlem2  47781  smflim  47786