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

Theorem eluzelz 8482
Description: A member of an upper set of integers is an integer. (Contributed by NM, 6-Sep-2005.)
Assertion
Ref Expression
eluzelz (𝑁 ∈ (ℤ𝑀) → 𝑁 ∈ ℤ)

Proof of Theorem eluzelz
StepHypRef Expression
1 eluz2 8479 . 2 (𝑁 ∈ (ℤ𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀𝑁))
21simp2bi 920 1 (𝑁 ∈ (ℤ𝑀) → 𝑁 ∈ ℤ)
Colors of variables: wff set class
Syntax hints:  wi 4  wcel 1393   class class class wbr 3764  cfv 4902  cle 7061  cz 8245  cuz 8473
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 630  ax-5 1336  ax-7 1337  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-10 1396  ax-11 1397  ax-i12 1398  ax-bndl 1399  ax-4 1400  ax-14 1405  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-i5r 1428  ax-ext 2022  ax-sep 3875  ax-pow 3927  ax-pr 3944  ax-cnex 6975  ax-resscn 6976
This theorem depends on definitions:  df-bi 110  df-3or 886  df-3an 887  df-tru 1246  df-nf 1350  df-sb 1646  df-eu 1903  df-mo 1904  df-clab 2027  df-cleq 2033  df-clel 2036  df-nfc 2167  df-ral 2311  df-rex 2312  df-rab 2315  df-v 2559  df-sbc 2765  df-un 2922  df-in 2924  df-ss 2931  df-pw 3361  df-sn 3381  df-pr 3382  df-op 3384  df-uni 3581  df-br 3765  df-opab 3819  df-mpt 3820  df-id 4030  df-xp 4351  df-rel 4352  df-cnv 4353  df-co 4354  df-dm 4355  df-rn 4356  df-res 4357  df-ima 4358  df-iota 4867  df-fun 4904  df-fn 4905  df-f 4906  df-fv 4910  df-ov 5515  df-neg 7185  df-z 8246  df-uz 8474
This theorem is referenced by:  eluzelre  8483  uztrn  8489  uzneg  8491  uzssz  8492  uzss  8493  eluzp1l  8497  eluzaddi  8499  eluzsubi  8500  eluzadd  8501  eluzsub  8502  uzm1  8503  uzin  8505  uzind4  8531  uz2mulcl  8545  elfz5  8882  elfzel2  8888  elfzelz  8890  eluzfz2  8896  peano2fzr  8901  fzsplit2  8914  fzopth  8924  fzsuc  8931  elfzp1  8934  fzdifsuc  8943  uzsplit  8954  uzdisj  8955  fzm1  8962  fzneuz  8963  uznfz  8965  nn0disj  8995  elfzo3  9019  fzoss2  9028  fzouzsplit  9035  eluzgtdifelfzo  9053  fzosplitsnm1  9065  fzofzp1b  9084  elfzonelfzo  9086  fzosplitsn  9089  fzisfzounsn  9092  frec2uzltd  9189  frecfzen2  9204  iseqfveq2  9228  iseqfeq2  9229  iseqshft2  9232  monoord  9235  monoord2  9236  isermono  9237  iseqsplit  9238  iseqid  9247  leexp2a  9307  expnlbnd2  9374  rexuz3  9588  r19.2uz  9591  cau4  9712  caubnd2  9713  clim  9802  climshft2  9827  climaddc1  9849  climmulc2  9851  climsubc1  9852  climsubc2  9853  clim2iser  9857  clim2iser2  9858  iiserex  9859  climlec2  9861  climub  9864  climcau  9866  climcaucn  9870  serif0  9871
  Copyright terms: Public domain W3C validator