Theorem uzid 9945

Description: Membership of the least member in an upper set of integers. (Contributed by NM, 2-Sep-2005.)

Assertion

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

Proof of Theorem uzid

Step	Hyp	Ref	Expression
1		zre 9652	. . . 4 |- ( M e. ZZ -> M e. RR )
2	1	leidd 8843	. . 3 |- ( M e. ZZ -> M <_ M )
3	2	ancli 323	. 2 |- ( M e. ZZ -> ( M e. ZZ /\ M <_ M ) )
4		eluz1 9934	. 2 |- ( M e. ZZ -> ( M e. ( ZZ>= ` M ) <-> ( M e. ZZ /\ M <_ M ) ) )
5	3, 4	mpbird 167	1 |- ( M e. ZZ -> M e. ( ZZ>= ` M ) )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   e. wcel 2209   class class class wbr 4130   ` cfv 5377   <_ cle 8361   ZZcz 9648   ZZ>=cuz 9930

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 623  ax-in2 624  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-14 2212  ax-ext 2220  ax-sep 4249  ax-pow 4311  ax-pr 4346  ax-un 4578  ax-setind 4684  ax-cnex 8270  ax-resscn 8271  ax-pre-ltirr 8291

This proof depends on definitions:  df-bi 117  df-3or 1010  df-3an 1011  df-tru 1405  df-fal 1408  df-nf 1514  df-sb 1816  df-eu 2089  df-mo 2090  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ne 2421  df-nel 2516  df-ral 2533  df-rex 2534  df-rab 2537  df-v 2823  df-sbc 3052  df-dif 3222  df-un 3224  df-in 3226  df-ss 3233  df-pw 3690  df-sn 3715  df-pr 3716  df-op 3718  df-uni 3936  df-br 4131  df-opab 4193  df-mpt 4194  df-id 4438  df-xp 4780  df-rel 4781  df-cnv 4782  df-co 4783  df-dm 4784  df-iota 5337  df-fun 5379  df-fv 5385  df-ov 6088  df-pnf 8362  df-mnf 8363  df-xr 8364  df-ltxr 8365  df-le 8366  df-neg 8501  df-z 9649  df-uz 9931

This theorem is used by:  uzidd  9946  uzn0  9947  uz11  9954  eluzfz1  10445  eluzfz2  10446  elfz3  10448  elfz1end  10471  fzssp1  10483  fzpred  10487  fzp1ss  10490  fzpr  10494  fztp  10495  elfz0add  10537  fzolb  10571  zpnn0elfzo  10635  fzosplitsnm1  10637  fzofzp1  10655  fzosplitsn  10661  fzostep1  10666  zsupcllemstep  10672  zsupcllemex  10673  frec2uzuzd  10852  frecuzrdgrrn  10858  frec2uzrdg  10859  frecuzrdgrcl  10860  frecuzrdgsuc  10864  frecuzrdgrclt  10865  frecuzrdgg  10866  frecuzrdgsuctlem  10873  uzsinds  10894  seq3val  10910  seqvalcd  10911  seq3-1  10912  seqf  10914  seq3p1  10915  seq3fveq  10929  seq3-1p  10940  seq3caopr3  10941  iseqf1olemjpcl  10958  iseqf1olemqpcl  10959  seq3f1oleml  10966  seq3f1o  10967  seq3homo  10977  faclbnd3  11195  bcm1k  11212  bcn2  11216  seq3coll  11308  swrds1  11454  pfxccatpfx2  11523  rexuz3  11770  r19.2uz  11773  resqrexlemcvg  11799  resqrexlemgt0  11800  resqrexlemoverl  11801  cau3lem  11895  caubnd2  11898  climconst  12072  climuni  12075  climcau  12129  serf0  12134  fsumparts  12253  isum1p  12275  isumrpcl  12277  cvgratz  12315  mertenslemi1  12318  ntrivcvgap0  12332  fprodabs  12399  eftlub  12473  bitsfzo  12738  bitsinv1  12745  ialgr0  12838  eucalg  12853  oddpwdc  12970  eulerthlemrprm  13027  oddprm  13058  pcfac  13149  pcbc  13150  prmlem0  13240  ballotfilemfp1  13280  ennnfonelem1  13347  gzsumconst  14192  lmconst  15366  2logb9irr  16126  sqrt2cxp2logb9e3  16130  2logb9irrap  16132  ppinprm  16171  ppiublem1  16192  lgseisenlem4  16290  lgsquadlem1  16294  lgsquad2  16300  cvgcmp2nlemabs  17179  trilpolemlt1  17188