Theorem eluzel2 9858

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 9856	. . . 4 |- ZZ>= : ZZ --> ~P ZZ
2		frel 5513	. . . 4 |- ( ZZ>= : ZZ --> ~P ZZ -> Rel ZZ>= )
3	1, 2	ax-mp 5	. . 3 |- Rel ZZ>=
4		relelfvdm 5702	. . 3 |- ( ( Rel ZZ>= /\ N e. ( ZZ>= ` M ) ) -> M e. dom ZZ>= )
5	3, 4	mpan 424	. 2 |- ( N e. ( ZZ>= ` M ) -> M e. dom ZZ>= )
6	1	fdmi 5516	. 2 |- dom ZZ>= = ZZ
7	5, 6	eleqtrdi 2325	1 |- ( N e. ( ZZ>= ` M ) -> M e. ZZ )

Syntax hints:   -> wi 4   e. wcel 2203   ~Pcpw 3669   dom cdm 4749   Rel wrel 4754   -->wf 5348   ` cfv 5352   ZZcz 9577   ZZ>=cuz 9853

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-14 2206  ax-ext 2214  ax-sep 4228  ax-pow 4287  ax-pr 4322  ax-cnex 8218  ax-resscn 8219

This theorem depends on definitions:  df-bi 117  df-3or 1006  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-eu 2083  df-mo 2084  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-ral 2525  df-rex 2526  df-rab 2529  df-v 2815  df-sbc 3043  df-un 3215  df-in 3217  df-ss 3224  df-pw 3671  df-sn 3695  df-pr 3696  df-op 3698  df-uni 3915  df-br 4110  df-opab 4172  df-mpt 4173  df-id 4414  df-xp 4755  df-rel 4756  df-cnv 4757  df-co 4758  df-dm 4759  df-rn 4760  df-res 4761  df-ima 4762  df-iota 5312  df-fun 5354  df-fn 5355  df-f 5356  df-fv 5360  df-ov 6053  df-neg 8447  df-z 9578  df-uz 9854

This theorem is referenced by:  eluz2  9859  uztrn  9871  uzneg  9873  uzss  9875  uz11  9877  eluzadd  9883  uzm1  9885  uzin  9887  uzind4  9920  elfz5  10351  elfzel1  10358  eluzfz1  10365  fzsplit2  10384  fzopth  10395  fzpred  10404  fzpreddisj  10405  fzdifsuc  10415  uzsplit  10426  uzdisj  10427  elfzp12  10433  fzm1  10434  uznfz  10437  nn0disj  10472  fzolb  10488  fzoss2  10508  fzouzdisj  10516  fzoun  10517  ige2m2fzo  10543  elfzonelfzo  10575  frec2uzrand  10767  frecfzen2  10789  seq3p1  10827  seqp1cd  10832  seq3clss  10833  seq3feq2  10838  seqfveqg  10840  seq3fveq  10841  seq3shft2  10843  seqshft2g  10844  ser3mono  10849  seq3split  10850  seqsplitg  10851  seq3caopr3  10853  seqcaopr3g  10854  seq3caopr2  10855  seq3f1olemp  10877  seq3f1oleml  10878  seq3f1o  10879  seqf1oglem2a  10880  seqf1oglem1  10881  seqf1oglem2  10882  seqf1og  10883  seq3id3  10886  seq3id  10887  seq3homo  10889  seq3z  10890  seqhomog  10892  seqfeq4g  10893  seq3distr  10894  ser3ge0  10898  ser3le  10899  leexp2a  10954  hashfz  11186  hashfzo  11187  hashfzp1  11189  seq3coll  11214  rexanuz2  11676  cau4  11801  clim2ser  12022  clim2ser2  12023  climserle  12030  fsum3cvg  12064  fsum3cvg2  12080  fsumsersdc  12081  fsum3ser  12083  fsumm1  12102  fsum1p  12104  telfsumo  12152  fsumparts  12156  cvgcmpub  12162  isumsplit  12177  cvgratnnlemmn  12211  clim2prod  12225  clim2divap  12226  prodfrecap  12232  prodfdivap  12233  ntrivcvgap  12234  fproddccvg  12258  fprodm1  12284  fprodabs  12302  fprodeq0  12303  uzwodc  12733  pcaddlem  13037  fngsum  13601  igsumvalx  13602  gsumfzval  13604  gsumval2  13610  gsumfzz  13708  gsumfzconst  14058  gsumfzfsumlemm  14735  inffz  16858  gsumgfsumlem  16865