Theorem uzid 9132

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 8852	. . . 4 |- ( M e. ZZ -> M e. RR )
2	1	leidd 8089	. . 3 |- ( M e. ZZ -> M <_ M )
3	2	ancli 317	. 2 |- ( M e. ZZ -> ( M e. ZZ /\ M <_ M ) )
4		eluz1 9122	. 2 |- ( M e. ZZ -> ( M e. ( ZZ>= ` M ) <-> ( M e. ZZ /\ M <_ M ) ) )
5	3, 4	mpbird 166	1 |- ( M e. ZZ -> M e. ( ZZ>= ` M ) )

Syntax hints:   -> wi 4   /\ wa 103   e. wcel 1445   class class class wbr 3867   ` cfv 5049   <_ cle 7620   ZZcz 8848   ZZ>=cuz 9118

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 582  ax-in2 583  ax-io 668  ax-5 1388  ax-7 1389  ax-gen 1390  ax-ie1 1434  ax-ie2 1435  ax-8 1447  ax-10 1448  ax-11 1449  ax-i12 1450  ax-bndl 1451  ax-4 1452  ax-13 1456  ax-14 1457  ax-17 1471  ax-i9 1475  ax-ial 1479  ax-i5r 1480  ax-ext 2077  ax-sep 3978  ax-pow 4030  ax-pr 4060  ax-un 4284  ax-setind 4381  ax-cnex 7533  ax-resscn 7534  ax-pre-ltirr 7554

This theorem depends on definitions:  df-bi 116  df-3or 928  df-3an 929  df-tru 1299  df-fal 1302  df-nf 1402  df-sb 1700  df-eu 1958  df-mo 1959  df-clab 2082  df-cleq 2088  df-clel 2091  df-nfc 2224  df-ne 2263  df-nel 2358  df-ral 2375  df-rex 2376  df-rab 2379  df-v 2635  df-sbc 2855  df-dif 3015  df-un 3017  df-in 3019  df-ss 3026  df-pw 3451  df-sn 3472  df-pr 3473  df-op 3475  df-uni 3676  df-br 3868  df-opab 3922  df-mpt 3923  df-id 4144  df-xp 4473  df-rel 4474  df-cnv 4475  df-co 4476  df-dm 4477  df-iota 5014  df-fun 5051  df-fv 5057  df-ov 5693  df-pnf 7621  df-mnf 7622  df-xr 7623  df-ltxr 7624  df-le 7625  df-neg 7753  df-z 8849  df-uz 9119

This theorem is referenced by:  uzn0  9133  uz11  9140  eluzfz1  9594  eluzfz2  9595  elfz3  9597  elfz1end  9618  fzssp1  9630  fzpred  9633  fzp1ss  9636  fzpr  9640  fztp  9641  elfz0add  9683  fzolb  9713  zpnn0elfzo  9767  fzosplitsnm1  9769  fzofzp1  9787  fzosplitsn  9793  fzostep1  9797  frec2uzuzd  9958  frecuzrdgrrn  9964  frec2uzrdg  9965  frecuzrdgrcl  9966  frecuzrdgsuc  9970  frecuzrdgrclt  9971  frecuzrdgg  9972  frecuzrdgsuctlem  9979  uzsinds  9997  seq3val  10013  seq3-1  10014  seqf  10015  seq3p1  10016  seq3fveq  10021  seq3-1p  10030  seq3caopr3  10031  iseqf1olemjpcl  10045  iseqf1olemqpcl  10046  seq3f1oleml  10053  seq3f1o  10054  seq3homo  10060  faclbnd3  10266  bcm1k  10283  bcn2  10287  seq3coll  10362  rexuz3  10538  r19.2uz  10541  resqrexlemcvg  10567  resqrexlemgt0  10568  resqrexlemoverl  10569  cau3lem  10662  caubnd2  10665  climconst  10833  climuni  10836  climcau  10890  serf0  10895  fsumparts  11013  isum1p  11035  isumrpcl  11037  cvgratz  11075  mertenslemi1  11078  eftlub  11129  zsupcllemstep  11368  zsupcllemex  11369  ialgr0  11453  eucalg  11468  pw2dvds  11571  lmconst  12067