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

Theorem atelch 23847
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 23846 . 2  |- HAtoms  C_  CH
21sseli 3344 1  |-  ( A  e. HAtoms  ->  A  e.  CH )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1725   CHcch 22432  HAtomscat 22468
This theorem is referenced by:  atsseq  23850  atcveq0  23851  chcv1  23858  chcv2  23859  hatomistici  23865  chrelati  23867  chrelat2i  23868  cvati  23869  cvexchlem  23871  cvp  23878  atnemeq0  23880  atcv0eq  23882  atcv1  23883  atexch  23884  atomli  23885  atoml2i  23886  atordi  23887  atcvatlem  23888  atcvati  23889  atcvat2i  23890  chirredlem1  23893  chirredlem2  23894  chirredlem3  23895  chirredlem4  23896  chirredi  23897  atcvat3i  23899  atcvat4i  23900  atdmd  23901  atmd  23902  atmd2  23903  atabsi  23904  mdsymlem2  23907  mdsymlem3  23908  mdsymlem5  23910  mdsymlem8  23913  atdmd2  23917  sumdmdi  23923  dmdbr4ati  23924  dmdbr5ati  23925  dmdbr6ati  23926
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-rab 2714  df-in 3327  df-ss 3334  df-at 23841
  Copyright terms: Public domain W3C validator