Theorem eluz2 11098

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 11097	. 2 |- ( N e. ( ZZ>= ` M ) -> M e. ZZ )
2		simp1 997	. 2 |- ( ( M e. ZZ /\ N e. ZZ /\ M <_ N ) -> M e. ZZ )
3		eluz1 11096	. . . 4 |- ( M e. ZZ -> ( N e. ( ZZ>= ` M ) <-> ( N e. ZZ /\ M <_ N ) ) )
4		ibar 504	. . . 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 978	. . 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 353	1 |- ( N e. ( ZZ>= ` M ) <-> ( M e. ZZ /\ N e. ZZ /\ M <_ N ) )

Syntax hints:   <-> wb 184   /\ wa 369   /\ w3a 974   e. wcel 1804   class class class wbr 4437   ` cfv 5578   <_ cle 9632   ZZcz 10871   ZZ>=cuz 11092

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-8 1806  ax-9 1808  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421  ax-sep 4558  ax-nul 4566  ax-pow 4615  ax-pr 4676  ax-cnex 9551  ax-resscn 9552

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 975  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-eu 2272  df-mo 2273  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ne 2640  df-ral 2798  df-rex 2799  df-rab 2802  df-v 3097  df-sbc 3314  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3771  df-if 3927  df-pw 3999  df-sn 4015  df-pr 4017  df-op 4021  df-uni 4235  df-br 4438  df-opab 4496  df-mpt 4497  df-id 4785  df-xp 4995  df-rel 4996  df-cnv 4997  df-co 4998  df-dm 4999  df-rn 5000  df-res 5001  df-ima 5002  df-iota 5541  df-fun 5580  df-fn 5581  df-f 5582  df-fv 5586  df-ov 6284  df-neg 9813  df-z 10872  df-uz 11093

This theorem is referenced by:  eluzuzle  11100  eluzelz  11101  eluzle  11104  uztrn  11108  eluzp1p1  11117  uzm1  11122  uznn0sub  11123  uz3m2nn  11134  1eluzge0  11135  2eluzge0OLD  11137  2eluzge1  11138  raluz2  11141  rexuz2  11143  peano2uz  11145  nn0pzuz  11149  uzind4  11150  zsupss  11182  nn01to3  11186  nn0ge2m1nnALT  11187  elfzuzb  11693  uzsubsubfz  11718  ige2m1fz  11779  elfz0addOLD  11787  4fvwrd4  11804  elfzo2  11814  elfzouz2  11824  fzossrbm1  11836  fzossfzop1  11875  ssfzo12bi  11889  elfzonelfzo  11894  elfzomelpfzo  11896  fzosplitprm1  11901  fzostep1  11904  fzind2  11906  flword2  11931  uzsup  11972  modaddmodup  12032  fzsdom2  12468  ccatval1  12577  swrdtrcfv0  12651  swrdtrcfvl  12657  swrdccatin12lem2a  12692  cshwidxmod  12756  rexuzre  13167  limsupgre  13286  rlimclim1  13350  rlimclim  13351  climrlim2  13352  isercolllem1  13469  isercoll  13472  climcndslem1  13643  bitsmod  14068  smueqlem  14122  prmgt1  14218  prmn2uzge3  14219  modprm0  14312  vdwlem9  14489  strlemor1  14706  strleun  14709  fislw  16624  efgsp1  16734  efgredleme  16740  lt6abl  16876  telgsumfzs  16997  ablfac1eu  17103  znidomb  18578  chfacfscmul0  19337  chfacfscmulfsupp  19338  chfacfpmmul0  19341  chfacfpmmulfsupp  19342  dvfsumlem1  22405  dvfsumlem3  22407  plyaddlem1  22588  coeidlem  22612  ppisval  23355  chtdif  23410  ppidif  23415  ppiublem1  23455  ppiub  23457  chtub  23465  lgsdilem2  23584  lgsquadlem1  23607  lgsquadlem3  23609  chebbnd1lem1  23632  chebbnd1lem2  23633  chebbnd1lem3  23634  dchrisumlem2  23653  dchrvmasumiflem1  23664  mulog2sumlem2  23698  logdivbnd  23719  pntlemg  23761  pntlemq  23764  pntlemf  23768  axlowdim  24242  4cycl4v4e  24644  4cycl4dv4e  24646  wwlknred  24701  wwlkm1edg  24713  clwlkisclwwlklem2fv1  24760  clwlkisclwwlklem1  24765  clwwlkf  24772  clwwlkext2edg  24780  wwlksubclwwlk  24782  clwwisshclwwlem  24784  usg2cwwkdifex  24799  clwlkfclwwlk  24822  eupath2lem3  24957  extwwlkfablem2  25056  numclwwlkovf2ex  25064  numclwlk1lem2f1  25072  frgrareggt1  25094  frgrareg  25095  frgraregord013  25096  ssnnssfz  27575  ballotlemsdom  28428  ballotlemsel1i  28429  ballotlemfrceq  28445  eluzmn  28469  signstfvc  28509  signstfveq0  28512  erdszelem8  28620  climuzcnv  29015  fallfacval4  29141  fdc  30214  eldioph2lem1  30669  hbt  31055  monoords  31450  fzdifsuc2  31466  fmul01lt1lem2  31533  sumnnodd  31590  ioodvbdlimc1lem2  31683  ioodvbdlimc2lem  31685  dvnmul  31694  dvnprodlem2  31698  itgspltprt  31732  stoweidlem11  31747  stoweidlem26  31762  wallispilem4  31804  fourierdlem12  31855  fourierdlem20  31863  fourierdlem41  31884  fourierdlem48  31891  fourierdlem49  31892  fourierdlem50  31893  fourierdlem54  31897  fourierdlem79  31922  fourierdlem102  31945  fourierdlem111  31954  fourierdlem114  31957  etransclem23  31994  etransclem48  32019  eluzge0nn0  32283  ssfz12  32284  elfzlble  32290  el2fzo  32293  fzoopth  32294  cznnring  32591  ssnn0ssfz  32806