Theorem uzssz 12843

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 12825	. . . . 5 ⊢ ℤ≥:ℤ⟶𝒫 ℤ
2	1	ffvelcdmi 7086	. . . 4 ⊢ (𝑀 ∈ ℤ → (ℤ≥‘𝑀) ∈ 𝒫 ℤ)
3	2	elpwid 4612	. . 3 ⊢ (𝑀 ∈ ℤ → (ℤ≥‘𝑀) ⊆ ℤ)
4	1	fdmi 6730	. . 3 ⊢ dom ℤ≥ = ℤ
5	3, 4	eleq2s 2852	. 2 ⊢ (𝑀 ∈ dom ℤ≥ → (ℤ≥‘𝑀) ⊆ ℤ)
6		ndmfv 6927	. . 3 ⊢ (¬ 𝑀 ∈ dom ℤ≥ → (ℤ≥‘𝑀) = ∅)
7		0ss 4397	. . 3 ⊢ ∅ ⊆ ℤ
8	6, 7	eqsstrdi 4037	. 2 ⊢ (¬ 𝑀 ∈ dom ℤ≥ → (ℤ≥‘𝑀) ⊆ ℤ)
9	5, 8	pm2.61i 182	1 ⊢ (ℤ≥‘𝑀) ⊆ ℤ

Syntax hints:  ¬ wn 3   ∈ wcel 2107   ⊆ wss 3949  ∅c0 4323  𝒫 cpw 4603  dom cdm 5677  ‘cfv 6544  ℤcz 12558  ℤ_≥cuz 12822

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pr 5428  ax-cnex 11166  ax-resscn 11167

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-opab 5212  df-mpt 5233  df-id 5575  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-fv 6552  df-ov 7412  df-neg 11447  df-z 12559  df-uz 12823

This theorem is referenced by:  uzssre  12844  uzwo  12895  uzwo2  12896  infssuzle  12915  infssuzcl  12916  uzsupss  12924  uzwo3  12927  uzsup  13828  cau3  15302  caubnd  15305  limsupgre  15425  rlimclim  15490  climz  15493  climaddc1  15579  climmulc2  15581  climsubc1  15582  climsubc2  15583  climlec2  15605  isercolllem1  15611  isercolllem2  15612  isercoll  15614  caurcvg  15623  caucvg  15625  iseraltlem1  15628  iseraltlem2  15629  iseraltlem3  15630  summolem2a  15661  summolem2  15662  zsum  15664  fsumcvg3  15675  climfsum  15766  divcnvshft  15801  clim2prod  15834  ntrivcvg  15843  ntrivcvgfvn0  15845  ntrivcvgtail  15846  ntrivcvgmullem  15847  ntrivcvgmul  15848  prodrblem  15873  prodmolem2a  15878  prodmolem2  15879  zprod  15881  4sqlem11  16888  gsumval3  19775  lmbrf  22764  lmres  22804  uzrest  23401  uzfbas  23402  lmflf  23509  lmmbrf  24779  iscau4  24796  iscauf  24797  caucfil  24800  lmclimf  24821  mbfsup  25181  mbflimsup  25183  ig1pdvds  25694  ulmval  25892  ulmpm  25895  2sqlem6  26926  ballotlemfc0  33491  ballotlemfcc  33492  ballotlemiex  33500  ballotlemsima  33514  ballotlemrv2  33520  breprexplemc  33644  erdszelem4  34185  erdszelem8  34189  caures  36628  diophin  41510  irrapxlem1  41560  monotuz  41680  hashnzfzclim  43081  uzmptshftfval  43105  uzct  43750  uzfissfz  44036  ssuzfz  44059  uzssre2  44117  uzssz2  44166  uzinico2  44275  fnlimfvre  44390  climleltrp  44392  limsupequzmpt2  44434  limsupequzlem  44438  liminfequzmpt2  44507  ioodvbdlimc1lem2  44648  ioodvbdlimc2lem  44650  sge0isum  45143  smflimlem1  45487  smflimlem2  45488  smflim  45493