Theorem uzssz 12081

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 12064	. . . . 5 ⊢ ℤ≥:ℤ⟶𝒫 ℤ
2	1	ffvelrni 6677	. . . 4 ⊢ (𝑀 ∈ ℤ → (ℤ≥‘𝑀) ∈ 𝒫 ℤ)
3	2	elpwid 4435	. . 3 ⊢ (𝑀 ∈ ℤ → (ℤ≥‘𝑀) ⊆ ℤ)
4	1	fdmi 6356	. . 3 ⊢ dom ℤ≥ = ℤ
5	3, 4	eleq2s 2884	. 2 ⊢ (𝑀 ∈ dom ℤ≥ → (ℤ≥‘𝑀) ⊆ ℤ)
6		ndmfv 6531	. . 3 ⊢ (¬ 𝑀 ∈ dom ℤ≥ → (ℤ≥‘𝑀) = ∅)
7		0ss 4237	. . 3 ⊢ ∅ ⊆ ℤ
8	6, 7	syl6eqss 3913	. 2 ⊢ (¬ 𝑀 ∈ dom ℤ≥ → (ℤ≥‘𝑀) ⊆ ℤ)
9	5, 8	pm2.61i 177	1 ⊢ (ℤ≥‘𝑀) ⊆ ℤ

Syntax hints:  ¬ wn 3   ∈ wcel 2050   ⊆ wss 3831  ∅c0 4180  𝒫 cpw 4423  dom cdm 5408  ‘cfv 6190  ℤcz 11796  ℤ_≥cuz 12061

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-13 2301  ax-ext 2750  ax-sep 5061  ax-nul 5068  ax-pow 5120  ax-pr 5187  ax-cnex 10393  ax-resscn 10394

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3or 1069  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-mo 2547  df-eu 2583  df-clab 2759  df-cleq 2771  df-clel 2846  df-nfc 2918  df-ne 2968  df-ral 3093  df-rex 3094  df-rab 3097  df-v 3417  df-sbc 3684  df-dif 3834  df-un 3836  df-in 3838  df-ss 3845  df-nul 4181  df-if 4352  df-pw 4425  df-sn 4443  df-pr 4445  df-op 4449  df-uni 4714  df-br 4931  df-opab 4993  df-mpt 5010  df-id 5313  df-xp 5414  df-rel 5415  df-cnv 5416  df-co 5417  df-dm 5418  df-rn 5419  df-res 5420  df-ima 5421  df-iota 6154  df-fun 6192  df-fn 6193  df-f 6194  df-fv 6198  df-ov 6981  df-neg 10675  df-z 11797  df-uz 12062

This theorem is referenced by:  uzwo  12128  uzwo2  12129  infssuzle  12148  infssuzcl  12149  uzsupss  12157  uzwo3  12160  uzsup  13049  cau3  14579  caubnd  14582  limsupgre  14702  rlimclim  14767  climz  14770  climaddc1  14855  climmulc2  14857  climsubc1  14858  climsubc2  14859  climlec2  14879  isercolllem1  14885  isercolllem2  14886  isercoll  14888  caurcvg  14897  caucvg  14899  iseraltlem1  14902  iseraltlem2  14903  iseraltlem3  14904  summolem2a  14935  summolem2  14936  zsum  14938  fsumcvg3  14949  climfsum  15038  divcnvshft  15073  clim2prod  15107  ntrivcvg  15116  ntrivcvgfvn0  15118  ntrivcvgtail  15119  ntrivcvgmullem  15120  ntrivcvgmul  15121  prodrblem  15146  prodmolem2a  15151  prodmolem2  15152  zprod  15154  4sqlem11  16150  gsumval3  18784  lmbrf  21575  lmres  21615  uzrest  22212  uzfbas  22213  lmflf  22320  lmmbrf  23571  iscau4  23588  iscauf  23589  caucfil  23592  lmclimf  23613  mbfsup  23971  mbflimsup  23973  ig1pdvds  24476  ulmval  24674  ulmpm  24677  2sqlem6  25704  ballotlemfc0  31396  ballotlemfcc  31397  ballotlemiex  31405  ballotlemsdom  31415  ballotlemsima  31419  ballotlemrv2  31425  breprexplemc  31551  erdszelem4  32026  erdszelem8  32030  caures  34477  diophin  38765  irrapxlem1  38815  monotuz  38934  hashnzfzclim  40070  uzmptshftfval  40094  uzct  40745  uzfissfz  41024  ssuzfz  41047  uzssre  41100  uzssre2  41112  uzssz2  41164  uzinico2  41270  fnlimfvre  41387  climleltrp  41389  limsupequzmpt2  41431  limsupequzlem  41435  liminfequzmpt2  41504  ioodvbdlimc1lem2  41648  ioodvbdlimc2lem  41650  sge0isum  42141  smflimlem1  42479  smflimlem2  42480  smflim  42485