Theorem eluzel2 9492

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 9490	. . . 4 |- ZZ>= : ZZ --> ~P ZZ
2		frel 5352	. . . 4 |- ( ZZ>= : ZZ --> ~P ZZ -> Rel ZZ>= )
3	1, 2	ax-mp 5	. . 3 |- Rel ZZ>=
4		relelfvdm 5528	. . 3 |- ( ( Rel ZZ>= /\ N e. ( ZZ>= ` M ) ) -> M e. dom ZZ>= )
5	3, 4	mpan 422	. 2 |- ( N e. ( ZZ>= ` M ) -> M e. dom ZZ>= )
6	1	fdmi 5355	. 2 |- dom ZZ>= = ZZ
7	5, 6	eleqtrdi 2263	1 |- ( N e. ( ZZ>= ` M ) -> M e. ZZ )

Syntax hints:   -> wi 4   e. wcel 2141   ~Pcpw 3566   dom cdm 4611   Rel wrel 4616   -->wf 5194   ` cfv 5198   ZZcz 9212   ZZ>=cuz 9487

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-14 2144  ax-ext 2152  ax-sep 4107  ax-pow 4160  ax-pr 4194  ax-cnex 7865  ax-resscn 7866

This theorem depends on definitions:  df-bi 116  df-3or 974  df-3an 975  df-tru 1351  df-nf 1454  df-sb 1756  df-eu 2022  df-mo 2023  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-ral 2453  df-rex 2454  df-rab 2457  df-v 2732  df-sbc 2956  df-un 3125  df-in 3127  df-ss 3134  df-pw 3568  df-sn 3589  df-pr 3590  df-op 3592  df-uni 3797  df-br 3990  df-opab 4051  df-mpt 4052  df-id 4278  df-xp 4617  df-rel 4618  df-cnv 4619  df-co 4620  df-dm 4621  df-rn 4622  df-res 4623  df-ima 4624  df-iota 5160  df-fun 5200  df-fn 5201  df-f 5202  df-fv 5206  df-ov 5856  df-neg 8093  df-z 9213  df-uz 9488

This theorem is referenced by:  eluz2  9493  uztrn  9503  uzneg  9505  uzss  9507  uz11  9509  eluzadd  9515  uzm1  9517  uzin  9519  uzind4  9547  elfz5  9973  elfzel1  9980  eluzfz1  9987  fzsplit2  10006  fzopth  10017  fzpred  10026  fzpreddisj  10027  fzdifsuc  10037  uzsplit  10048  uzdisj  10049  elfzp12  10055  fzm1  10056  uznfz  10059  nn0disj  10094  fzolb  10109  fzoss2  10128  fzouzdisj  10136  ige2m2fzo  10154  elfzonelfzo  10186  frec2uzrand  10361  frecfzen2  10383  seq3p1  10418  seqp1cd  10422  seq3clss  10423  seq3feq2  10426  seq3fveq  10427  seq3shft2  10429  ser3mono  10434  seq3split  10435  seq3caopr3  10437  seq3caopr2  10438  seq3f1olemp  10458  seq3f1oleml  10459  seq3f1o  10460  seq3id3  10463  seq3id  10464  seq3homo  10466  seq3z  10467  seq3distr  10469  ser3ge0  10473  ser3le  10474  leexp2a  10529  hashfz  10756  hashfzo  10757  hashfzp1  10759  seq3coll  10777  rexanuz2  10955  cau4  11080  clim2ser  11300  clim2ser2  11301  climserle  11308  fsum3cvg  11341  fsum3cvg2  11357  fsumsersdc  11358  fsum3ser  11360  fsumm1  11379  fsum1p  11381  telfsumo  11429  fsumparts  11433  cvgcmpub  11439  isumsplit  11454  cvgratnnlemmn  11488  clim2prod  11502  clim2divap  11503  prodfrecap  11509  prodfdivap  11510  ntrivcvgap  11511  fproddccvg  11535  fprodm1  11561  fprodabs  11579  fprodeq0  11580  uzwodc  11992  pcaddlem  12292  inffz  14101