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

Theorem hlatl 30158
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 30157 . 2  |-  ( K  e.  HL  ->  K  e.  CvLat )
2 cvlatl 30123 . 2  |-  ( K  e.  CvLat  ->  K  e.  AtLat
)
31, 2syl 16 1  |-  ( K  e.  HL  ->  K  e.  AtLat )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1725   AtLatcal 30062   CvLatclc 30063   HLchlt 30148
This theorem is referenced by:  hllat  30161  hlomcmat  30162  intnatN  30204  cvratlem  30218  atcvrj0  30225  atcvrneN  30227  atcvrj1  30228  atcvrj2b  30229  atltcvr  30232  cvrat4  30240  2atjm  30242  atbtwn  30243  3dim2  30265  2dim  30267  1cvrjat  30272  ps-2  30275  ps-2b  30279  islln3  30307  llnnleat  30310  llnexatN  30318  2llnmat  30321  2atm  30324  2llnm3N  30366  2llnm4  30367  2llnmeqat  30368  dalem21  30491  dalem24  30494  dalem25  30495  dalem54  30523  dalem55  30524  dalem57  30526  pmapat  30560  pmapeq0  30563  isline4N  30574  2lnat  30581  2llnma1b  30583  cdlema2N  30589  cdlemblem  30590  pmapjat1  30650  llnexchb2lem  30665  pol1N  30707  pnonsingN  30730  pclfinclN  30747  lhpocnle  30813  lhpmat  30827  lhpmatb  30828  lhp2at0  30829  lhp2atnle  30830  lhp2at0nle  30832  lhpat3  30843  4atexlemcnd  30869  ltrnmw  30948  trlatn0  30969  ltrnnidn  30971  trlnidatb  30974  trlnle  30983  trlval3  30984  trlval4  30985  cdlemc5  30992  cdleme0e  31014  cdleme3  31034  cdleme7c  31042  cdleme7ga  31045  cdleme7  31046  cdleme11k  31065  cdleme15b  31072  cdleme16b  31076  cdleme16e  31079  cdleme16f  31080  cdlemednpq  31096  cdleme20zN  31098  cdleme20y  31099  cdleme20j  31115  cdleme22aa  31136  cdleme22cN  31139  cdleme22d  31140  cdlemf2  31359  cdlemb3  31403  cdlemg12e  31444  cdlemg17dALTN  31461  cdlemg19a  31480  cdlemg27b  31493  cdlemg31d  31497  cdlemg33c  31505  cdlemg33e  31507  trlcone  31525  cdlemi  31617  tendotr  31627  cdlemk17  31655  cdlemk52  31751  cdleml1N  31773  dian0  31837  dia0  31850  dia2dimlem1  31862  dia2dimlem2  31863  dia2dimlem3  31864  dih0cnv  32081  dihmeetlem4preN  32104  dihmeetlem7N  32108  dihmeetlem17N  32121  dihlspsnat  32131  dihatexv  32136
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-3an 938  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-ral 2710  df-rex 2711  df-rab 2714  df-v 2958  df-dif 3323  df-un 3325  df-in 3327  df-ss 3334  df-nul 3629  df-if 3740  df-sn 3820  df-pr 3821  df-op 3823  df-uni 4016  df-br 4213  df-iota 5418  df-fv 5462  df-ov 6084  df-cvlat 30120  df-hlat 30149
  Copyright terms: Public domain W3C validator