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 34127
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 34126 . 2 (𝐾 ∈ HL → 𝐾 ∈ CvLat)
2 cvlatl 34092 . 2 (𝐾 ∈ CvLat → 𝐾 ∈ AtLat)
31, 2syl 17 1 (𝐾 ∈ HL → 𝐾 ∈ AtLat)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1987  AtLatcal 34031  CvLatclc 34032  HLchlt 34117
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ral 2912  df-rex 2913  df-rab 2916  df-v 3188  df-dif 3558  df-un 3560  df-in 3562  df-ss 3569  df-nul 3892  df-if 4059  df-sn 4149  df-pr 4151  df-op 4155  df-uni 4403  df-br 4614  df-iota 5810  df-fv 5855  df-ov 6607  df-cvlat 34089  df-hlat 34118
This theorem is referenced by:  hllat  34130  hlomcmat  34131  intnatN  34173  cvratlem  34187  atcvrj0  34194  atcvrneN  34196  atcvrj1  34197  atcvrj2b  34198  atltcvr  34201  cvrat4  34209  2atjm  34211  atbtwn  34212  3dim2  34234  2dim  34236  1cvrjat  34241  ps-2  34244  ps-2b  34248  islln3  34276  llnnleat  34279  llnexatN  34287  2llnmat  34290  2atm  34293  2llnm3N  34335  2llnm4  34336  2llnmeqat  34337  dalem21  34460  dalem24  34463  dalem25  34464  dalem54  34492  dalem55  34493  dalem57  34495  pmapat  34529  pmapeq0  34532  isline4N  34543  2lnat  34550  2llnma1b  34552  cdlema2N  34558  cdlemblem  34559  pmapjat1  34619  llnexchb2lem  34634  pol1N  34676  pnonsingN  34699  pclfinclN  34716  lhpocnle  34782  lhpmat  34796  lhpmatb  34797  lhp2at0  34798  lhp2atnle  34799  lhp2at0nle  34801  lhpat3  34812  4atexlemcnd  34838  ltrnmwOLD  34918  trlatn0  34939  ltrnnidn  34941  trlnidatb  34944  trlnle  34953  trlval3  34954  trlval4  34955  cdlemc5  34962  cdleme0e  34984  cdleme3  35004  cdleme7c  35012  cdleme7ga  35015  cdleme7  35016  cdleme11k  35035  cdleme15b  35042  cdleme16b  35046  cdleme16e  35049  cdleme16f  35050  cdlemednpq  35066  cdleme20zN  35068  cdleme20yOLD  35070  cdleme20j  35086  cdleme22aa  35107  cdleme22cN  35110  cdleme22d  35111  cdlemf2  35330  cdlemb3  35374  cdlemg12e  35415  cdlemg17dALTN  35432  cdlemg19a  35451  cdlemg27b  35464  cdlemg31d  35468  cdlemg33c  35476  cdlemg33e  35478  trlcone  35496  cdlemi  35588  tendotr  35598  cdlemk17  35626  cdlemk52  35722  cdleml1N  35744  dian0  35808  dia0  35821  dia2dimlem1  35833  dia2dimlem2  35834  dia2dimlem3  35835  dih0cnv  36052  dihmeetlem4preN  36075  dihmeetlem7N  36079  dihmeetlem17N  36092  dihlspsnat  36102  dihatexv  36107
  Copyright terms: Public domain W3C validator