Theorem eluzel2 9821

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 9819	. . . 4 |- ZZ>= : ZZ --> ~P ZZ
2		frel 5494	. . . 4 |- ( ZZ>= : ZZ --> ~P ZZ -> Rel ZZ>= )
3	1, 2	ax-mp 5	. . 3 |- Rel ZZ>=
4		relelfvdm 5680	. . 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 5497	. 2 |- dom ZZ>= = ZZ
7	5, 6	eleqtrdi 2324	1 |- ( N e. ( ZZ>= ` M ) -> M e. ZZ )

Syntax hints:   -> wi 4   e. wcel 2202   ~Pcpw 3656   dom cdm 4731   Rel wrel 4736   -->wf 5329   ` cfv 5333   ZZcz 9540   ZZ>=cuz 9816

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 2205  ax-ext 2213  ax-sep 4212  ax-pow 4270  ax-pr 4305  ax-cnex 8183  ax-resscn 8184

This theorem depends on definitions:  df-bi 117  df-3or 1006  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1811  df-eu 2082  df-mo 2083  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-ral 2516  df-rex 2517  df-rab 2520  df-v 2805  df-sbc 3033  df-un 3205  df-in 3207  df-ss 3214  df-pw 3658  df-sn 3679  df-pr 3680  df-op 3682  df-uni 3899  df-br 4094  df-opab 4156  df-mpt 4157  df-id 4396  df-xp 4737  df-rel 4738  df-cnv 4739  df-co 4740  df-dm 4741  df-rn 4742  df-res 4743  df-ima 4744  df-iota 5293  df-fun 5335  df-fn 5336  df-f 5337  df-fv 5341  df-ov 6031  df-neg 8412  df-z 9541  df-uz 9817

This theorem is referenced by:  eluz2  9822  uztrn  9834  uzneg  9836  uzss  9838  uz11  9840  eluzadd  9846  uzm1  9848  uzin  9850  uzind4  9883  elfz5  10314  elfzel1  10321  eluzfz1  10328  fzsplit2  10347  fzopth  10358  fzpred  10367  fzpreddisj  10368  fzdifsuc  10378  uzsplit  10389  uzdisj  10390  elfzp12  10396  fzm1  10397  uznfz  10400  nn0disj  10435  fzolb  10451  fzoss2  10471  fzouzdisj  10479  fzoun  10480  ige2m2fzo  10506  elfzonelfzo  10538  frec2uzrand  10730  frecfzen2  10752  seq3p1  10790  seqp1cd  10795  seq3clss  10796  seq3feq2  10801  seqfveqg  10803  seq3fveq  10804  seq3shft2  10806  seqshft2g  10807  ser3mono  10812  seq3split  10813  seqsplitg  10814  seq3caopr3  10816  seqcaopr3g  10817  seq3caopr2  10818  seq3f1olemp  10840  seq3f1oleml  10841  seq3f1o  10842  seqf1oglem2a  10843  seqf1oglem1  10844  seqf1oglem2  10845  seqf1og  10846  seq3id3  10849  seq3id  10850  seq3homo  10852  seq3z  10853  seqhomog  10855  seqfeq4g  10856  seq3distr  10857  ser3ge0  10861  ser3le  10862  leexp2a  10917  hashfz  11148  hashfzo  11149  hashfzp1  11151  seq3coll  11169  rexanuz2  11631  cau4  11756  clim2ser  11977  clim2ser2  11978  climserle  11985  fsum3cvg  12019  fsum3cvg2  12035  fsumsersdc  12036  fsum3ser  12038  fsumm1  12057  fsum1p  12059  telfsumo  12107  fsumparts  12111  cvgcmpub  12117  isumsplit  12132  cvgratnnlemmn  12166  clim2prod  12180  clim2divap  12181  prodfrecap  12187  prodfdivap  12188  ntrivcvgap  12189  fproddccvg  12213  fprodm1  12239  fprodabs  12257  fprodeq0  12258  uzwodc  12688  pcaddlem  12992  fngsum  13551  igsumvalx  13552  gsumfzval  13554  gsumval2  13560  gsumfzz  13658  gsumfzconst  14008  gsumfzfsumlemm  14683  inffz  16805  gsumgfsumlem  16812