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

Theorem hlatl 32358
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 32357 . 2  |-  ( K  e.  HL  ->  K  e.  CvLat )
2 cvlatl 32323 . 2  |-  ( K  e.  CvLat  ->  K  e.  AtLat
)
31, 2syl 17 1  |-  ( K  e.  HL  ->  K  e.  AtLat )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1842   AtLatcal 32262   CvLatclc 32263   HLchlt 32348
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 976  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-ral 2758  df-rex 2759  df-rab 2762  df-v 3060  df-dif 3416  df-un 3418  df-in 3420  df-ss 3427  df-nul 3738  df-if 3885  df-sn 3972  df-pr 3974  df-op 3978  df-uni 4191  df-br 4395  df-iota 5532  df-fv 5576  df-ov 6280  df-cvlat 32320  df-hlat 32349
This theorem is referenced by:  hllat  32361  hlomcmat  32362  intnatN  32404  cvratlem  32418  atcvrj0  32425  atcvrneN  32427  atcvrj1  32428  atcvrj2b  32429  atltcvr  32432  cvrat4  32440  2atjm  32442  atbtwn  32443  3dim2  32465  2dim  32467  1cvrjat  32472  ps-2  32475  ps-2b  32479  islln3  32507  llnnleat  32510  llnexatN  32518  2llnmat  32521  2atm  32524  2llnm3N  32566  2llnm4  32567  2llnmeqat  32568  dalem21  32691  dalem24  32694  dalem25  32695  dalem54  32723  dalem55  32724  dalem57  32726  pmapat  32760  pmapeq0  32763  isline4N  32774  2lnat  32781  2llnma1b  32783  cdlema2N  32789  cdlemblem  32790  pmapjat1  32850  llnexchb2lem  32865  pol1N  32907  pnonsingN  32930  pclfinclN  32947  lhpocnle  33013  lhpmat  33027  lhpmatb  33028  lhp2at0  33029  lhp2atnle  33030  lhp2at0nle  33032  lhpat3  33043  4atexlemcnd  33069  ltrnmwOLD  33149  trlatn0  33170  ltrnnidn  33172  trlnidatb  33175  trlnle  33184  trlval3  33185  trlval4  33186  cdlemc5  33193  cdleme0e  33215  cdleme3  33235  cdleme7c  33243  cdleme7ga  33246  cdleme7  33247  cdleme11k  33266  cdleme15b  33273  cdleme16b  33277  cdleme16e  33280  cdleme16f  33281  cdlemednpq  33297  cdleme20zN  33299  cdleme20yOLD  33301  cdleme20j  33317  cdleme22aa  33338  cdleme22cN  33341  cdleme22d  33342  cdlemf2  33561  cdlemb3  33605  cdlemg12e  33646  cdlemg17dALTN  33663  cdlemg19a  33682  cdlemg27b  33695  cdlemg31d  33699  cdlemg33c  33707  cdlemg33e  33709  trlcone  33727  cdlemi  33819  tendotr  33829  cdlemk17  33857  cdlemk52  33953  cdleml1N  33975  dian0  34039  dia0  34052  dia2dimlem1  34064  dia2dimlem2  34065  dia2dimlem3  34066  dih0cnv  34283  dihmeetlem4preN  34306  dihmeetlem7N  34310  dihmeetlem17N  34323  dihlspsnat  34333  dihatexv  34338
  Copyright terms: Public domain W3C validator