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

Theorem hlatl 33665
Description: A Hilbert lattice is atomic. (Contributed by NM, 20-Oct-2011.)
Assertion
Ref Expression
hlatl (𝐾 ∈ HL → 𝐾 ∈ AtLat)

Proof of Theorem hlatl
StepHypRef Expression
1 hlcvl 33664 . 2 (𝐾 ∈ HL → 𝐾 ∈ CvLat)
2 cvlatl 33630 . 2 (𝐾 ∈ CvLat → 𝐾 ∈ AtLat)
31, 2syl 17 1 (𝐾 ∈ HL → 𝐾 ∈ AtLat)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1977  AtLatcal 33569  CvLatclc 33570  HLchlt 33655
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-iota 5768  df-fv 5812  df-ov 6552  df-cvlat 33627  df-hlat 33656
This theorem is referenced by:  hllat  33668  hlomcmat  33669  intnatN  33711  cvratlem  33725  atcvrj0  33732  atcvrneN  33734  atcvrj1  33735  atcvrj2b  33736  atltcvr  33739  cvrat4  33747  2atjm  33749  atbtwn  33750  3dim2  33772  2dim  33774  1cvrjat  33779  ps-2  33782  ps-2b  33786  islln3  33814  llnnleat  33817  llnexatN  33825  2llnmat  33828  2atm  33831  2llnm3N  33873  2llnm4  33874  2llnmeqat  33875  dalem21  33998  dalem24  34001  dalem25  34002  dalem54  34030  dalem55  34031  dalem57  34033  pmapat  34067  pmapeq0  34070  isline4N  34081  2lnat  34088  2llnma1b  34090  cdlema2N  34096  cdlemblem  34097  pmapjat1  34157  llnexchb2lem  34172  pol1N  34214  pnonsingN  34237  pclfinclN  34254  lhpocnle  34320  lhpmat  34334  lhpmatb  34335  lhp2at0  34336  lhp2atnle  34337  lhp2at0nle  34339  lhpat3  34350  4atexlemcnd  34376  ltrnmwOLD  34456  trlatn0  34477  ltrnnidn  34479  trlnidatb  34482  trlnle  34491  trlval3  34492  trlval4  34493  cdlemc5  34500  cdleme0e  34522  cdleme3  34542  cdleme7c  34550  cdleme7ga  34553  cdleme7  34554  cdleme11k  34573  cdleme15b  34580  cdleme16b  34584  cdleme16e  34587  cdleme16f  34588  cdlemednpq  34604  cdleme20zN  34606  cdleme20yOLD  34608  cdleme20j  34624  cdleme22aa  34645  cdleme22cN  34648  cdleme22d  34649  cdlemf2  34868  cdlemb3  34912  cdlemg12e  34953  cdlemg17dALTN  34970  cdlemg19a  34989  cdlemg27b  35002  cdlemg31d  35006  cdlemg33c  35014  cdlemg33e  35016  trlcone  35034  cdlemi  35126  tendotr  35136  cdlemk17  35164  cdlemk52  35260  cdleml1N  35282  dian0  35346  dia0  35359  dia2dimlem1  35371  dia2dimlem2  35372  dia2dimlem3  35373  dih0cnv  35590  dihmeetlem4preN  35613  dihmeetlem7N  35617  dihmeetlem17N  35630  dihlspsnat  35640  dihatexv  35645
  Copyright terms: Public domain W3C validator