Theorem eluz2 11155

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 11154	. 2 |- ( N e. ( ZZ>= ` M ) -> M e. ZZ )
2		simp1 1009	. 2 |- ( ( M e. ZZ /\ N e. ZZ /\ M <_ N ) -> M e. ZZ )
3		eluz1 11153	. . . 4 |- ( M e. ZZ -> ( N e. ( ZZ>= ` M ) <-> ( N e. ZZ /\ M <_ N ) ) )
4		ibar 511	. . . 4 |- ( M e. ZZ -> ( ( N e. ZZ /\ M <_ N ) <-> ( M e. ZZ /\ ( N e. ZZ /\ M <_ N ) ) ) )
5	3, 4	bitrd 261	. . 3 |- ( M e. ZZ -> ( N e. ( ZZ>= ` M ) <-> ( M e. ZZ /\ ( N e. ZZ /\ M <_ N ) ) ) )
6		3anass 990	. . 3 |- ( ( M e. ZZ /\ N e. ZZ /\ M <_ N ) <-> ( M e. ZZ /\ ( N e. ZZ /\ M <_ N ) ) )
7	5, 6	syl6bbr 271	. 2 |- ( M e. ZZ -> ( N e. ( ZZ>= ` M ) <-> ( M e. ZZ /\ N e. ZZ /\ M <_ N ) ) )
8	1, 2, 7	pm5.21nii 359	1 |- ( N e. ( ZZ>= ` M ) <-> ( M e. ZZ /\ N e. ZZ /\ M <_ N ) )

Syntax hints:   <-> wb 189   /\ wa 375   /\ w3a 986   e. wcel 1891   class class class wbr 4374   ` cfv 5561   <_ cle 9663   ZZcz 10927   ZZ>=cuz 11149

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1673  ax-4 1686  ax-5 1762  ax-6 1809  ax-7 1855  ax-8 1893  ax-9 1900  ax-10 1919  ax-11 1924  ax-12 1937  ax-13 2092  ax-ext 2432  ax-sep 4497  ax-nul 4506  ax-pow 4554  ax-pr 4612  ax-cnex 9582  ax-resscn 9583

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 987  df-3an 988  df-tru 1451  df-ex 1668  df-nf 1672  df-sb 1802  df-eu 2304  df-mo 2305  df-clab 2439  df-cleq 2445  df-clel 2448  df-nfc 2582  df-ne 2624  df-ral 2742  df-rex 2743  df-rab 2746  df-v 3015  df-sbc 3236  df-dif 3375  df-un 3377  df-in 3379  df-ss 3386  df-nul 3700  df-if 3850  df-pw 3921  df-sn 3937  df-pr 3939  df-op 3943  df-uni 4169  df-br 4375  df-opab 4434  df-mpt 4435  df-id 4727  df-xp 4818  df-rel 4819  df-cnv 4820  df-co 4821  df-dm 4822  df-rn 4823  df-res 4824  df-ima 4825  df-iota 5525  df-fun 5563  df-fn 5564  df-f 5565  df-fv 5569  df-ov 6279  df-neg 9850  df-z 10928  df-uz 11150

This theorem is referenced by:  eluzuzle  11157  eluzelz  11158  eluzle  11161  uztrn  11165  eluzp1p1  11174  uzm1  11179  uznn0sub  11180  uz3m2nn  11191  1eluzge0  11192  2eluzge0OLD  11194  2eluzge1  11195  raluz2  11198  rexuz2  11200  peano2uz  11202  nn0pzuz  11206  uzind4  11207  uzinfi  11228  zsupss  11243  nn01to3  11247  nn0ge2m1nnALT  11248  elfzuzb  11785  uzsubsubfz  11812  ige2m1fz  11875  elfz0addOLD  11883  4fvwrd4  11902  elfzo2  11916  elfzouz2  11927  fzossrbm1  11940  fzossfzop1  11984  ssfzo12bi  11999  elfzonelfzo  12004  elfzomelpfzo  12006  fzosplitprm1  12011  fzostep1  12014  fzind2  12016  flword2  12042  uzsup  12084  modaddmodup  12147  fzsdom2  12595  swrdtrcfv0  12797  swrdsbslen  12803  swrdspsleq  12804  swrdtrcfvl  12805  swrdccatin12lem2a  12840  cshwidxmod  12904  rexuzre  13426  limsupgre  13553  limsupgreOLD  13554  rlimclim1  13620  rlimclim  13621  climrlim2  13622  isercolllem1  13739  isercoll  13742  climcndslem1  13918  fallfacval4  14107  bitsmod  14421  smueqlem  14475  prmgt1  14654  prmn2uzge3  14655  modprm0  14767  vdwlem9  14950  prmgaplem3  15034  prmgaplem5  15036  prmgaplem6  15037  prmgaplem7  15038  strlemor1  15228  strleun  15231  fislw  17288  efgsp1  17398  efgredleme  17404  lt6abl  17540  telgsumfzs  17630  ablfac1eu  17717  znidomb  19143  chfacfscmul0  19893  chfacfscmulfsupp  19894  chfacfpmmul0  19897  chfacfpmmulfsupp  19898  dvfsumlem1  22990  dvfsumlem3  22992  plyaddlem1  23179  coeidlem  23203  ppisval  24042  chtdif  24097  ppidif  24102  ppiublem1  24142  ppiub  24144  chtub  24152  lgsdilem2  24271  lgsquadlem1  24294  lgsquadlem3  24296  chebbnd1lem1  24319  chebbnd1lem2  24320  chebbnd1lem3  24321  dchrisumlem2  24340  dchrvmasumiflem1  24351  mulog2sumlem2  24385  logdivbnd  24406  pntlemg  24448  pntlemq  24451  pntlemf  24455  axlowdim  25003  4cycl4v4e  25406  4cycl4dv4e  25408  wwlknred  25463  wwlkm1edg  25475  clwlkisclwwlklem2fv1  25522  clwlkisclwwlklem1  25527  clwwlkf  25534  clwwlkext2edg  25542  wwlksubclwwlk  25544  clwwisshclwwlem  25546  usg2cwwkdifex  25561  clwlkfclwwlk  25584  eupath2lem3  25719  extwwlkfablem2  25818  numclwwlkovf2ex  25826  numclwlk1lem2f1  25834  frgrareggt1  25856  frgrareg  25857  frgraregord013  25858  ssnnssfz  28375  ballotlemsdom  29350  ballotlemsel1i  29351  ballotlemfrceq  29367  ballotlemsdomOLD  29388  ballotlemsel1iOLD  29389  ballotlemfrceqOLD  29405  eluzmn  29429  signstfvc  29469  signstfveq0  29472  erdszelem8  29927  climuzcnv  30321  poimirlem6  31948  fdc  32076  eldioph2lem1  35604  hbt  35991  monoords  37545  fzdifsuc2  37561  fmul01lt1lem2  37705  sumnnodd  37752  ioodvbdlimc1lem2  37846  ioodvbdlimc1lem2OLD  37848  ioodvbdlimc2lem  37850  ioodvbdlimc2lemOLD  37851  dvnmul  37860  dvnprodlem2  37864  itgspltprt  37898  stoweidlem11  37928  stoweidlem26  37943  wallispilem4  37987  fourierdlem12  38038  fourierdlem20  38046  fourierdlem41  38068  fourierdlem48  38075  fourierdlem49  38076  fourierdlem50  38077  fourierdlem54  38081  fourierdlem79  38106  fourierdlem102  38129  fourierdlem111  38138  fourierdlem114  38141  etransclem23  38179  etransclem48OLD  38204  etransclem48  38205  caratheodorylem1  38411  fzopredsuc  38811  iccpartipre  38826  iccpartiltu  38827  iccpartgt  38832  gbegt5  38953  gbogt5  38954  nnsum3primesle9  38980  nnsum4primesodd  38982  nnsum4primesoddALTV  38983  evengpop3  38984  evengpoap3  38985  nnsum4primeseven  38986  nnsum4primesevenALTV  38987  wtgoldbnnsum4prm  38988  bgoldbnnsum3prm  38990  bgoldbtbndlem3  38993  tgblthelfgott  38999  pfxtrcfv0  39036  pfxtrcfvl  39039  eluzge0nn0  39147  ssfz12  39148  elfzlble  39154  fzoopth  39157  pthdlem1  39844  cznnring  40283  ssnn0ssfz  40455  elfzolborelfzop1  40641  m1modmmod  40649  nn0o  40654  rege1logbzge0  40695  fllog2  40704  nnolog2flm1  40726  dignn0ldlem  40738