Theorem uzssz 12784

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 12766	. . . . 5 ⊢ ℤ≥:ℤ⟶𝒫 ℤ
2	1	ffvelcdmi 7037	. . . 4 ⊢ (𝑀 ∈ ℤ → (ℤ≥‘𝑀) ∈ 𝒫 ℤ)
3	2	elpwid 4565	. . 3 ⊢ (𝑀 ∈ ℤ → (ℤ≥‘𝑀) ⊆ ℤ)
4	1	fdmi 6681	. . 3 ⊢ dom ℤ≥ = ℤ
5	3, 4	eleq2s 2855	. 2 ⊢ (𝑀 ∈ dom ℤ≥ → (ℤ≥‘𝑀) ⊆ ℤ)
6		ndmfv 6874	. . 3 ⊢ (¬ 𝑀 ∈ dom ℤ≥ → (ℤ≥‘𝑀) = ∅)
7		0ss 4354	. . 3 ⊢ ∅ ⊆ ℤ
8	6, 7	eqsstrdi 3980	. 2 ⊢ (¬ 𝑀 ∈ dom ℤ≥ → (ℤ≥‘𝑀) ⊆ ℤ)
9	5, 8	pm2.61i 182	1 ⊢ (ℤ≥‘𝑀) ⊆ ℤ

Syntax hints:  ¬ wn 3   ∈ wcel 2114   ⊆ wss 3903  ∅c0 4287  𝒫 cpw 4556  dom cdm 5632  ‘cfv 6500  ℤcz 12500  ℤ_≥cuz 12763

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5243  ax-nul 5253  ax-pr 5379  ax-cnex 11094  ax-resscn 11095

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5527  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-iota 6456  df-fun 6502  df-fn 6503  df-f 6504  df-fv 6508  df-ov 7371  df-neg 11379  df-z 12501  df-uz 12764

This theorem is referenced by:  uzssre  12785  uzwo  12836  uzwo2  12837  infssuzle  12856  infssuzcl  12857  uzsupss  12865  uzwo3  12868  uzsup  13795  cau3  15291  caubnd  15294  limsupgre  15416  rlimclim  15481  climz  15484  climaddc1  15570  climmulc2  15572  climsubc1  15573  climsubc2  15574  climlec2  15594  isercolllem1  15600  isercolllem2  15601  isercoll  15603  caurcvg  15612  caucvg  15614  iseraltlem1  15617  iseraltlem2  15618  iseraltlem3  15619  summolem2a  15650  summolem2  15651  zsum  15653  fsumcvg3  15664  climfsum  15755  divcnvshft  15790  clim2prod  15823  ntrivcvg  15832  ntrivcvgfvn0  15834  ntrivcvgtail  15835  ntrivcvgmullem  15836  ntrivcvgmul  15837  prodrblem  15864  prodmolem2a  15869  prodmolem2  15870  zprod  15872  4sqlem11  16895  gsumval3  19851  lmbrf  23219  lmres  23259  uzrest  23856  uzfbas  23857  lmflf  23964  lmmbrf  25233  iscau4  25250  iscauf  25251  caucfil  25254  lmclimf  25275  mbfsup  25636  mbflimsup  25638  ig1pdvds  26156  ulmval  26360  ulmpm  26363  2sqlem6  27405  ballotlemfc0  34675  ballotlemfcc  34676  ballotlemiex  34684  ballotlemsima  34698  ballotlemrv2  34704  breprexplemc  34814  erdszelem4  35414  erdszelem8  35418  caures  38015  diophin  43133  irrapxlem1  43183  monotuz  43302  hashnzfzclim  44682  uzmptshftfval  44706  uzct  45427  uzfissfz  45689  ssuzfz  45712  uzssre2  45769  uzssz2  45818  uzinico2  45925  fnlimfvre  46036  climleltrp  46038  limsupequzmpt2  46080  limsupequzlem  46084  liminfequzmpt2  46153  ioodvbdlimc1lem2  46294  ioodvbdlimc2lem  46296  sge0isum  46789  smflimlem1  47133  smflimlem2  47134  smflim  47139