Theorem eluz2 11172

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 11171	. 2 |- ( N e. ( ZZ>= ` M ) -> M e. ZZ )
2		simp1 1005	. 2 |- ( ( M e. ZZ /\ N e. ZZ /\ M <_ N ) -> M e. ZZ )
3		eluz1 11170	. . . 4 |- ( M e. ZZ -> ( N e. ( ZZ>= ` M ) <-> ( N e. ZZ /\ M <_ N ) ) )
4		ibar 506	. . . 4 |- ( M e. ZZ -> ( ( N e. ZZ /\ M <_ N ) <-> ( M e. ZZ /\ ( N e. ZZ /\ M <_ N ) ) ) )
5	3, 4	bitrd 256	. . 3 |- ( M e. ZZ -> ( N e. ( ZZ>= ` M ) <-> ( M e. ZZ /\ ( N e. ZZ /\ M <_ N ) ) ) )
6		3anass 986	. . 3 |- ( ( M e. ZZ /\ N e. ZZ /\ M <_ N ) <-> ( M e. ZZ /\ ( N e. ZZ /\ M <_ N ) ) )
7	5, 6	syl6bbr 266	. 2 |- ( M e. ZZ -> ( N e. ( ZZ>= ` M ) <-> ( M e. ZZ /\ N e. ZZ /\ M <_ N ) ) )
8	1, 2, 7	pm5.21nii 354	1 |- ( N e. ( ZZ>= ` M ) <-> ( M e. ZZ /\ N e. ZZ /\ M <_ N ) )

Syntax hints:   <-> wb 187   /\ wa 370   /\ w3a 982   e. wcel 1872   class class class wbr 4423   ` cfv 5601   <_ cle 9683   ZZcz 10944   ZZ>=cuz 11166

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401  ax-sep 4546  ax-nul 4555  ax-pow 4602  ax-pr 4660  ax-cnex 9602  ax-resscn 9603

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2273  df-mo 2274  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-ne 2616  df-ral 2776  df-rex 2777  df-rab 2780  df-v 3082  df-sbc 3300  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3912  df-pw 3983  df-sn 3999  df-pr 4001  df-op 4005  df-uni 4220  df-br 4424  df-opab 4483  df-mpt 4484  df-id 4768  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-rn 4864  df-res 4865  df-ima 4866  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-fv 5609  df-ov 6308  df-neg 9870  df-z 10945  df-uz 11167

This theorem is referenced by:  eluzuzle  11174  eluzelz  11175  eluzle  11178  uztrn  11182  eluzp1p1  11191  uzm1  11196  uznn0sub  11197  uz3m2nn  11208  1eluzge0  11209  2eluzge0OLD  11211  2eluzge1  11212  raluz2  11215  rexuz2  11217  peano2uz  11219  nn0pzuz  11223  uzind4  11224  uzinfi  11245  zsupss  11260  nn01to3  11264  nn0ge2m1nnALT  11265  elfzuzb  11801  uzsubsubfz  11828  ige2m1fz  11891  elfz0addOLD  11899  4fvwrd4  11916  elfzo2  11930  elfzouz2  11941  fzossrbm1  11954  fzossfzop1  11997  ssfzo12bi  12012  elfzonelfzo  12017  elfzomelpfzo  12019  fzosplitprm1  12024  fzostep1  12027  fzind2  12029  flword2  12054  uzsup  12096  modaddmodup  12159  fzsdom2  12604  swrdtrcfv0  12800  swrdsbslen  12806  swrdspsleq  12807  swrdtrcfvl  12808  swrdccatin12lem2a  12843  cshwidxmod  12907  rexuzre  13415  limsupgre  13541  limsupgreOLD  13542  rlimclim1  13608  rlimclim  13609  climrlim2  13610  isercolllem1  13727  isercoll  13730  climcndslem1  13906  fallfacval4  14095  bitsmod  14409  smueqlem  14463  prmgt1  14642  prmn2uzge3  14643  modprm0  14755  vdwlem9  14938  prmgaplem3  15022  prmgaplem5  15024  prmgaplem6  15025  prmgaplem7  15026  strlemor1  15216  strleun  15219  fislw  17276  efgsp1  17386  efgredleme  17392  lt6abl  17528  telgsumfzs  17618  ablfac1eu  17705  znidomb  19130  chfacfscmul0  19880  chfacfscmulfsupp  19881  chfacfpmmul0  19884  chfacfpmmulfsupp  19885  dvfsumlem1  22976  dvfsumlem3  22978  plyaddlem1  23165  coeidlem  23189  ppisval  24028  chtdif  24083  ppidif  24088  ppiublem1  24128  ppiub  24130  chtub  24138  lgsdilem2  24257  lgsquadlem1  24280  lgsquadlem3  24282  chebbnd1lem1  24305  chebbnd1lem2  24306  chebbnd1lem3  24307  dchrisumlem2  24326  dchrvmasumiflem1  24337  mulog2sumlem2  24371  logdivbnd  24392  pntlemg  24434  pntlemq  24437  pntlemf  24441  axlowdim  24989  4cycl4v4e  25392  4cycl4dv4e  25394  wwlknred  25449  wwlkm1edg  25461  clwlkisclwwlklem2fv1  25508  clwlkisclwwlklem1  25513  clwwlkf  25520  clwwlkext2edg  25528  wwlksubclwwlk  25530  clwwisshclwwlem  25532  usg2cwwkdifex  25547  clwlkfclwwlk  25570  eupath2lem3  25705  extwwlkfablem2  25804  numclwwlkovf2ex  25812  numclwlk1lem2f1  25820  frgrareggt1  25842  frgrareg  25843  frgraregord013  25844  ssnnssfz  28373  ballotlemsdom  29352  ballotlemsel1i  29353  ballotlemfrceq  29369  ballotlemsdomOLD  29390  ballotlemsel1iOLD  29391  ballotlemfrceqOLD  29407  eluzmn  29431  signstfvc  29471  signstfveq0  29474  erdszelem8  29929  climuzcnv  30323  poimirlem6  31910  fdc  32038  eldioph2lem1  35571  hbt  35959  monoords  37468  fzdifsuc2  37484  fmul01lt1lem2  37603  sumnnodd  37650  ioodvbdlimc1lem2  37744  ioodvbdlimc1lem2OLD  37746  ioodvbdlimc2lem  37748  ioodvbdlimc2lemOLD  37749  dvnmul  37758  dvnprodlem2  37762  itgspltprt  37796  stoweidlem11  37811  stoweidlem26  37826  wallispilem4  37870  fourierdlem12  37921  fourierdlem20  37929  fourierdlem41  37951  fourierdlem48  37958  fourierdlem49  37959  fourierdlem50  37960  fourierdlem54  37964  fourierdlem79  37989  fourierdlem102  38012  fourierdlem111  38021  fourierdlem114  38024  etransclem23  38062  etransclem48OLD  38087  etransclem48  38088  caratheodorylem1  38255  fzopredsuc  38590  iccpartipre  38605  iccpartiltu  38606  iccpartgt  38611  gbegt5  38732  gbogt5  38733  nnsum3primesle9  38759  nnsum4primesodd  38761  nnsum4primesoddALTV  38762  evengpop3  38763  evengpoap3  38764  nnsum4primeseven  38765  nnsum4primesevenALTV  38766  wtgoldbnnsum4prm  38767  bgoldbnnsum3prm  38769  bgoldbtbndlem3  38772  tgblthelfgott  38778  pfxtrcfv0  38813  pfxtrcfvl  38816  eluzge0nn0  38907  ssfz12  38908  elfzlble  38914  fzoopth  38917  cznnring  39577  ssnn0ssfz  39751  elfzolborelfzop1  39937  m1modmmod  39945  nn0o  39950  rege1logbzge0  39991  fllog2  40000  nnolog2flm1  40022  dignn0ldlem  40034