Theorem uzssz 12682

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 12664	. . . . 5 ⊢ ℤ≥:ℤ⟶𝒫 ℤ
2	1	ffvelcdmi 6999	. . . 4 ⊢ (𝑀 ∈ ℤ → (ℤ≥‘𝑀) ∈ 𝒫 ℤ)
3	2	elpwid 4553	. . 3 ⊢ (𝑀 ∈ ℤ → (ℤ≥‘𝑀) ⊆ ℤ)
4	1	fdmi 6649	. . 3 ⊢ dom ℤ≥ = ℤ
5	3, 4	eleq2s 2855	. 2 ⊢ (𝑀 ∈ dom ℤ≥ → (ℤ≥‘𝑀) ⊆ ℤ)
6		ndmfv 6843	. . 3 ⊢ (¬ 𝑀 ∈ dom ℤ≥ → (ℤ≥‘𝑀) = ∅)
7		0ss 4340	. . 3 ⊢ ∅ ⊆ ℤ
8	6, 7	eqsstrdi 3984	. 2 ⊢ (¬ 𝑀 ∈ dom ℤ≥ → (ℤ≥‘𝑀) ⊆ ℤ)
9	5, 8	pm2.61i 182	1 ⊢ (ℤ≥‘𝑀) ⊆ ℤ

Syntax hints:  ¬ wn 3   ∈ wcel 2105   ⊆ wss 3896  ∅c0 4266  𝒫 cpw 4544  dom cdm 5607  ‘cfv 6465  ℤcz 12398  ℤ_≥cuz 12661

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 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2707  ax-sep 5237  ax-nul 5244  ax-pr 5366  ax-cnex 11006  ax-resscn 11007

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2886  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3404  df-v 3442  df-dif 3899  df-un 3901  df-in 3903  df-ss 3913  df-nul 4267  df-if 4471  df-pw 4546  df-sn 4571  df-pr 4573  df-op 4577  df-uni 4850  df-br 5087  df-opab 5149  df-mpt 5170  df-id 5506  df-xp 5613  df-rel 5614  df-cnv 5615  df-co 5616  df-dm 5617  df-rn 5618  df-res 5619  df-ima 5620  df-iota 6417  df-fun 6467  df-fn 6468  df-f 6469  df-fv 6473  df-ov 7319  df-neg 11287  df-z 12399  df-uz 12662

This theorem is referenced by:  uzssre  12683  uzwo  12730  uzwo2  12731  infssuzle  12750  infssuzcl  12751  uzsupss  12759  uzwo3  12762  uzsup  13662  cau3  15143  caubnd  15146  limsupgre  15266  rlimclim  15331  climz  15334  climaddc1  15420  climmulc2  15422  climsubc1  15423  climsubc2  15424  climlec2  15446  isercolllem1  15452  isercolllem2  15453  isercoll  15455  caurcvg  15464  caucvg  15466  iseraltlem1  15469  iseraltlem2  15470  iseraltlem3  15471  summolem2a  15503  summolem2  15504  zsum  15506  fsumcvg3  15517  climfsum  15608  divcnvshft  15643  clim2prod  15676  ntrivcvg  15685  ntrivcvgfvn0  15687  ntrivcvgtail  15688  ntrivcvgmullem  15689  ntrivcvgmul  15690  prodrblem  15715  prodmolem2a  15720  prodmolem2  15721  zprod  15723  4sqlem11  16730  gsumval3  19580  lmbrf  22491  lmres  22531  uzrest  23128  uzfbas  23129  lmflf  23236  lmmbrf  24506  iscau4  24523  iscauf  24524  caucfil  24527  lmclimf  24548  mbfsup  24908  mbflimsup  24910  ig1pdvds  25421  ulmval  25619  ulmpm  25622  2sqlem6  26651  ballotlemfc0  32595  ballotlemfcc  32596  ballotlemiex  32604  ballotlemsima  32618  ballotlemrv2  32624  breprexplemc  32748  erdszelem4  33291  erdszelem8  33295  caures  35995  diophin  40815  irrapxlem1  40865  monotuz  40985  hashnzfzclim  42179  uzmptshftfval  42203  uzct  42850  uzfissfz  43119  ssuzfz  43142  uzssre2  43201  uzssz2  43250  uzinico2  43355  fnlimfvre  43470  climleltrp  43472  limsupequzmpt2  43514  limsupequzlem  43518  liminfequzmpt2  43587  ioodvbdlimc1lem2  43728  ioodvbdlimc2lem  43730  sge0isum  44221  smflimlem1  44565  smflimlem2  44566  smflim  44571