Theorem eluz2 9739

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 9738	. 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 9737	. . . 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 8193   ZZcz 9457   ZZ>=cuz 9733

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 8101  ax-resscn 8102

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 8331  df-z 9458  df-uz 9734

This theorem is referenced by:  eluzmn  9740  eluzuzle  9742  eluzelz  9743  eluzle  9746  uztrn  9751  eluzp1p1  9760  uznn0sub  9766  uz3m2nn  9780  1eluzge0  9781  2eluzge1  9783  raluz2  9786  rexuz2  9788  peano2uz  9790  nn0pzuz  9794  uzind4  9795  nn0ge2m1nnALT  9825  elfzuzb  10227  uzsubsubfz  10255  ige2m1fz  10318  4fvwrd4  10348  elfzo2  10358  elfzouz2  10370  fzossrbm1  10383  fzossfzop1  10430  ssfzo12bi  10443  elfzonelfzo  10448  elfzomelpfzo  10449  fzosplitprm1  10452  fzostep1  10455  fzind2  10457  suprzubdc  10468  zsupssdc  10470  flqword2  10521  fldiv4p1lem1div2  10537  uzennn  10670  xnn0nnen  10671  seq3split  10722  iseqf1olemqk  10741  seq3f1olemqsumkj  10745  seq3f1olemqsumk  10746  seq3f1olemqsum  10747  bcval5  10997  seq3coll  11077  swrdsbslen  11214  swrdspsleq  11215  pfxtrcfv0  11242  pfxtrcfvl  11245  pfxccatin12lem2a  11275  seq3shft  11365  resqrexlemoverl  11548  resqrexlemga  11550  fsum3cvg3  11923  fisumrev2  11973  isumshft  12017  cvgratnnlemseq  12053  cvgratnnlemabsle  12054  cvgratnnlemsumlt  12055  cvgratz  12059  oddge22np1  12408  nn0o  12434  bitsmod  12483  uzwodc  12574  dvdsnprmd  12663  prmgt1  12670  oddprmgt2  12672  oddprmge3  12673  prm23ge5  12803  nninfdclemcl  13035  nninfdclemp1  13037  nninfdclemlt  13038  strleund  13152  strleun  13153  gsumfzz  13544  gsumfzcl  13548  gsumfzreidx  13890  gsumfzsubmcl  13891  gsumfzmptfidmadd  13892  gsumfzmhm  13896  gsumfzfsum  14568  znidomb  14638  plyaddlem1  15437  2logb9irr  15661  2logb9irrap  15667  lgsdilem2  15731  gausslemma2dlem2  15757  gausslemma2dlem4  15759  gausslemma2dlem5  15761  gausslemma2dlem6  15762  lgsquadlem1  15772  lgsquadlem3  15774  2lgslem1  15786  clwwlkext2edg  16164