Theorem hlatl 39348

Description: A Hilbert lattice is atomic. (Contributed by NM, 20-Oct-2011.)

Assertion

Ref	Expression
hlatl	⊢ (𝐾 ∈ HL → 𝐾 ∈ AtLat)

Proof of Theorem hlatl

Step	Hyp	Ref	Expression
1		hlcvl 39347	. 2 ⊢ (𝐾 ∈ HL → 𝐾 ∈ CvLat)
2		cvlatl 39313	. 2 ⊢ (𝐾 ∈ CvLat → 𝐾 ∈ AtLat)
3	1, 2	syl 17	1 ⊢ (𝐾 ∈ HL → 𝐾 ∈ AtLat)

Syntax hints:   → wi 4   ∈ wcel 2109  AtLatcal 39252  CvLatclc 39253  HLchlt 39338

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3919  df-un 3921  df-in 3923  df-ss 3933  df-nul 4299  df-if 4491  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4874  df-br 5110  df-iota 6466  df-fv 6521  df-ov 7392  df-cvlat 39310  df-hlat 39339

This theorem is referenced by:  hllat  39351  hlomcmat  39353  intnatN  39396  cvratlem  39410  atcvrj0  39417  atcvrneN  39419  atcvrj1  39420  atcvrj2b  39421  atltcvr  39424  cvrat4  39432  2atjm  39434  atbtwn  39435  3dim2  39457  2dim  39459  1cvrjat  39464  ps-2  39467  ps-2b  39471  islln3  39499  llnnleat  39502  llnexatN  39510  2llnmat  39513  2atm  39516  2llnm3N  39558  2llnm4  39559  2llnmeqat  39560  dalem21  39683  dalem24  39686  dalem25  39687  dalem54  39715  dalem55  39716  dalem57  39718  pmapat  39752  pmapeq0  39755  isline4N  39766  2lnat  39773  2llnma1b  39775  cdlema2N  39781  cdlemblem  39782  pmapjat1  39842  llnexchb2lem  39857  pol1N  39899  pnonsingN  39922  pclfinclN  39939  lhpocnle  40005  lhpmat  40019  lhpmatb  40020  lhp2at0  40021  lhp2atnle  40022  lhp2at0nle  40024  lhpat3  40035  4atexlemcnd  40061  trlatn0  40161  ltrnnidn  40163  trlnidatb  40166  trlnle  40175  trlval3  40176  trlval4  40177  cdlemc5  40184  cdleme0e  40206  cdleme3  40226  cdleme7c  40234  cdleme7ga  40237  cdleme7  40238  cdleme11k  40257  cdleme15b  40264  cdleme16b  40268  cdleme16e  40271  cdleme16f  40272  cdlemednpq  40288  cdleme20zN  40290  cdleme20j  40307  cdleme22aa  40328  cdleme22cN  40331  cdleme22d  40332  cdlemf2  40551  cdlemb3  40595  cdlemg12e  40636  cdlemg17dALTN  40653  cdlemg19a  40672  cdlemg27b  40685  cdlemg31d  40689  cdlemg33c  40697  cdlemg33e  40699  trlcone  40717  cdlemi  40809  tendotr  40819  cdlemk17  40847  cdlemk52  40943  cdleml1N  40965  dian0  41028  dia0  41041  dia2dimlem1  41053  dia2dimlem2  41054  dia2dimlem3  41055  dih0cnv  41272  dihmeetlem4preN  41295  dihmeetlem7N  41299  dihmeetlem17N  41312  dihlspsnat  41322  dihatexv  41327