Theorem eluzel2 9535

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 9533	. . . 4 |- ZZ>= : ZZ --> ~P ZZ
2		frel 5372	. . . 4 |- ( ZZ>= : ZZ --> ~P ZZ -> Rel ZZ>= )
3	1, 2	ax-mp 5	. . 3 |- Rel ZZ>=
4		relelfvdm 5549	. . 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 5375	. 2 |- dom ZZ>= = ZZ
7	5, 6	eleqtrdi 2270	1 |- ( N e. ( ZZ>= ` M ) -> M e. ZZ )

Syntax hints:   -> wi 4   e. wcel 2148   ~Pcpw 3577   dom cdm 4628   Rel wrel 4633   -->wf 5214   ` cfv 5218   ZZcz 9255   ZZ>=cuz 9530

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-14 2151  ax-ext 2159  ax-sep 4123  ax-pow 4176  ax-pr 4211  ax-cnex 7904  ax-resscn 7905

This theorem depends on definitions:  df-bi 117  df-3or 979  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ral 2460  df-rex 2461  df-rab 2464  df-v 2741  df-sbc 2965  df-un 3135  df-in 3137  df-ss 3144  df-pw 3579  df-sn 3600  df-pr 3601  df-op 3603  df-uni 3812  df-br 4006  df-opab 4067  df-mpt 4068  df-id 4295  df-xp 4634  df-rel 4635  df-cnv 4636  df-co 4637  df-dm 4638  df-rn 4639  df-res 4640  df-ima 4641  df-iota 5180  df-fun 5220  df-fn 5221  df-f 5222  df-fv 5226  df-ov 5880  df-neg 8133  df-z 9256  df-uz 9531

This theorem is referenced by:  eluz2  9536  uztrn  9546  uzneg  9548  uzss  9550  uz11  9552  eluzadd  9558  uzm1  9560  uzin  9562  uzind4  9590  elfz5  10019  elfzel1  10026  eluzfz1  10033  fzsplit2  10052  fzopth  10063  fzpred  10072  fzpreddisj  10073  fzdifsuc  10083  uzsplit  10094  uzdisj  10095  elfzp12  10101  fzm1  10102  uznfz  10105  nn0disj  10140  fzolb  10155  fzoss2  10174  fzouzdisj  10182  ige2m2fzo  10200  elfzonelfzo  10232  frec2uzrand  10407  frecfzen2  10429  seq3p1  10464  seqp1cd  10468  seq3clss  10469  seq3feq2  10472  seq3fveq  10473  seq3shft2  10475  ser3mono  10480  seq3split  10481  seq3caopr3  10483  seq3caopr2  10484  seq3f1olemp  10504  seq3f1oleml  10505  seq3f1o  10506  seq3id3  10509  seq3id  10510  seq3homo  10512  seq3z  10513  seq3distr  10515  ser3ge0  10519  ser3le  10520  leexp2a  10575  hashfz  10803  hashfzo  10804  hashfzp1  10806  seq3coll  10824  rexanuz2  11002  cau4  11127  clim2ser  11347  clim2ser2  11348  climserle  11355  fsum3cvg  11388  fsum3cvg2  11404  fsumsersdc  11405  fsum3ser  11407  fsumm1  11426  fsum1p  11428  telfsumo  11476  fsumparts  11480  cvgcmpub  11486  isumsplit  11501  cvgratnnlemmn  11535  clim2prod  11549  clim2divap  11550  prodfrecap  11556  prodfdivap  11557  ntrivcvgap  11558  fproddccvg  11582  fprodm1  11608  fprodabs  11626  fprodeq0  11627  uzwodc  12040  pcaddlem  12340  inffz  14859