Theorem hlatl 38218

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

Syntax hints:   → wi 4   ∈ wcel 2106  AtLatcal 38122  CvLatclc 38123  HLchlt 38208

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-iota 6492  df-fv 6548  df-ov 7408  df-cvlat 38180  df-hlat 38209

This theorem is referenced by:  hllat  38221  hlomcmat  38223  intnatN  38266  cvratlem  38280  atcvrj0  38287  atcvrneN  38289  atcvrj1  38290  atcvrj2b  38291  atltcvr  38294  cvrat4  38302  2atjm  38304  atbtwn  38305  3dim2  38327  2dim  38329  1cvrjat  38334  ps-2  38337  ps-2b  38341  islln3  38369  llnnleat  38372  llnexatN  38380  2llnmat  38383  2atm  38386  2llnm3N  38428  2llnm4  38429  2llnmeqat  38430  dalem21  38553  dalem24  38556  dalem25  38557  dalem54  38585  dalem55  38586  dalem57  38588  pmapat  38622  pmapeq0  38625  isline4N  38636  2lnat  38643  2llnma1b  38645  cdlema2N  38651  cdlemblem  38652  pmapjat1  38712  llnexchb2lem  38727  pol1N  38769  pnonsingN  38792  pclfinclN  38809  lhpocnle  38875  lhpmat  38889  lhpmatb  38890  lhp2at0  38891  lhp2atnle  38892  lhp2at0nle  38894  lhpat3  38905  4atexlemcnd  38931  trlatn0  39031  ltrnnidn  39033  trlnidatb  39036  trlnle  39045  trlval3  39046  trlval4  39047  cdlemc5  39054  cdleme0e  39076  cdleme3  39096  cdleme7c  39104  cdleme7ga  39107  cdleme7  39108  cdleme11k  39127  cdleme15b  39134  cdleme16b  39138  cdleme16e  39141  cdleme16f  39142  cdlemednpq  39158  cdleme20zN  39160  cdleme20j  39177  cdleme22aa  39198  cdleme22cN  39201  cdleme22d  39202  cdlemf2  39421  cdlemb3  39465  cdlemg12e  39506  cdlemg17dALTN  39523  cdlemg19a  39542  cdlemg27b  39555  cdlemg31d  39559  cdlemg33c  39567  cdlemg33e  39569  trlcone  39587  cdlemi  39679  tendotr  39689  cdlemk17  39717  cdlemk52  39813  cdleml1N  39835  dian0  39898  dia0  39911  dia2dimlem1  39923  dia2dimlem2  39924  dia2dimlem3  39925  dih0cnv  40142  dihmeetlem4preN  40165  dihmeetlem7N  40169  dihmeetlem17N  40182  dihlspsnat  40192  dihatexv  40197