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

Theorem atelch 29543
 Description: An atom is a Hilbert lattice element. (Contributed by NM, 22-Jun-2004.) (New usage is discouraged.)
Assertion
Ref Expression
atelch (𝐴 ∈ HAtoms → 𝐴C )

Proof of Theorem atelch
StepHypRef Expression
1 atssch 29542 . 2 HAtoms ⊆ C
21sseli 3748 1 (𝐴 ∈ HAtoms → 𝐴C )
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∈ wcel 2145   Cℋ cch 28126  HAtomscat 28162 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751 This theorem depends on definitions:  df-bi 197  df-an 383  df-or 835  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-rab 3070  df-in 3730  df-ss 3737  df-at 29537 This theorem is referenced by:  atsseq  29546  atcveq0  29547  chcv1  29554  chcv2  29555  hatomistici  29561  chrelati  29563  chrelat2i  29564  cvati  29565  cvexchlem  29567  cvp  29574  atnemeq0  29576  atcv0eq  29578  atcv1  29579  atexch  29580  atomli  29581  atoml2i  29582  atordi  29583  atcvatlem  29584  atcvati  29585  atcvat2i  29586  chirredlem1  29589  chirredlem2  29590  chirredlem3  29591  chirredlem4  29592  chirredi  29593  atcvat3i  29595  atcvat4i  29596  atdmd  29597  atmd  29598  atmd2  29599  atabsi  29600  mdsymlem2  29603  mdsymlem3  29604  mdsymlem5  29606  mdsymlem8  29609  atdmd2  29613  sumdmdi  29619  dmdbr4ati  29620  dmdbr5ati  29621  dmdbr6ati  29622
 Copyright terms: Public domain W3C validator