Theorem eluzel2 9942

Description: Implication of membership in an upper set of integers. (Contributed by NM, 6-Sep-2005.) (Revised by Mario Carneiro, 3-Nov-2013.)

Assertion

Ref	Expression
eluzel2	|- ( N e. ( ZZ>= ` M ) -> M e. ZZ )

Proof of Theorem eluzel2

Step	Hyp	Ref	Expression
1		uzf 9940	. . . 4 |- ZZ>= : ZZ --> ~P ZZ
2		frel 5541	. . . 4 |- ( ZZ>= : ZZ --> ~P ZZ -> Rel ZZ>= )
3	1, 2	ax-mp 5	. . 3 |- Rel ZZ>=
4		relelfvdm 5730	. . 3 |- ( ( Rel ZZ>= /\ N e. ( ZZ>= ` M ) ) -> M e. dom ZZ>= )
5	3, 4	mpan 428	. 2 |- ( N e. ( ZZ>= ` M ) -> M e. dom ZZ>= )
6	1	fdmi 5544	. 2 |- dom ZZ>= = ZZ
7	5, 6	eleqtrdi 2331	1 |- ( N e. ( ZZ>= ` M ) -> M e. ZZ )

This proof depends on syntax axioms:   -> wi 4   e. wcel 2209   ~Pcpw 3688   dom cdm 4776   Rel wrel 4781   -->wf 5376   ` cfv 5380   ZZcz 9655   ZZ>=cuz 9937

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-14 2212  ax-ext 2220  ax-sep 4251  ax-pow 4313  ax-pr 4348  ax-cnex 8276  ax-resscn 8277

This proof depends on definitions:  df-bi 117  df-3or 1010  df-3an 1011  df-tru 1405  df-nf 1514  df-sb 1816  df-eu 2089  df-mo 2090  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ral 2533  df-rex 2534  df-rab 2537  df-v 2823  df-sbc 3052  df-un 3224  df-in 3226  df-ss 3233  df-pw 3690  df-sn 3715  df-pr 3716  df-op 3718  df-uni 3936  df-br 4132  df-opab 4194  df-mpt 4195  df-id 4440  df-xp 4782  df-rel 4783  df-cnv 4784  df-co 4785  df-dm 4786  df-rn 4787  df-res 4788  df-ima 4789  df-iota 5340  df-fun 5382  df-fn 5383  df-f 5384  df-fv 5388  df-ov 6091  df-neg 8507  df-z 9656  df-uz 9938

This theorem is used by:  eluz2  9943  uztrn  9955  uzneg  9957  uzss  9959  uz11  9961  eluzadd  9967  uzm1  9969  uzin  9971  uzind4  10004  elfz5  10437  elfzel1  10444  eluzfz1  10452  fzsplit2  10472  fzopth  10484  fzpred  10494  fzpreddisj  10495  fzdifsuc  10505  uzsplit  10516  uzdisj  10517  elfzp12  10523  fzm1  10524  uznfz  10527  nn0disj  10562  fzolb  10578  fzoss2  10598  fzouzdisj  10606  fzoun  10607  ige2m2fzo  10633  elfzonelfzo  10665  frec2uzrand  10863  frecfzen2  10885  seq3p1  10923  seqp1cd  10928  seq3clss  10929  seq3feq2  10934  seqfveqg  10936  seq3fveq  10937  seq3shft2  10939  seqshft2g  10940  ser3mono  10945  seq3split  10946  seqsplitg  10947  seq3caopr3  10949  seqcaopr3g  10950  seq3caopr2  10951  seq3f1olemp  10973  seq3f1oleml  10974  seq3f1o  10975  seqf1oglem2a  10976  seqf1oglem1  10977  seqf1oglem2  10978  seqf1og  10979  seq3id3  10982  seq3id  10983  seq3homo  10985  seq3z  10986  seqhomog  10988  seqfeq4g  10989  seq3distr  10990  ser3ge0  10994  ser3le  10995  leexp2a  11050  hashfz  11284  hashfzo  11285  hashfzp1  11287  seq3coll  11316  rexanuz2  11779  cau4  11905  clim2ser  12128  clim2ser2  12129  climserle  12136  fsum3cvg  12170  fsum3cvg2  12186  fsumsersdc  12187  fsum3ser  12189  fsumm1  12208  fsum1p  12210  telfsumo  12258  fsumparts  12262  cvgcmpub  12268  isumsplit  12283  cvgratnnlemmn  12317  clim2prod  12331  clim2divap  12332  prodfrecap  12338  prodfdivap  12339  ntrivcvgap  12340  fproddccvg  12364  fprodm1  12390  fprodabs  12408  fprodeq0  12409  uzwodc  12839  pcaddlem  13147  prmlem0  13249  fngzsum  13767  gzsumvalx  13768  gzsumfzval  13770  gzsumval2  13773  gzsumconst  14233  gzsumshift  14239  logfac  16126  chtdif  16264  ppidif  16269  bcmono  16304  inffz  17329