Theorem eluz2 9564

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 9563	. 2 |- ( N e. ( ZZ>= ` M ) -> M e. ZZ )
2		simp1 999	. 2 |- ( ( M e. ZZ /\ N e. ZZ /\ M <_ N ) -> M e. ZZ )
3		eluz1 9562	. . . 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 984	. . 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 705	1 |- ( N e. ( ZZ>= ` M ) <-> ( M e. ZZ /\ N e. ZZ /\ M <_ N ) )

Syntax hints:   /\ wa 104   <-> wb 105   /\ w3a 980   e. wcel 2160   class class class wbr 4018   ` cfv 5235   <_ cle 8023   ZZcz 9283   ZZ>=cuz 9558

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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-14 2163  ax-ext 2171  ax-sep 4136  ax-pow 4192  ax-pr 4227  ax-cnex 7932  ax-resscn 7933

This theorem depends on definitions:  df-bi 117  df-3or 981  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-eu 2041  df-mo 2042  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-ral 2473  df-rex 2474  df-rab 2477  df-v 2754  df-sbc 2978  df-un 3148  df-in 3150  df-ss 3157  df-pw 3592  df-sn 3613  df-pr 3614  df-op 3616  df-uni 3825  df-br 4019  df-opab 4080  df-mpt 4081  df-id 4311  df-xp 4650  df-rel 4651  df-cnv 4652  df-co 4653  df-dm 4654  df-rn 4655  df-res 4656  df-ima 4657  df-iota 5196  df-fun 5237  df-fn 5238  df-f 5239  df-fv 5243  df-ov 5899  df-neg 8161  df-z 9284  df-uz 9559

This theorem is referenced by:  eluzuzle  9566  eluzelz  9567  eluzle  9570  uztrn  9574  eluzp1p1  9583  uznn0sub  9589  uz3m2nn  9603  1eluzge0  9604  2eluzge1  9606  raluz2  9609  rexuz2  9611  peano2uz  9613  nn0pzuz  9617  uzind4  9618  nn0ge2m1nnALT  9648  elfzuzb  10049  uzsubsubfz  10077  ige2m1fz  10140  4fvwrd4  10170  elfzo2  10180  elfzouz2  10191  fzossrbm1  10203  fzossfzop1  10242  ssfzo12bi  10255  elfzonelfzo  10260  elfzomelpfzo  10261  fzosplitprm1  10264  fzostep1  10267  fzind2  10269  flqword2  10320  fldiv4p1lem1div2  10336  uzennn  10467  seq3split  10510  iseqf1olemqk  10525  seq3f1olemqsumkj  10529  seq3f1olemqsumk  10530  seq3f1olemqsum  10531  bcval5  10775  seq3coll  10854  seq3shft  10879  resqrexlemoverl  11062  resqrexlemga  11064  fsum3cvg3  11436  fisumrev2  11486  isumshft  11530  cvgratnnlemseq  11566  cvgratnnlemabsle  11567  cvgratnnlemsumlt  11568  cvgratz  11572  oddge22np1  11918  nn0o  11944  suprzubdc  11985  zsupssdc  11987  uzwodc  12070  dvdsnprmd  12157  prmgt1  12164  oddprmgt2  12166  oddprmge3  12167  prm23ge5  12296  nninfdclemcl  12499  nninfdclemp1  12501  nninfdclemlt  12502  strleund  12615  strleun  12616  cnfldstr  13866  2logb9irr  14846  2logb9irrap  14852  lgsdilem2  14895