Theorem eluz2 10863

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 10862	. 2 |- ( N e. ( ZZ>= ` M ) -> M e. ZZ )
2		simp1 983	. 2 |- ( ( M e. ZZ /\ N e. ZZ /\ M <_ N ) -> M e. ZZ )
3		eluz1 10861	. . . 4 |- ( M e. ZZ -> ( N e. ( ZZ>= ` M ) <-> ( N e. ZZ /\ M <_ N ) ) )
4		ibar 501	. . . 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 964	. . 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 960   e. wcel 1761   class class class wbr 4289   ` cfv 5415   <_ cle 9415   ZZcz 10642   ZZ>=cuz 10857

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-8 1763  ax-9 1765  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422  ax-sep 4410  ax-nul 4418  ax-pow 4467  ax-pr 4528  ax-cnex 9334  ax-resscn 9335

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 961  df-3an 962  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-eu 2261  df-mo 2262  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-ne 2606  df-ral 2718  df-rex 2719  df-rab 2722  df-v 2972  df-sbc 3184  df-dif 3328  df-un 3330  df-in 3332  df-ss 3339  df-nul 3635  df-if 3789  df-pw 3859  df-sn 3875  df-pr 3877  df-op 3881  df-uni 4089  df-br 4290  df-opab 4348  df-mpt 4349  df-id 4632  df-xp 4842  df-rel 4843  df-cnv 4844  df-co 4845  df-dm 4846  df-rn 4847  df-res 4848  df-ima 4849  df-iota 5378  df-fun 5417  df-fn 5418  df-f 5419  df-fv 5423  df-ov 6093  df-neg 9594  df-z 10643  df-uz 10858

This theorem is referenced by:  uzletr  10865  eluzelz  10866  eluzle  10869  uztrn  10873  eluzp1p1  10882  uzm1  10887  uznn0sub  10888  1eluzge0  10895  2eluzge0  10896  2eluzge1  10897  raluz2  10900  rexuz2  10902  peano2uz  10904  uzind4  10908  zsupss  10940  elfzuzb  11443  uzsubsubfz  11467  elfzelfzadd  11504  4fvwrd4  11529  elfzo2  11552  elfzouz2  11562  fzossrbm1  11574  fzossfzop1  11606  ssfzo12bi  11618  elfzonelfzo  11623  elfzomelpfzo  11625  fzostep1  11631  fzind2  11633  flword2  11657  uzsup  11698  modaddmodup  11758  fzsdom2  12185  ccatval1  12272  swrdtrcfv0  12334  swrdtrcfvl  12340  swrdccatin12lem2a  12372  cshwidxmod  12436  rexuzre  12836  limsupgre  12955  rlimclim1  13019  rlimclim  13020  climrlim2  13021  isercolllem1  13138  isercoll  13141  climcndslem1  13308  bitsmod  13628  smueqlem  13682  prmgt1  13778  modprm0  13869  vdwlem9  14046  strlemor1  14261  strleun  14264  fislw  16117  efgsp1  16227  efgredleme  16233  lt6abl  16364  ablfac1eu  16564  znidomb  17953  dvfsumlem1  21457  dvfsumlem3  21459  plyaddlem1  21640  coeidlem  21664  ppisval  22400  chtdif  22455  ppidif  22460  ppiublem1  22500  ppiub  22502  chtub  22510  lgsdilem2  22629  lgsquadlem1  22652  lgsquadlem3  22654  chebbnd1lem1  22677  chebbnd1lem2  22678  chebbnd1lem3  22679  dchrisumlem2  22698  dchrvmasumiflem1  22709  mulog2sumlem2  22743  logdivbnd  22764  pntlemg  22806  pntlemq  22809  pntlemf  22813  axlowdim  23142  4cycl4v4e  23487  4cycl4dv4e  23489  eupath2lem3  23535  ssnnssfz  26009  ballotlemsdom  26824  ballotlemsel1i  26825  ballotlemfrceq  26841  eluzmn  26865  signstfvc  26905  signstfveq0  26908  erdszelem8  27016  climuzcnv  27245  fallfacval4  27475  fdc  28566  eldioph2lem1  29023  hbt  29411  fmul01lt1lem2  29691  stoweidlem11  29731  stoweidlem26  29746  wallispilem4  29788  nn0ge2m1nn  30109  nn01to3  30112  eluzge0nn0  30114  uzuzle  30115  uz3m2nn  30120  nn0pzuz  30121  ssfz12  30122  ige2m1fz  30131  elfzlble  30133  el2fzo  30137  fzoopth  30138  elfzom1elfzo  30142  fzosplitprm1  30149  prmn2uzge3  30174  wwlknred  30280  wwlkm1edg  30292  clwlkisclwwlklem2fv1  30369  clwlkisclwwlklem1  30374  clwwlkf  30381  clwwlkext2edg  30389  wwlksubclwwlk  30391  clwwisshclwwlem  30395  usg2cwwkdifex  30420  clwlkfclwwlk  30442  extwwlkfablem2  30596  numclwwlkovf2ex  30604  numclwlk1lem2f1  30612  frgrareggt1  30634  frgrareg  30635  frgraregord013  30636