Theorem uzssz 12772

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 12754	. . . . 5 ⊢ ℤ≥:ℤ⟶𝒫 ℤ
2	1	ffvelcdmi 7028	. . . 4 ⊢ (𝑀 ∈ ℤ → (ℤ≥‘𝑀) ∈ 𝒫 ℤ)
3	2	elpwid 4563	. . 3 ⊢ (𝑀 ∈ ℤ → (ℤ≥‘𝑀) ⊆ ℤ)
4	1	fdmi 6673	. . 3 ⊢ dom ℤ≥ = ℤ
5	3, 4	eleq2s 2854	. 2 ⊢ (𝑀 ∈ dom ℤ≥ → (ℤ≥‘𝑀) ⊆ ℤ)
6		ndmfv 6866	. . 3 ⊢ (¬ 𝑀 ∈ dom ℤ≥ → (ℤ≥‘𝑀) = ∅)
7		0ss 4352	. . 3 ⊢ ∅ ⊆ ℤ
8	6, 7	eqsstrdi 3978	. 2 ⊢ (¬ 𝑀 ∈ dom ℤ≥ → (ℤ≥‘𝑀) ⊆ ℤ)
9	5, 8	pm2.61i 182	1 ⊢ (ℤ≥‘𝑀) ⊆ ℤ

Syntax hints:  ¬ wn 3   ∈ wcel 2113   ⊆ wss 3901  ∅c0 4285  𝒫 cpw 4554  dom cdm 5624  ‘cfv 6492  ℤcz 12488  ℤ_≥cuz 12751

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 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377  ax-cnex 11082  ax-resscn 11083

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 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-opab 5161  df-mpt 5180  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-fv 6500  df-ov 7361  df-neg 11367  df-z 12489  df-uz 12752

This theorem is referenced by:  uzssre  12773  uzwo  12824  uzwo2  12825  infssuzle  12844  infssuzcl  12845  uzsupss  12853  uzwo3  12856  uzsup  13783  cau3  15279  caubnd  15282  limsupgre  15404  rlimclim  15469  climz  15472  climaddc1  15558  climmulc2  15560  climsubc1  15561  climsubc2  15562  climlec2  15582  isercolllem1  15588  isercolllem2  15589  isercoll  15591  caurcvg  15600  caucvg  15602  iseraltlem1  15605  iseraltlem2  15606  iseraltlem3  15607  summolem2a  15638  summolem2  15639  zsum  15641  fsumcvg3  15652  climfsum  15743  divcnvshft  15778  clim2prod  15811  ntrivcvg  15820  ntrivcvgfvn0  15822  ntrivcvgtail  15823  ntrivcvgmullem  15824  ntrivcvgmul  15825  prodrblem  15852  prodmolem2a  15857  prodmolem2  15858  zprod  15860  4sqlem11  16883  gsumval3  19836  lmbrf  23204  lmres  23244  uzrest  23841  uzfbas  23842  lmflf  23949  lmmbrf  25218  iscau4  25235  iscauf  25236  caucfil  25239  lmclimf  25260  mbfsup  25621  mbflimsup  25623  ig1pdvds  26141  ulmval  26345  ulmpm  26348  2sqlem6  27390  ballotlemfc0  34650  ballotlemfcc  34651  ballotlemiex  34659  ballotlemsima  34673  ballotlemrv2  34679  breprexplemc  34789  erdszelem4  35388  erdszelem8  35392  caures  37961  diophin  43014  irrapxlem1  43064  monotuz  43183  hashnzfzclim  44563  uzmptshftfval  44587  uzct  45308  uzfissfz  45571  ssuzfz  45594  uzssre2  45651  uzssz2  45700  uzinico2  45807  fnlimfvre  45918  climleltrp  45920  limsupequzmpt2  45962  limsupequzlem  45966  liminfequzmpt2  46035  ioodvbdlimc1lem2  46176  ioodvbdlimc2lem  46178  sge0isum  46671  smflimlem1  47015  smflimlem2  47016  smflim  47021