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

Theorem hlatl 29847
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 29846 . 2  |-  ( K  e.  HL  ->  K  e.  CvLat )
2 cvlatl 29812 . 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 1721   AtLatcal 29751   CvLatclc 29752   HLchlt 29837
This theorem is referenced by:  hllat  29850  hlomcmat  29851  intnatN  29893  cvratlem  29907  atcvrj0  29914  atcvrneN  29916  atcvrj1  29917  atcvrj2b  29918  atltcvr  29921  cvrat4  29929  2atjm  29931  atbtwn  29932  3dim2  29954  2dim  29956  1cvrjat  29961  ps-2  29964  ps-2b  29968  islln3  29996  llnnleat  29999  llnexatN  30007  2llnmat  30010  2atm  30013  2llnm3N  30055  2llnm4  30056  2llnmeqat  30057  dalem21  30180  dalem24  30183  dalem25  30184  dalem54  30212  dalem55  30213  dalem57  30215  pmapat  30249  pmapeq0  30252  isline4N  30263  2lnat  30270  2llnma1b  30272  cdlema2N  30278  cdlemblem  30279  pmapjat1  30339  llnexchb2lem  30354  pol1N  30396  pnonsingN  30419  pclfinclN  30436  lhpocnle  30502  lhpmat  30516  lhpmatb  30517  lhp2at0  30518  lhp2atnle  30519  lhp2at0nle  30521  lhpat3  30532  4atexlemcnd  30558  ltrnmw  30637  trlatn0  30658  ltrnnidn  30660  trlnidatb  30663  trlnle  30672  trlval3  30673  trlval4  30674  cdlemc5  30681  cdleme0e  30703  cdleme3  30723  cdleme7c  30731  cdleme7ga  30734  cdleme7  30735  cdleme11k  30754  cdleme15b  30761  cdleme16b  30765  cdleme16e  30768  cdleme16f  30769  cdlemednpq  30785  cdleme20zN  30787  cdleme20y  30788  cdleme20j  30804  cdleme22aa  30825  cdleme22cN  30828  cdleme22d  30829  cdlemf2  31048  cdlemb3  31092  cdlemg12e  31133  cdlemg17dALTN  31150  cdlemg19a  31169  cdlemg27b  31182  cdlemg31d  31186  cdlemg33c  31194  cdlemg33e  31196  trlcone  31214  cdlemi  31306  tendotr  31316  cdlemk17  31344  cdlemk52  31440  cdleml1N  31462  dian0  31526  dia0  31539  dia2dimlem1  31551  dia2dimlem2  31552  dia2dimlem3  31553  dih0cnv  31770  dihmeetlem4preN  31793  dihmeetlem7N  31797  dihmeetlem17N  31810  dihlspsnat  31820  dihatexv  31825
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2389
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2395  df-cleq 2401  df-clel 2404  df-nfc 2533  df-ral 2675  df-rex 2676  df-rab 2679  df-v 2922  df-dif 3287  df-un 3289  df-in 3291  df-ss 3298  df-nul 3593  df-if 3704  df-sn 3784  df-pr 3785  df-op 3787  df-uni 3980  df-br 4177  df-iota 5381  df-fv 5425  df-ov 6047  df-cvlat 29809  df-hlat 29838
  Copyright terms: Public domain W3C validator