Theorem uzssz 9441

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	|- ( ZZ>= ` M ) C_ ZZ

Proof of Theorem uzssz

Dummy variable y is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eluzelz 9431	. 2 |- ( y e. ( ZZ>= ` M ) -> y e. ZZ )
2	1	ssriv 3132	1 |- ( ZZ>= ` M ) C_ ZZ

Syntax hints:   C_ wss 3102   ` cfv 5167   ZZcz 9150   ZZ>=cuz 9422

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-10 1485  ax-11 1486  ax-i12 1487  ax-bndl 1489  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-14 2131  ax-ext 2139  ax-sep 4082  ax-pow 4134  ax-pr 4168  ax-cnex 7806  ax-resscn 7807

This theorem depends on definitions:  df-bi 116  df-3or 964  df-3an 965  df-tru 1338  df-nf 1441  df-sb 1743  df-eu 2009  df-mo 2010  df-clab 2144  df-cleq 2150  df-clel 2153  df-nfc 2288  df-ral 2440  df-rex 2441  df-rab 2444  df-v 2714  df-sbc 2938  df-un 3106  df-in 3108  df-ss 3115  df-pw 3545  df-sn 3566  df-pr 3567  df-op 3569  df-uni 3773  df-br 3966  df-opab 4026  df-mpt 4027  df-id 4252  df-xp 4589  df-rel 4590  df-cnv 4591  df-co 4592  df-dm 4593  df-rn 4594  df-res 4595  df-ima 4596  df-iota 5132  df-fun 5169  df-fn 5170  df-f 5171  df-fv 5175  df-ov 5821  df-neg 8032  df-z 9151  df-uz 9423

This theorem is referenced by:  cau3  10997  climz  11171  serclim0  11184  climaddc1  11208  climmulc2  11210  climsubc1  11211  climsubc2  11212  climle  11213  climlec2  11220  summodclem2a  11260  summodclem2  11261  zsumdc  11263  fsum3cvg3  11275  iserabs  11354  isumshft  11369  explecnv  11384  clim2prod  11418  prodfclim1  11423  ntrivcvgap  11427  prodmodclem2a  11455  prodmodclem2  11456  zproddc  11458  infssuzcldc  11819  exmidunben  12127  lmbrf  12575  lmres  12608  climcncf  12931