Theorem hlatl 39324

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 39323	. 2 ⊢ (𝐾 ∈ HL → 𝐾 ∈ CvLat)
2		cvlatl 39289	. 2 ⊢ (𝐾 ∈ CvLat → 𝐾 ∈ AtLat)
3	1, 2	syl 17	1 ⊢ (𝐾 ∈ HL → 𝐾 ∈ AtLat)

Syntax hints:   → wi 4   ∈ wcel 2108  AtLatcal 39228  CvLatclc 39229  HLchlt 39314

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707

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 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-iota 6483  df-fv 6538  df-ov 7406  df-cvlat 39286  df-hlat 39315

This theorem is referenced by:  hllat  39327  hlomcmat  39329  intnatN  39372  cvratlem  39386  atcvrj0  39393  atcvrneN  39395  atcvrj1  39396  atcvrj2b  39397  atltcvr  39400  cvrat4  39408  2atjm  39410  atbtwn  39411  3dim2  39433  2dim  39435  1cvrjat  39440  ps-2  39443  ps-2b  39447  islln3  39475  llnnleat  39478  llnexatN  39486  2llnmat  39489  2atm  39492  2llnm3N  39534  2llnm4  39535  2llnmeqat  39536  dalem21  39659  dalem24  39662  dalem25  39663  dalem54  39691  dalem55  39692  dalem57  39694  pmapat  39728  pmapeq0  39731  isline4N  39742  2lnat  39749  2llnma1b  39751  cdlema2N  39757  cdlemblem  39758  pmapjat1  39818  llnexchb2lem  39833  pol1N  39875  pnonsingN  39898  pclfinclN  39915  lhpocnle  39981  lhpmat  39995  lhpmatb  39996  lhp2at0  39997  lhp2atnle  39998  lhp2at0nle  40000  lhpat3  40011  4atexlemcnd  40037  trlatn0  40137  ltrnnidn  40139  trlnidatb  40142  trlnle  40151  trlval3  40152  trlval4  40153  cdlemc5  40160  cdleme0e  40182  cdleme3  40202  cdleme7c  40210  cdleme7ga  40213  cdleme7  40214  cdleme11k  40233  cdleme15b  40240  cdleme16b  40244  cdleme16e  40247  cdleme16f  40248  cdlemednpq  40264  cdleme20zN  40266  cdleme20j  40283  cdleme22aa  40304  cdleme22cN  40307  cdleme22d  40308  cdlemf2  40527  cdlemb3  40571  cdlemg12e  40612  cdlemg17dALTN  40629  cdlemg19a  40648  cdlemg27b  40661  cdlemg31d  40665  cdlemg33c  40673  cdlemg33e  40675  trlcone  40693  cdlemi  40785  tendotr  40795  cdlemk17  40823  cdlemk52  40919  cdleml1N  40941  dian0  41004  dia0  41017  dia2dimlem1  41029  dia2dimlem2  41030  dia2dimlem3  41031  dih0cnv  41248  dihmeetlem4preN  41271  dihmeetlem7N  41275  dihmeetlem17N  41288  dihlspsnat  41298  dihatexv  41303