Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  hlatl Unicode version

Theorem hlatl 29602
Description: A Hilbert lattice is atomic. (Contributed by NM, 20-Oct-2011.)
Assertion
Ref Expression
hlatl  |-  ( K  e.  HL  ->  K  e.  AtLat )

Proof of Theorem hlatl
StepHypRef Expression
1 hlcvl 29601 . 2  |-  ( K  e.  HL  ->  K  e.  CvLat )
2 cvlatl 29567 . 2  |-  ( K  e.  CvLat  ->  K  e.  AtLat
)
31, 2syl 15 1  |-  ( K  e.  HL  ->  K  e.  AtLat )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1710   AtLatcal 29506   CvLatclc 29507   HLchlt 29592
This theorem is referenced by:  hllat  29605  hlomcmat  29606  intnatN  29648  cvratlem  29662  atcvrj0  29669  atcvrneN  29671  atcvrj1  29672  atcvrj2b  29673  atltcvr  29676  cvrat4  29684  2atjm  29686  atbtwn  29687  3dim2  29709  2dim  29711  1cvrjat  29716  ps-2  29719  ps-2b  29723  islln3  29751  llnnleat  29754  llnexatN  29762  2llnmat  29765  2atm  29768  2llnm3N  29810  2llnm4  29811  2llnmeqat  29812  dalem21  29935  dalem24  29938  dalem25  29939  dalem54  29967  dalem55  29968  dalem57  29970  pmapat  30004  pmapeq0  30007  isline4N  30018  2lnat  30025  2llnma1b  30027  cdlema2N  30033  cdlemblem  30034  pmapjat1  30094  llnexchb2lem  30109  pol1N  30151  pnonsingN  30174  pclfinclN  30191  lhpocnle  30257  lhpmat  30271  lhpmatb  30272  lhp2at0  30273  lhp2atnle  30274  lhp2at0nle  30276  lhpat3  30287  4atexlemcnd  30313  ltrnmw  30392  trlatn0  30413  ltrnnidn  30415  trlnidatb  30418  trlnle  30427  trlval3  30428  trlval4  30429  cdlemc5  30436  cdleme0e  30458  cdleme3  30478  cdleme7c  30486  cdleme7ga  30489  cdleme7  30490  cdleme11k  30509  cdleme15b  30516  cdleme16b  30520  cdleme16e  30523  cdleme16f  30524  cdlemednpq  30540  cdleme20zN  30542  cdleme20y  30543  cdleme20j  30559  cdleme22aa  30580  cdleme22cN  30583  cdleme22d  30584  cdlemf2  30803  cdlemb3  30847  cdlemg12e  30888  cdlemg17dALTN  30905  cdlemg19a  30924  cdlemg27b  30937  cdlemg31d  30941  cdlemg33c  30949  cdlemg33e  30951  trlcone  30969  cdlemi  31061  tendotr  31071  cdlemk17  31099  cdlemk52  31195  cdleml1N  31217  dian0  31281  dia0  31294  dia2dimlem1  31306  dia2dimlem2  31307  dia2dimlem3  31308  dih0cnv  31525  dihmeetlem4preN  31548  dihmeetlem7N  31552  dihmeetlem17N  31565  dihlspsnat  31575  dihatexv  31580
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2345  df-cleq 2351  df-clel 2354  df-nfc 2483  df-ral 2624  df-rex 2625  df-rab 2628  df-v 2866  df-dif 3231  df-un 3233  df-in 3235  df-ss 3242  df-nul 3532  df-if 3642  df-sn 3722  df-pr 3723  df-op 3725  df-uni 3907  df-br 4103  df-iota 5298  df-fv 5342  df-ov 5945  df-cvlat 29564  df-hlat 29593
  Copyright terms: Public domain W3C validator