Theorem eluz2 9654

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 9653	. 2 |- ( N e. ( ZZ>= ` M ) -> M e. ZZ )
2		simp1 1000	. 2 |- ( ( M e. ZZ /\ N e. ZZ /\ M <_ N ) -> M e. ZZ )
3		eluz1 9652	. . . 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 985	. . 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 706	1 |- ( N e. ( ZZ>= ` M ) <-> ( M e. ZZ /\ N e. ZZ /\ M <_ N ) )

Syntax hints:   /\ wa 104   <-> wb 105   /\ w3a 981   e. wcel 2176   class class class wbr 4044   ` cfv 5271   <_ cle 8108   ZZcz 9372   ZZ>=cuz 9648

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 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-14 2179  ax-ext 2187  ax-sep 4162  ax-pow 4218  ax-pr 4253  ax-cnex 8016  ax-resscn 8017

This theorem depends on definitions:  df-bi 117  df-3or 982  df-3an 983  df-tru 1376  df-nf 1484  df-sb 1786  df-eu 2057  df-mo 2058  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-ral 2489  df-rex 2490  df-rab 2493  df-v 2774  df-sbc 2999  df-un 3170  df-in 3172  df-ss 3179  df-pw 3618  df-sn 3639  df-pr 3640  df-op 3642  df-uni 3851  df-br 4045  df-opab 4106  df-mpt 4107  df-id 4340  df-xp 4681  df-rel 4682  df-cnv 4683  df-co 4684  df-dm 4685  df-rn 4686  df-res 4687  df-ima 4688  df-iota 5232  df-fun 5273  df-fn 5274  df-f 5275  df-fv 5279  df-ov 5947  df-neg 8246  df-z 9373  df-uz 9649

This theorem is referenced by:  eluzuzle  9656  eluzelz  9657  eluzle  9660  uztrn  9665  eluzp1p1  9674  uznn0sub  9680  uz3m2nn  9694  1eluzge0  9695  2eluzge1  9697  raluz2  9700  rexuz2  9702  peano2uz  9704  nn0pzuz  9708  uzind4  9709  nn0ge2m1nnALT  9739  elfzuzb  10141  uzsubsubfz  10169  ige2m1fz  10232  4fvwrd4  10262  elfzo2  10272  elfzouz2  10284  fzossrbm1  10297  fzossfzop1  10341  ssfzo12bi  10354  elfzonelfzo  10359  elfzomelpfzo  10360  fzosplitprm1  10363  fzostep1  10366  fzind2  10368  suprzubdc  10379  zsupssdc  10381  flqword2  10432  fldiv4p1lem1div2  10448  uzennn  10581  xnn0nnen  10582  seq3split  10633  iseqf1olemqk  10652  seq3f1olemqsumkj  10656  seq3f1olemqsumk  10657  seq3f1olemqsum  10658  bcval5  10908  seq3coll  10987  swrdsbslen  11119  swrdspsleq  11120  seq3shft  11149  resqrexlemoverl  11332  resqrexlemga  11334  fsum3cvg3  11707  fisumrev2  11757  isumshft  11801  cvgratnnlemseq  11837  cvgratnnlemabsle  11838  cvgratnnlemsumlt  11839  cvgratz  11843  oddge22np1  12192  nn0o  12218  bitsmod  12267  uzwodc  12358  dvdsnprmd  12447  prmgt1  12454  oddprmgt2  12456  oddprmge3  12457  prm23ge5  12587  nninfdclemcl  12819  nninfdclemp1  12821  nninfdclemlt  12822  strleund  12935  strleun  12936  gsumfzz  13327  gsumfzcl  13331  gsumfzreidx  13673  gsumfzsubmcl  13674  gsumfzmptfidmadd  13675  gsumfzmhm  13679  gsumfzfsum  14350  znidomb  14420  plyaddlem1  15219  2logb9irr  15443  2logb9irrap  15449  lgsdilem2  15513  gausslemma2dlem2  15539  gausslemma2dlem4  15541  gausslemma2dlem5  15543  gausslemma2dlem6  15544  lgsquadlem1  15554  lgsquadlem3  15556  2lgslem1  15568