Theorem uzid 10456

Description: Membership of the least member in a set of upper 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 10242	. . . 4 |- ( M e. ZZ -> M e. RR )
2	1	leidd 9549	. . 3 |- ( M e. ZZ -> M <_ M )
3	2	ancli 535	. 2 |- ( M e. ZZ -> ( M e. ZZ /\ M <_ M ) )
4		eluz1 10448	. 2 |- ( M e. ZZ -> ( M e. ( ZZ>= ` M ) <-> ( M e. ZZ /\ M <_ M ) ) )
5	3, 4	mpbird 224	1 |- ( M e. ZZ -> M e. ( ZZ>= ` M ) )

Syntax hints:   -> wi 4   /\ wa 359   e. wcel 1721   class class class wbr 4172   ` cfv 5413   <_ cle 9077   ZZcz 10238   ZZ>=cuz 10444

This theorem is referenced by:  uzn0  10457  uz11  10464  uzinfmi  10511  uzsupss  10524  eluzfz1  11020  eluzfz2  11021  elfz3  11023  elfz1end  11037  fzssp1  11051  fzp1ss  11054  fzpr  11057  fztp  11058  fzolb  11100  fzofzp1  11144  fzosplitsn  11150  fzostep1  11152  om2uzuzi  11244  axdc4uzlem  11276  seqf  11299  seqfveq  11302  seq1p  11312  faclbnd3  11538  bcm1k  11561  bcn2  11565  seqcoll  11667  ccatass  11705  swrdccat1  11729  swrdccat2  11730  splfv1  11739  splval2  11741  swrds1  11742  revccat  11753  rexuz3  12107  r19.2uz  12110  cau3lem  12113  caubnd2  12116  climconst  12292  climuni  12301  isercoll2  12417  climsup  12418  climcau  12419  serf0  12429  iseralt  12433  fsumcvg3  12478  fsumparts  12540  o1fsum  12547  abscvgcvg  12553  isum1p  12576  isumrpcl  12578  isumsup2  12581  climcndslem1  12584  climcndslem2  12585  climcnds  12586  cvgrat  12615  mertenslem1  12616  eftlub  12665  rpnnen2lem11  12779  bitsfzo  12902  bitsinv1  12909  smupval  12955  seq1st  13017  algr0  13018  eucalg  13033  oddprm  13144  pcfac  13223  pcbc  13224  vdwlem6  13309  prmlem0  13383  gsumccat  14742  efginvrel2  15314  efgsres  15325  lmconst  17279  lmmo  17398  zfbas  17881  uzrest  17882  iscau2  19183  iscau4  19185  caun0  19187  caussi  19203  equivcau  19206  lmcau  19218  mbfsup  19509  mbfinf  19510  mbflimsup  19511  plyco0  20064  dvply2g  20155  geolim3  20209  aaliou3lem2  20213  aaliou3lem3  20214  ulm2  20254  ulm0  20260  ulmcaulem  20263  ulmcau  20264  ulmss  20266  ulmcn  20268  ulmdvlem3  20271  ulmdv  20272  abelthlem7  20307  ppinprm  20888  chtnprm  20890  ppiublem1  20939  chtublem  20948  chtub  20949  bposlem6  21026  lgsqr  21083  lgseisenlem4  21089  lgsquadlem1  21091  lgsquad2  21097  pntpbnd1  21233  pntlemf  21252  ostth2lem2  21281  3v3e3cycl1  21584  esumcvg  24429  dya2ub  24573  dya2icoseg  24580  ballotlemfp1  24702  ntrivcvgn0  25179  fprodabs  25250  fprodefsum  25251  iprodefisumlem  25270  binomfallfaclem2  25307  axlowdimlem17  25801  mblfinlem  26143  sdclem1  26337  fdc  26339  seqpo  26341  incsequz2  26343  geomcau  26355  bfplem2  26422  eq0rabdioph  26725  rexrabdioph  26744  jm3.1lem1  26978  fmul01lt1lem1  27581  climinf  27599  climsuse  27601  stoweidlem7  27623  wallispilem1  27681  wallispilem4  27684  fzosplitsnm1  27991  swrdccatin2  28018  swrdccatin12  28026

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-sep 4290  ax-nul 4298  ax-pow 4337  ax-pr 4363  ax-un 4660  ax-cnex 9002  ax-resscn 9003  ax-pre-lttri 9020

This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-nel 2570  df-ral 2671  df-rex 2672  df-rab 2675  df-v 2918  df-sbc 3122  df-csb 3212  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-pw 3761  df-sn 3780  df-pr 3781  df-op 3783  df-uni 3976  df-br 4173  df-opab 4227  df-mpt 4228  df-id 4458  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850  df-iota 5377  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-fv 5421  df-ov 6043  df-er 6864  df-en 7069  df-dom 7070  df-sdom 7071  df-pnf 9078  df-mnf 9079  df-xr 9080  df-ltxr 9081  df-le 9082  df-neg 9250  df-z 10239  df-uz 10445