Theorem eluz2 11007

Description: Membership in an upper set of integers. We use the fact that a function's value (under our function value definition) is empty outside of its domain to show M e. ZZ. (Contributed by NM, 5-Sep-2005.) (Revised by Mario Carneiro, 3-Nov-2013.)

Assertion

Ref	Expression
eluz2	|- ( N e. ( ZZ>= ` M ) <-> ( M e. ZZ /\ N e. ZZ /\ M <_ N ) )

Proof of Theorem eluz2

Step	Hyp	Ref	Expression
1		eluzel2 11006	. 2 |- ( N e. ( ZZ>= ` M ) -> M e. ZZ )
2		simp1 994	. 2 |- ( ( M e. ZZ /\ N e. ZZ /\ M <_ N ) -> M e. ZZ )
3		eluz1 11005	. . . 4 |- ( M e. ZZ -> ( N e. ( ZZ>= ` M ) <-> ( N e. ZZ /\ M <_ N ) ) )
4		ibar 502	. . . 4 |- ( M e. ZZ -> ( ( N e. ZZ /\ M <_ N ) <-> ( M e. ZZ /\ ( N e. ZZ /\ M <_ N ) ) ) )
5	3, 4	bitrd 253	. . 3 |- ( M e. ZZ -> ( N e. ( ZZ>= ` M ) <-> ( M e. ZZ /\ ( N e. ZZ /\ M <_ N ) ) ) )
6		3anass 975	. . 3 |- ( ( M e. ZZ /\ N e. ZZ /\ M <_ N ) <-> ( M e. ZZ /\ ( N e. ZZ /\ M <_ N ) ) )
7	5, 6	syl6bbr 263	. 2 |- ( M e. ZZ -> ( N e. ( ZZ>= ` M ) <-> ( M e. ZZ /\ N e. ZZ /\ M <_ N ) ) )
8	1, 2, 7	pm5.21nii 351	1 |- ( N e. ( ZZ>= ` M ) <-> ( M e. ZZ /\ N e. ZZ /\ M <_ N ) )

Syntax hints:   <-> wb 184   /\ wa 367   /\ w3a 971   e. wcel 1826   class class class wbr 4367   ` cfv 5496   <_ cle 9540   ZZcz 10781   ZZ>=cuz 11001

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-8 1828  ax-9 1830  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360  ax-sep 4488  ax-nul 4496  ax-pow 4543  ax-pr 4601  ax-cnex 9459  ax-resscn 9460

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 972  df-3an 973  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-eu 2222  df-mo 2223  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2532  df-ne 2579  df-ral 2737  df-rex 2738  df-rab 2741  df-v 3036  df-sbc 3253  df-dif 3392  df-un 3394  df-in 3396  df-ss 3403  df-nul 3712  df-if 3858  df-pw 3929  df-sn 3945  df-pr 3947  df-op 3951  df-uni 4164  df-br 4368  df-opab 4426  df-mpt 4427  df-id 4709  df-xp 4919  df-rel 4920  df-cnv 4921  df-co 4922  df-dm 4923  df-rn 4924  df-res 4925  df-ima 4926  df-iota 5460  df-fun 5498  df-fn 5499  df-f 5500  df-fv 5504  df-ov 6199  df-neg 9721  df-z 10782  df-uz 11002

This theorem is referenced by:  eluzuzle  11009  eluzelz  11010  eluzle  11013  uztrn  11017  eluzp1p1  11026  uzm1  11031  uznn0sub  11032  uz3m2nn  11043  1eluzge0  11044  2eluzge0OLD  11046  2eluzge1  11047  raluz2  11050  rexuz2  11052  peano2uz  11054  nn0pzuz  11058  uzind4  11059  zsupss  11090  nn01to3  11094  nn0ge2m1nnALT  11095  elfzuzb  11603  uzsubsubfz  11628  ige2m1fz  11690  elfz0addOLD  11698  4fvwrd4  11715  elfzo2  11725  elfzouz2  11736  fzossrbm1  11749  fzossfzop1  11792  ssfzo12bi  11806  elfzonelfzo  11811  elfzomelpfzo  11813  fzosplitprm1  11818  fzostep1  11821  fzind2  11823  flword2  11848  uzsup  11890  modaddmodup  11953  fzsdom2  12390  swrdtrcfv0  12578  swrdsbslen  12584  swrdspsleq  12585  swrdtrcfvl  12586  swrdccatin12lem2a  12621  cshwidxmod  12685  rexuzre  13187  limsupgre  13306  rlimclim1  13370  rlimclim  13371  climrlim2  13372  isercolllem1  13489  isercoll  13492  climcndslem1  13663  bitsmod  14088  smueqlem  14142  prmgt1  14238  prmn2uzge3  14239  modprm0  14332  vdwlem9  14509  strlemor1  14729  strleun  14732  fislw  16762  efgsp1  16872  efgredleme  16878  lt6abl  17014  telgsumfzs  17131  ablfac1eu  17237  znidomb  18691  chfacfscmul0  19444  chfacfscmulfsupp  19445  chfacfpmmul0  19448  chfacfpmmulfsupp  19449  dvfsumlem1  22512  dvfsumlem3  22514  plyaddlem1  22695  coeidlem  22719  ppisval  23494  chtdif  23549  ppidif  23554  ppiublem1  23594  ppiub  23596  chtub  23604  lgsdilem2  23723  lgsquadlem1  23746  lgsquadlem3  23748  chebbnd1lem1  23771  chebbnd1lem2  23772  chebbnd1lem3  23773  dchrisumlem2  23792  dchrvmasumiflem1  23803  mulog2sumlem2  23837  logdivbnd  23858  pntlemg  23900  pntlemq  23903  pntlemf  23907  axlowdim  24385  4cycl4v4e  24787  4cycl4dv4e  24789  wwlknred  24844  wwlkm1edg  24856  clwlkisclwwlklem2fv1  24903  clwlkisclwwlklem1  24908  clwwlkf  24915  clwwlkext2edg  24923  wwlksubclwwlk  24925  clwwisshclwwlem  24927  usg2cwwkdifex  24942  clwlkfclwwlk  24965  eupath2lem3  25100  extwwlkfablem2  25199  numclwwlkovf2ex  25207  numclwlk1lem2f1  25215  frgrareggt1  25237  frgrareg  25238  frgraregord013  25239  ssnnssfz  27750  ballotlemsdom  28633  ballotlemsel1i  28634  ballotlemfrceq  28650  eluzmn  28674  signstfvc  28714  signstfveq0  28717  erdszelem8  28831  climuzcnv  29226  fallfacval4  29331  fdc  30404  eldioph2lem1  30858  hbt  31247  monoords  31662  fzdifsuc2  31678  fmul01lt1lem2  31745  sumnnodd  31802  ioodvbdlimc1lem2  31895  ioodvbdlimc2lem  31897  dvnmul  31906  dvnprodlem2  31910  itgspltprt  31944  stoweidlem11  31959  stoweidlem26  31974  wallispilem4  32016  fourierdlem12  32067  fourierdlem20  32075  fourierdlem41  32096  fourierdlem48  32103  fourierdlem49  32104  fourierdlem50  32105  fourierdlem54  32109  fourierdlem79  32134  fourierdlem102  32157  fourierdlem111  32166  fourierdlem114  32169  etransclem23  32206  etransclem48  32231  pfxtrcfv0  32577  pfxtrcfvl  32580  eluzge0nn0  32650  ssfz12  32651  elfzlble  32657  fzoopth  32660  cznnring  32964  ssnn0ssfz  33138  elfzolborelfzop1  33325  m1modmmod  33334  nn0o  33339  rege1logbzge0  33380  fllog2  33389  nnolog2flm1  33411  dignn0ldlem  33423