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

Theorem hlatl 29550
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 29549 . 2  |-  ( K  e.  HL  ->  K  e.  CvLat )
2 cvlatl 29515 . 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 1684   AtLatcal 29454   CvLatclc 29455   HLchlt 29540
This theorem is referenced by:  hllat  29553  hlomcmat  29554  intnatN  29596  cvratlem  29610  atcvrj0  29617  atcvrneN  29619  atcvrj1  29620  atcvrj2b  29621  atltcvr  29624  cvrat4  29632  2atjm  29634  atbtwn  29635  3dim2  29657  2dim  29659  1cvrjat  29664  ps-2  29667  ps-2b  29671  islln3  29699  llnnleat  29702  llnexatN  29710  2llnmat  29713  2atm  29716  2llnm3N  29758  2llnm4  29759  2llnmeqat  29760  dalem21  29883  dalem24  29886  dalem25  29887  dalem54  29915  dalem55  29916  dalem57  29918  pmapat  29952  pmapeq0  29955  isline4N  29966  2lnat  29973  2llnma1b  29975  cdlema2N  29981  cdlemblem  29982  pmapjat1  30042  llnexchb2lem  30057  pol1N  30099  pnonsingN  30122  pclfinclN  30139  lhpocnle  30205  lhpmat  30219  lhpmatb  30220  lhp2at0  30221  lhp2atnle  30222  lhp2at0nle  30224  lhpat3  30235  4atexlemcnd  30261  ltrnmw  30340  trlatn0  30361  ltrnnidn  30363  trlnidatb  30366  trlnle  30375  trlval3  30376  trlval4  30377  cdlemc5  30384  cdleme0e  30406  cdleme3  30426  cdleme7c  30434  cdleme7ga  30437  cdleme7  30438  cdleme11k  30457  cdleme15b  30464  cdleme16b  30468  cdleme16e  30471  cdleme16f  30472  cdlemednpq  30488  cdleme20zN  30490  cdleme20y  30491  cdleme20j  30507  cdleme22aa  30528  cdleme22cN  30531  cdleme22d  30532  cdlemf2  30751  cdlemb3  30795  cdlemg12e  30836  cdlemg17dALTN  30853  cdlemg19a  30872  cdlemg27b  30885  cdlemg31d  30889  cdlemg33c  30897  cdlemg33e  30899  trlcone  30917  cdlemi  31009  tendotr  31019  cdlemk17  31047  cdlemk52  31143  cdleml1N  31165  dian0  31229  dia0  31242  dia2dimlem1  31254  dia2dimlem2  31255  dia2dimlem3  31256  dih0cnv  31473  dihmeetlem4preN  31496  dihmeetlem7N  31500  dihmeetlem17N  31513  dihlspsnat  31523  dihatexv  31528
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-3an 936  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-ral 2548  df-rex 2549  df-rab 2552  df-v 2790  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-uni 3828  df-br 4024  df-iota 5219  df-fv 5263  df-ov 5861  df-cvlat 29512  df-hlat 29541
  Copyright terms: Public domain W3C validator