Theorem eluz2 9689

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 9688	. 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 9687	. . . 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 2178   class class class wbr 4059   ` cfv 5290   <_ cle 8143   ZZcz 9407   ZZ>=cuz 9683

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 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-14 2181  ax-ext 2189  ax-sep 4178  ax-pow 4234  ax-pr 4269  ax-cnex 8051  ax-resscn 8052

This theorem depends on definitions:  df-bi 117  df-3or 982  df-3an 983  df-tru 1376  df-nf 1485  df-sb 1787  df-eu 2058  df-mo 2059  df-clab 2194  df-cleq 2200  df-clel 2203  df-nfc 2339  df-ral 2491  df-rex 2492  df-rab 2495  df-v 2778  df-sbc 3006  df-un 3178  df-in 3180  df-ss 3187  df-pw 3628  df-sn 3649  df-pr 3650  df-op 3652  df-uni 3865  df-br 4060  df-opab 4122  df-mpt 4123  df-id 4358  df-xp 4699  df-rel 4700  df-cnv 4701  df-co 4702  df-dm 4703  df-rn 4704  df-res 4705  df-ima 4706  df-iota 5251  df-fun 5292  df-fn 5293  df-f 5294  df-fv 5298  df-ov 5970  df-neg 8281  df-z 9408  df-uz 9684

This theorem is referenced by:  eluzuzle  9691  eluzelz  9692  eluzle  9695  uztrn  9700  eluzp1p1  9709  uznn0sub  9715  uz3m2nn  9729  1eluzge0  9730  2eluzge1  9732  raluz2  9735  rexuz2  9737  peano2uz  9739  nn0pzuz  9743  uzind4  9744  nn0ge2m1nnALT  9774  elfzuzb  10176  uzsubsubfz  10204  ige2m1fz  10267  4fvwrd4  10297  elfzo2  10307  elfzouz2  10319  fzossrbm1  10332  fzossfzop1  10378  ssfzo12bi  10391  elfzonelfzo  10396  elfzomelpfzo  10397  fzosplitprm1  10400  fzostep1  10403  fzind2  10405  suprzubdc  10416  zsupssdc  10418  flqword2  10469  fldiv4p1lem1div2  10485  uzennn  10618  xnn0nnen  10619  seq3split  10670  iseqf1olemqk  10689  seq3f1olemqsumkj  10693  seq3f1olemqsumk  10694  seq3f1olemqsum  10695  bcval5  10945  seq3coll  11024  swrdsbslen  11157  swrdspsleq  11158  pfxtrcfv0  11185  pfxtrcfvl  11188  pfxccatin12lem2a  11218  seq3shft  11264  resqrexlemoverl  11447  resqrexlemga  11449  fsum3cvg3  11822  fisumrev2  11872  isumshft  11916  cvgratnnlemseq  11952  cvgratnnlemabsle  11953  cvgratnnlemsumlt  11954  cvgratz  11958  oddge22np1  12307  nn0o  12333  bitsmod  12382  uzwodc  12473  dvdsnprmd  12562  prmgt1  12569  oddprmgt2  12571  oddprmge3  12572  prm23ge5  12702  nninfdclemcl  12934  nninfdclemp1  12936  nninfdclemlt  12937  strleund  13050  strleun  13051  gsumfzz  13442  gsumfzcl  13446  gsumfzreidx  13788  gsumfzsubmcl  13789  gsumfzmptfidmadd  13790  gsumfzmhm  13794  gsumfzfsum  14465  znidomb  14535  plyaddlem1  15334  2logb9irr  15558  2logb9irrap  15564  lgsdilem2  15628  gausslemma2dlem2  15654  gausslemma2dlem4  15656  gausslemma2dlem5  15658  gausslemma2dlem6  15659  lgsquadlem1  15669  lgsquadlem3  15671  2lgslem1  15683