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

Theorem atelch 22979
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 22978 . 2  |- HAtoms  C_  CH
21sseli 3210 1  |-  ( A  e. HAtoms  ->  A  e.  CH )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1701   CHcch 21564  HAtomscat 21600
This theorem is referenced by:  atsseq  22982  atcveq0  22983  chcv1  22990  chcv2  22991  hatomistici  22997  chrelati  22999  chrelat2i  23000  cvati  23001  cvexchlem  23003  cvp  23010  atnemeq0  23012  atcv0eq  23014  atcv1  23015  atexch  23016  atomli  23017  atoml2i  23018  atordi  23019  atcvatlem  23020  atcvati  23021  atcvat2i  23022  chirredlem1  23025  chirredlem2  23026  chirredlem3  23027  chirredlem4  23028  chirredi  23029  atcvat3i  23031  atcvat4i  23032  atdmd  23033  atmd  23034  atmd2  23035  atabsi  23036  mdsymlem2  23039  mdsymlem3  23040  mdsymlem5  23042  mdsymlem8  23045  atdmd2  23049  sumdmdi  23055  dmdbr4ati  23056  dmdbr5ati  23057  dmdbr6ati  23058
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1537  ax-5 1548  ax-17 1607  ax-9 1645  ax-8 1666  ax-6 1720  ax-7 1725  ax-11 1732  ax-12 1897  ax-ext 2297
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1533  df-nf 1536  df-sb 1640  df-clab 2303  df-cleq 2309  df-clel 2312  df-nfc 2441  df-rab 2586  df-in 3193  df-ss 3200  df-at 22973
  Copyright terms: Public domain W3C validator