ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  eluzel2 Unicode version

Theorem eluzel2 8705
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
StepHypRef Expression
1 uzf 8703 . . . 4  |-  ZZ>= : ZZ --> ~P ZZ
2 frel 5080 . . . 4  |-  ( ZZ>= : ZZ --> ~P ZZ  ->  Rel  ZZ>= )
31, 2ax-mp 7 . . 3  |-  Rel  ZZ>=
4 relelfvdm 5237 . . 3  |-  ( ( Rel  ZZ>=  /\  N  e.  ( ZZ>= `  M )
)  ->  M  e.  dom  ZZ>= )
53, 4mpan 415 . 2  |-  ( N  e.  ( ZZ>= `  M
)  ->  M  e.  dom  ZZ>= )
61fdmi 5082 . 2  |-  dom  ZZ>=  =  ZZ
75, 6syl6eleq 2172 1  |-  ( N  e.  ( ZZ>= `  M
)  ->  M  e.  ZZ )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1434   ~Pcpw 3390   dom cdm 4371   Rel wrel 4376   -->wf 4928   ` cfv 4932   ZZcz 8432   ZZ>=cuz 8700
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 663  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-14 1446  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2064  ax-sep 3904  ax-pow 3956  ax-pr 3972  ax-cnex 7129  ax-resscn 7130
This theorem depends on definitions:  df-bi 115  df-3or 921  df-3an 922  df-tru 1288  df-nf 1391  df-sb 1687  df-eu 1945  df-mo 1946  df-clab 2069  df-cleq 2075  df-clel 2078  df-nfc 2209  df-ral 2354  df-rex 2355  df-rab 2358  df-v 2604  df-sbc 2817  df-un 2978  df-in 2980  df-ss 2987  df-pw 3392  df-sn 3412  df-pr 3413  df-op 3415  df-uni 3610  df-br 3794  df-opab 3848  df-mpt 3849  df-id 4056  df-xp 4377  df-rel 4378  df-cnv 4379  df-co 4380  df-dm 4381  df-rn 4382  df-res 4383  df-ima 4384  df-iota 4897  df-fun 4934  df-fn 4935  df-f 4936  df-fv 4940  df-ov 5546  df-neg 7349  df-z 8433  df-uz 8701
This theorem is referenced by:  eluz2  8706  uztrn  8716  uzneg  8718  uzss  8720  uz11  8722  eluzadd  8728  uzm1  8730  uzin  8732  uzind4  8757  elfz5  9113  elfzel1  9120  eluzfz1  9126  fzsplit2  9145  fzopth  9155  fzpred  9163  fzpreddisj  9164  fzdifsuc  9174  uzsplit  9185  uzdisj  9186  elfzp12  9192  fzm1  9193  uznfz  9196  nn0disj  9225  fzolb  9239  fzoss2  9258  fzouzdisj  9266  ige2m2fzo  9284  elfzonelfzo  9316  frec2uzrand  9487  frecfzen2  9509  iseqcl  9537  iseqp1  9538  iseqp1t  9539  iseqfeq2  9545  iseqfveq  9546  iseqshft2  9548  iseqsplit  9554  iseqcaopr3  9556  iseqid3s  9562  iseqid  9563  iseqhomo  9565  iseqz  9566  serige0  9570  serile  9571  leexp2a  9626  rexanuz2  10015  cau4  10140  clim2iser  10313  clim2iser2  10314  climserile  10321  fisumcvg  10338
  Copyright terms: Public domain W3C validator