Theorem uzssz 12774

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 12756	. . . . 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 12490  ℤ_≥cuz 12753

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 11084  ax-resscn 11085

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 11369  df-z 12491  df-uz 12754

This theorem is referenced by:  uzssre  12775  uzwo  12826  uzwo2  12827  infssuzle  12846  infssuzcl  12847  uzsupss  12855  uzwo3  12858  uzsup  13785  cau3  15281  caubnd  15284  limsupgre  15406  rlimclim  15471  climz  15474  climaddc1  15560  climmulc2  15562  climsubc1  15563  climsubc2  15564  climlec2  15584  isercolllem1  15590  isercolllem2  15591  isercoll  15593  caurcvg  15602  caucvg  15604  iseraltlem1  15607  iseraltlem2  15608  iseraltlem3  15609  summolem2a  15640  summolem2  15641  zsum  15643  fsumcvg3  15654  climfsum  15745  divcnvshft  15780  clim2prod  15813  ntrivcvg  15822  ntrivcvgfvn0  15824  ntrivcvgtail  15825  ntrivcvgmullem  15826  ntrivcvgmul  15827  prodrblem  15854  prodmolem2a  15859  prodmolem2  15860  zprod  15862  4sqlem11  16885  gsumval3  19838  lmbrf  23206  lmres  23246  uzrest  23843  uzfbas  23844  lmflf  23951  lmmbrf  25220  iscau4  25237  iscauf  25238  caucfil  25241  lmclimf  25262  mbfsup  25623  mbflimsup  25625  ig1pdvds  26143  ulmval  26347  ulmpm  26350  2sqlem6  27392  ballotlemfc0  34652  ballotlemfcc  34653  ballotlemiex  34661  ballotlemsima  34675  ballotlemrv2  34681  breprexplemc  34791  erdszelem4  35390  erdszelem8  35394  caures  37963  diophin  43035  irrapxlem1  43085  monotuz  43204  hashnzfzclim  44584  uzmptshftfval  44608  uzct  45329  uzfissfz  45592  ssuzfz  45615  uzssre2  45672  uzssz2  45721  uzinico2  45828  fnlimfvre  45939  climleltrp  45941  limsupequzmpt2  45983  limsupequzlem  45987  liminfequzmpt2  46056  ioodvbdlimc1lem2  46197  ioodvbdlimc2lem  46199  sge0isum  46692  smflimlem1  47036  smflimlem2  47037  smflim  47042