Theorem uzssz 12883

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 12865	. . . . 5 ⊢ ℤ≥:ℤ⟶𝒫 ℤ
2	1	ffvelcdmi 7079	. . . 4 ⊢ (𝑀 ∈ ℤ → (ℤ≥‘𝑀) ∈ 𝒫 ℤ)
3	2	elpwid 4576	. . 3 ⊢ (𝑀 ∈ ℤ → (ℤ≥‘𝑀) ⊆ ℤ)
4	1	fdmi 6718	. . 3 ⊢ dom ℤ≥ = ℤ
5	3, 4	eleq2s 2887	. 2 ⊢ (𝑀 ∈ dom ℤ≥ → (ℤ≥‘𝑀) ⊆ ℤ)
6		ndmfv 6914	. . 3 ⊢ (¬ 𝑀 ∈ dom ℤ≥ → (ℤ≥‘𝑀) = ∅)
7		0ss 4364	. . 3 ⊢ ∅ ⊆ ℤ
8	6, 7	eqsstrdi 3989	. 2 ⊢ (¬ 𝑀 ∈ dom ℤ≥ → (ℤ≥‘𝑀) ⊆ ℤ)
9	5, 8	pm2.61i 184	1 ⊢ (ℤ≥‘𝑀) ⊆ ℤ

Syntax hints:  ¬ wn 3   ∈ wcel 2149   ⊆ wss 3913  ∅c0 4294  𝒫 cpw 4567  dom cdm 5662  ‘cfv 6537  ℤcz 12591  ℤ_≥cuz 12862

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5261  ax-nul 5271  ax-pr 5405  ax-cnex 11156  ax-resscn 11157

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-ral 3086  df-rex 3096  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-br 5114  df-opab 5178  df-mpt 5197  df-id 5557  df-xp 5668  df-rel 5669  df-cnv 5670  df-co 5671  df-dm 5672  df-rn 5673  df-res 5674  df-ima 5675  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-fv 6545  df-ov 7414  df-neg 11444  df-z 12592  df-uz 12863

This theorem is referenced by:  uzssre  12884  uzwo  12935  uzwo2  12936  infssuzle  12955  infssuzcl  12956  uzsupss  12964  uzwo3  12967  uzsup  13896  cau3  15407  caubnd  15410  limsupgre  15532  rlimclim  15597  climz  15600  climaddc1  15686  climmulc2  15688  climsubc1  15689  climsubc2  15690  climlec2  15710  isercolllem1  15716  isercolllem2  15717  isercoll  15719  caurcvg  15728  caucvg  15730  iseraltlem1  15733  iseraltlem2  15734  iseraltlem3  15735  summolem2a  15766  summolem2  15767  zsum  15769  fsumcvg3  15780  climfsum  15872  divcnvshft  15909  clim2prod  15942  ntrivcvg  15951  ntrivcvgfvn0  15953  ntrivcvgtail  15954  ntrivcvgmullem  15955  ntrivcvgmul  15956  prodrblem  15983  prodmolem2a  15988  prodmolem2  15989  zprod  15991  4sqlem11  17015  gsumval3  19977  lmbrf  23386  lmres  23426  uzrest  24023  uzfbas  24024  lmflf  24131  lmmbrf  25390  iscau4  25407  iscauf  25408  caucfil  25411  lmclimf  25432  mbfsup  25792  mbflimsup  25794  ig1pdvds  26306  ulmval  26509  ulmpm  26512  2sqlem6  27553  ballotlemfc0  34828  ballotlemfcc  34829  ballotlemiex  34837  ballotlemsima  34851  ballotlemrv2  34857  breprexplemc  34964  erdszelem4  35619  erdszelem8  35623  caures  38333  diophin  43429  irrapxlem1  43475  monotuz  43594  hashnzfzclim  44958  uzmptshftfval  44982  uzct  45709  uzfissfz  45968  ssuzfz  45991  uzssre2  46047  uzssz2  46096  uzinico2  46203  fnlimfvre  46314  climleltrp  46316  limsupequzmpt2  46358  limsupequzlem  46362  liminfequzmpt2  46431  ioodvbdlimc1lem2  46572  ioodvbdlimc2lem  46574  sge0isum  47067  smflimlem1  47411  smflimlem2  47412  smflim  47417