Theorem eluz2 9736

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 9735	. 2 |- ( N e. ( ZZ>= ` M ) -> M e. ZZ )
2		simp1 1021	. 2 |- ( ( M e. ZZ /\ N e. ZZ /\ M <_ N ) -> M e. ZZ )
3		eluz1 9734	. . . 4 |- ( M e. ZZ -> ( N e. ( ZZ>= ` M ) <-> ( N e. ZZ /\ M <_ N ) ) )
4		ibar 301	. . . 4 |- ( M e. ZZ -> ( ( N e. ZZ /\ M <_ N ) <-> ( M e. ZZ /\ ( N e. ZZ /\ M <_ N ) ) ) )
5	3, 4	bitrd 188	. . 3 |- ( M e. ZZ -> ( N e. ( ZZ>= ` M ) <-> ( M e. ZZ /\ ( N e. ZZ /\ M <_ N ) ) ) )
6		3anass 1006	. . 3 |- ( ( M e. ZZ /\ N e. ZZ /\ M <_ N ) <-> ( M e. ZZ /\ ( N e. ZZ /\ M <_ N ) ) )
7	5, 6	bitr4di 198	. 2 |- ( M e. ZZ -> ( N e. ( ZZ>= ` M ) <-> ( M e. ZZ /\ N e. ZZ /\ M <_ N ) ) )
8	1, 2, 7	pm5.21nii 709	1 |- ( N e. ( ZZ>= ` M ) <-> ( M e. ZZ /\ N e. ZZ /\ M <_ N ) )

Syntax hints:   /\ wa 104   <-> wb 105   /\ w3a 1002   e. wcel 2200   class class class wbr 4083   ` cfv 5318   <_ cle 8190   ZZcz 9454   ZZ>=cuz 9730

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-14 2203  ax-ext 2211  ax-sep 4202  ax-pow 4258  ax-pr 4293  ax-cnex 8098  ax-resscn 8099

This theorem depends on definitions:  df-bi 117  df-3or 1003  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-eu 2080  df-mo 2081  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ral 2513  df-rex 2514  df-rab 2517  df-v 2801  df-sbc 3029  df-un 3201  df-in 3203  df-ss 3210  df-pw 3651  df-sn 3672  df-pr 3673  df-op 3675  df-uni 3889  df-br 4084  df-opab 4146  df-mpt 4147  df-id 4384  df-xp 4725  df-rel 4726  df-cnv 4727  df-co 4728  df-dm 4729  df-rn 4730  df-res 4731  df-ima 4732  df-iota 5278  df-fun 5320  df-fn 5321  df-f 5322  df-fv 5326  df-ov 6010  df-neg 8328  df-z 9455  df-uz 9731

This theorem is referenced by:  eluzuzle  9738  eluzelz  9739  eluzle  9742  uztrn  9747  eluzp1p1  9756  uznn0sub  9762  uz3m2nn  9776  1eluzge0  9777  2eluzge1  9779  raluz2  9782  rexuz2  9784  peano2uz  9786  nn0pzuz  9790  uzind4  9791  nn0ge2m1nnALT  9821  elfzuzb  10223  uzsubsubfz  10251  ige2m1fz  10314  4fvwrd4  10344  elfzo2  10354  elfzouz2  10366  fzossrbm1  10379  fzossfzop1  10426  ssfzo12bi  10439  elfzonelfzo  10444  elfzomelpfzo  10445  fzosplitprm1  10448  fzostep1  10451  fzind2  10453  suprzubdc  10464  zsupssdc  10466  flqword2  10517  fldiv4p1lem1div2  10533  uzennn  10666  xnn0nnen  10667  seq3split  10718  iseqf1olemqk  10737  seq3f1olemqsumkj  10741  seq3f1olemqsumk  10742  seq3f1olemqsum  10743  bcval5  10993  seq3coll  11072  swrdsbslen  11206  swrdspsleq  11207  pfxtrcfv0  11234  pfxtrcfvl  11237  pfxccatin12lem2a  11267  seq3shft  11357  resqrexlemoverl  11540  resqrexlemga  11542  fsum3cvg3  11915  fisumrev2  11965  isumshft  12009  cvgratnnlemseq  12045  cvgratnnlemabsle  12046  cvgratnnlemsumlt  12047  cvgratz  12051  oddge22np1  12400  nn0o  12426  bitsmod  12475  uzwodc  12566  dvdsnprmd  12655  prmgt1  12662  oddprmgt2  12664  oddprmge3  12665  prm23ge5  12795  nninfdclemcl  13027  nninfdclemp1  13029  nninfdclemlt  13030  strleund  13144  strleun  13145  gsumfzz  13536  gsumfzcl  13540  gsumfzreidx  13882  gsumfzsubmcl  13883  gsumfzmptfidmadd  13884  gsumfzmhm  13888  gsumfzfsum  14560  znidomb  14630  plyaddlem1  15429  2logb9irr  15653  2logb9irrap  15659  lgsdilem2  15723  gausslemma2dlem2  15749  gausslemma2dlem4  15751  gausslemma2dlem5  15753  gausslemma2dlem6  15754  lgsquadlem1  15764  lgsquadlem3  15766  2lgslem1  15778