Theorem eluzelz 9442

Description: A member of an upper set of integers is an integer. (Contributed by NM, 6-Sep-2005.)

Assertion

Ref	Expression
eluzelz	|- ( N e. ( ZZ>= ` M ) -> N e. ZZ )

Proof of Theorem eluzelz

Step	Hyp	Ref	Expression
1		eluz2 9439	. 2 |- ( N e. ( ZZ>= ` M ) <-> ( M e. ZZ /\ N e. ZZ /\ M <_ N ) )
2	1	simp2bi 998	1 |- ( N e. ( ZZ>= ` M ) -> N e. ZZ )

Syntax hints:   -> wi 4   e. wcel 2128   class class class wbr 3965   ` cfv 5169   <_ cle 7907   ZZcz 9161   ZZ>=cuz 9433

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 4135  ax-pr 4169  ax-cnex 7817  ax-resscn 7818

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 4253  df-xp 4591  df-rel 4592  df-cnv 4593  df-co 4594  df-dm 4595  df-rn 4596  df-res 4597  df-ima 4598  df-iota 5134  df-fun 5171  df-fn 5172  df-f 5173  df-fv 5177  df-ov 5824  df-neg 8043  df-z 9162  df-uz 9434

This theorem is referenced by:  eluzelre  9443  uztrn  9449  uzneg  9451  uzssz  9452  uzss  9453  eluzp1l  9457  eluzaddi  9459  eluzsubi  9460  eluzadd  9461  eluzsub  9462  uzm1  9463  uzin  9465  uzind4  9493  uz2mulcl  9512  elfz5  9913  elfzel2  9919  elfzelz  9921  eluzfz2  9927  peano2fzr  9932  fzsplit2  9945  fzopth  9956  fzsuc  9964  elfzp1  9967  fzdifsuc  9976  uzsplit  9987  uzdisj  9988  fzm1  9995  fzneuz  9996  uznfz  9998  nn0disj  10030  elfzo3  10055  fzoss2  10064  fzouzsplit  10071  eluzgtdifelfzo  10089  fzosplitsnm1  10101  fzofzp1b  10120  elfzonelfzo  10122  fzosplitsn  10125  fzisfzounsn  10128  mulp1mod1  10257  m1modge3gt1  10263  frec2uzltd  10295  frecfzen2  10319  uzennn  10328  uzsinds  10334  seq3fveq2  10361  seq3feq2  10362  seq3shft2  10365  monoord  10368  monoord2  10369  ser3mono  10370  seq3split  10371  iseqf1olemjpcl  10387  iseqf1olemqpcl  10388  seq3f1olemqsumk  10391  seq3f1olemp  10394  seq3f1oleml  10395  seq3f1o  10396  seq3id  10400  seq3z  10403  fser0const  10408  leexp2a  10465  expnlbnd2  10536  hashfz  10688  hashfzo  10689  hashfzp1  10691  seq3coll  10706  seq3shft  10731  rexuz3  10883  r19.2uz  10886  cau4  11009  caubnd2  11010  clim  11171  climshft2  11196  climaddc1  11219  climmulc2  11221  climsubc1  11222  climsubc2  11223  clim2ser  11227  clim2ser2  11228  iserex  11229  climlec2  11231  climub  11234  climcau  11237  climcaucn  11241  serf0  11242  sumrbdclem  11267  fsum3cvg  11268  summodclem2a  11271  zsumdc  11274  fsum3  11277  fisumss  11282  fsum3cvg2  11284  fsum3ser  11287  fsumcl2lem  11288  fsumadd  11296  fsumm1  11306  fzosump1  11307  fsum1p  11308  fsump1  11310  fsummulc2  11338  telfsumo  11356  fsumparts  11360  iserabs  11365  binomlem  11373  isumshft  11380  isumsplit  11381  isumrpcl  11384  divcnv  11387  trireciplem  11390  geosergap  11396  geolim2  11402  cvgratnnlemseq  11416  cvgratnnlemabsle  11417  cvgratnnlemsumlt  11418  cvgratnnlemrate  11420  cvgratz  11422  cvgratgt0  11423  mertenslemi1  11425  clim2divap  11430  prodrbdclem  11461  fproddccvg  11462  prodmodclem3  11465  prodmodclem2a  11466  zproddc  11469  fprodntrivap  11474  fprodssdc  11480  fprodm1  11488  fprod1p  11489  fprodp1  11490  fprodabs  11506  fprodeq0  11507  efgt1p2  11585  zsupcllemstep  11824  infssuzex  11828  dvdsbnd  11831  ncoprmgcdne1b  11957  isprm3  11986  prmind2  11988  nprm  11991  dvdsprm  12004  exprmfct  12005  phibndlem  12079  phibnd  12080  dfphi2  12083  hashdvds  12084  relogbval  13239  relogbzcl  13240  nnlogbexp  13247  logblt  13250  logbgcd1irr  13255  supfz  13610