Theorem uzssz 12770

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 12752	. . . . 5 ⊢ ℤ≥:ℤ⟶𝒫 ℤ
2	1	ffvelcdmi 7026	. . . 4 ⊢ (𝑀 ∈ ℤ → (ℤ≥‘𝑀) ∈ 𝒫 ℤ)
3	2	elpwid 4561	. . 3 ⊢ (𝑀 ∈ ℤ → (ℤ≥‘𝑀) ⊆ ℤ)
4	1	fdmi 6671	. . 3 ⊢ dom ℤ≥ = ℤ
5	3, 4	eleq2s 2852	. 2 ⊢ (𝑀 ∈ dom ℤ≥ → (ℤ≥‘𝑀) ⊆ ℤ)
6		ndmfv 6864	. . 3 ⊢ (¬ 𝑀 ∈ dom ℤ≥ → (ℤ≥‘𝑀) = ∅)
7		0ss 4350	. . 3 ⊢ ∅ ⊆ ℤ
8	6, 7	eqsstrdi 3976	. 2 ⊢ (¬ 𝑀 ∈ dom ℤ≥ → (ℤ≥‘𝑀) ⊆ ℤ)
9	5, 8	pm2.61i 182	1 ⊢ (ℤ≥‘𝑀) ⊆ ℤ

Syntax hints:  ¬ wn 3   ∈ wcel 2113   ⊆ wss 3899  ∅c0 4283  𝒫 cpw 4552  dom cdm 5622  ‘cfv 6490  ℤcz 12486  ℤ_≥cuz 12749

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2706  ax-sep 5239  ax-nul 5249  ax-pr 5375  ax-cnex 11080  ax-resscn 11081

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2809  df-nfc 2883  df-ne 2931  df-ral 3050  df-rex 3059  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4862  df-br 5097  df-opab 5159  df-mpt 5178  df-id 5517  df-xp 5628  df-rel 5629  df-cnv 5630  df-co 5631  df-dm 5632  df-rn 5633  df-res 5634  df-ima 5635  df-iota 6446  df-fun 6492  df-fn 6493  df-f 6494  df-fv 6498  df-ov 7359  df-neg 11365  df-z 12487  df-uz 12750

This theorem is referenced by:  uzssre  12771  uzwo  12822  uzwo2  12823  infssuzle  12842  infssuzcl  12843  uzsupss  12851  uzwo3  12854  uzsup  13781  cau3  15277  caubnd  15280  limsupgre  15402  rlimclim  15467  climz  15470  climaddc1  15556  climmulc2  15558  climsubc1  15559  climsubc2  15560  climlec2  15580  isercolllem1  15586  isercolllem2  15587  isercoll  15589  caurcvg  15598  caucvg  15600  iseraltlem1  15603  iseraltlem2  15604  iseraltlem3  15605  summolem2a  15636  summolem2  15637  zsum  15639  fsumcvg3  15650  climfsum  15741  divcnvshft  15776  clim2prod  15809  ntrivcvg  15818  ntrivcvgfvn0  15820  ntrivcvgtail  15821  ntrivcvgmullem  15822  ntrivcvgmul  15823  prodrblem  15850  prodmolem2a  15855  prodmolem2  15856  zprod  15858  4sqlem11  16881  gsumval3  19834  lmbrf  23202  lmres  23242  uzrest  23839  uzfbas  23840  lmflf  23947  lmmbrf  25216  iscau4  25233  iscauf  25234  caucfil  25237  lmclimf  25258  mbfsup  25619  mbflimsup  25621  ig1pdvds  26139  ulmval  26343  ulmpm  26346  2sqlem6  27388  ballotlemfc0  34599  ballotlemfcc  34600  ballotlemiex  34608  ballotlemsima  34622  ballotlemrv2  34628  breprexplemc  34738  erdszelem4  35337  erdszelem8  35341  caures  37900  diophin  42956  irrapxlem1  43006  monotuz  43125  hashnzfzclim  44505  uzmptshftfval  44529  uzct  45250  uzfissfz  45513  ssuzfz  45536  uzssre2  45593  uzssz2  45642  uzinico2  45749  fnlimfvre  45860  climleltrp  45862  limsupequzmpt2  45904  limsupequzlem  45908  liminfequzmpt2  45977  ioodvbdlimc1lem2  46118  ioodvbdlimc2lem  46120  sge0isum  46613  smflimlem1  46957  smflimlem2  46958  smflim  46963