HSE Home Hilbert Space Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  HSE Home  >  Th. List  >  atelch Unicode version

Theorem atelch 22924
Description: An atom is a Hilbert lattice element. (Contributed by NM, 22-Jun-2004.) (New usage is discouraged.)
Assertion
Ref Expression
atelch  |-  ( A  e. HAtoms  ->  A  e.  CH )

Proof of Theorem atelch
StepHypRef Expression
1 atssch 22923 . 2  |- HAtoms  C_  CH
21sseli 3176 1  |-  ( A  e. HAtoms  ->  A  e.  CH )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1684   CHcch 21509  HAtomscat 21545
This theorem is referenced by:  atsseq  22927  atcveq0  22928  chcv1  22935  chcv2  22936  hatomistici  22942  chrelati  22944  chrelat2i  22945  cvati  22946  cvexchlem  22948  cvp  22955  atnemeq0  22957  atcv0eq  22959  atcv1  22960  atexch  22961  atomli  22962  atoml2i  22963  atordi  22964  atcvatlem  22965  atcvati  22966  atcvat2i  22967  chirredlem1  22970  chirredlem2  22971  chirredlem3  22972  chirredlem4  22973  chirredi  22974  atcvat3i  22976  atcvat4i  22977  atdmd  22978  atmd  22979  atmd2  22980  atabsi  22981  mdsymlem2  22984  mdsymlem3  22985  mdsymlem5  22987  mdsymlem8  22990  atdmd2  22994  sumdmdi  23000  dmdbr4ati  23001  dmdbr5ati  23002  dmdbr6ati  23003
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-rab 2552  df-in 3159  df-ss 3166  df-at 22918
  Copyright terms: Public domain W3C validator