Theorem eluzel2 9655

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 9653	. . . 4 |- ZZ>= : ZZ --> ~P ZZ
2		frel 5432	. . . 4 |- ( ZZ>= : ZZ --> ~P ZZ -> Rel ZZ>= )
3	1, 2	ax-mp 5	. . 3 |- Rel ZZ>=
4		relelfvdm 5610	. . 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 5435	. 2 |- dom ZZ>= = ZZ
7	5, 6	eleqtrdi 2298	1 |- ( N e. ( ZZ>= ` M ) -> M e. ZZ )

Syntax hints:   -> wi 4   e. wcel 2176   ~Pcpw 3616   dom cdm 4676   Rel wrel 4681   -->wf 5268   ` cfv 5272   ZZcz 9374   ZZ>=cuz 9650

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 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-14 2179  ax-ext 2187  ax-sep 4163  ax-pow 4219  ax-pr 4254  ax-cnex 8018  ax-resscn 8019

This theorem depends on definitions:  df-bi 117  df-3or 982  df-3an 983  df-tru 1376  df-nf 1484  df-sb 1786  df-eu 2057  df-mo 2058  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-ral 2489  df-rex 2490  df-rab 2493  df-v 2774  df-sbc 2999  df-un 3170  df-in 3172  df-ss 3179  df-pw 3618  df-sn 3639  df-pr 3640  df-op 3642  df-uni 3851  df-br 4046  df-opab 4107  df-mpt 4108  df-id 4341  df-xp 4682  df-rel 4683  df-cnv 4684  df-co 4685  df-dm 4686  df-rn 4687  df-res 4688  df-ima 4689  df-iota 5233  df-fun 5274  df-fn 5275  df-f 5276  df-fv 5280  df-ov 5949  df-neg 8248  df-z 9375  df-uz 9651

This theorem is referenced by:  eluz2  9656  uztrn  9667  uzneg  9669  uzss  9671  uz11  9673  eluzadd  9679  uzm1  9681  uzin  9683  uzind4  9711  elfz5  10141  elfzel1  10148  eluzfz1  10155  fzsplit2  10174  fzopth  10185  fzpred  10194  fzpreddisj  10195  fzdifsuc  10205  uzsplit  10216  uzdisj  10217  elfzp12  10223  fzm1  10224  uznfz  10227  nn0disj  10262  fzolb  10278  fzoss2  10298  fzouzdisj  10306  ige2m2fzo  10329  elfzonelfzo  10361  frec2uzrand  10552  frecfzen2  10574  seq3p1  10612  seqp1cd  10617  seq3clss  10618  seq3feq2  10623  seqfveqg  10625  seq3fveq  10626  seq3shft2  10628  seqshft2g  10629  ser3mono  10634  seq3split  10635  seqsplitg  10636  seq3caopr3  10638  seqcaopr3g  10639  seq3caopr2  10640  seq3f1olemp  10662  seq3f1oleml  10663  seq3f1o  10664  seqf1oglem2a  10665  seqf1oglem1  10666  seqf1oglem2  10667  seqf1og  10668  seq3id3  10671  seq3id  10672  seq3homo  10674  seq3z  10675  seqhomog  10677  seqfeq4g  10678  seq3distr  10679  ser3ge0  10683  ser3le  10684  leexp2a  10739  hashfz  10968  hashfzo  10969  hashfzp1  10971  seq3coll  10989  rexanuz2  11335  cau4  11460  clim2ser  11681  clim2ser2  11682  climserle  11689  fsum3cvg  11722  fsum3cvg2  11738  fsumsersdc  11739  fsum3ser  11741  fsumm1  11760  fsum1p  11762  telfsumo  11810  fsumparts  11814  cvgcmpub  11820  isumsplit  11835  cvgratnnlemmn  11869  clim2prod  11883  clim2divap  11884  prodfrecap  11890  prodfdivap  11891  ntrivcvgap  11892  fproddccvg  11916  fprodm1  11942  fprodabs  11960  fprodeq0  11961  uzwodc  12391  pcaddlem  12695  fngsum  13253  igsumvalx  13254  gsumfzval  13256  gsumval2  13262  gsumfzz  13360  gsumfzconst  13710  gsumfzfsumlemm  14382  inffz  16048