Theorem hlatl 39806

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

Syntax hints:   → wi 4   ∈ wcel 2114  AtLatcal 39710  CvLatclc 39711  HLchlt 39796

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-iota 6454  df-fv 6506  df-ov 7370  df-cvlat 39768  df-hlat 39797

This theorem is referenced by:  hllat  39809  hlomcmat  39811  intnatN  39853  cvratlem  39867  atcvrj0  39874  atcvrneN  39876  atcvrj1  39877  atcvrj2b  39878  atltcvr  39881  cvrat4  39889  2atjm  39891  atbtwn  39892  3dim2  39914  2dim  39916  1cvrjat  39921  ps-2  39924  ps-2b  39928  islln3  39956  llnnleat  39959  llnexatN  39967  2llnmat  39970  2atm  39973  2llnm3N  40015  2llnm4  40016  2llnmeqat  40017  dalem21  40140  dalem24  40143  dalem25  40144  dalem54  40172  dalem55  40173  dalem57  40175  pmapat  40209  pmapeq0  40212  isline4N  40223  2lnat  40230  2llnma1b  40232  cdlema2N  40238  cdlemblem  40239  pmapjat1  40299  llnexchb2lem  40314  pol1N  40356  pnonsingN  40379  pclfinclN  40396  lhpocnle  40462  lhpmat  40476  lhpmatb  40477  lhp2at0  40478  lhp2atnle  40479  lhp2at0nle  40481  lhpat3  40492  4atexlemcnd  40518  trlatn0  40618  ltrnnidn  40620  trlnidatb  40623  trlnle  40632  trlval3  40633  trlval4  40634  cdlemc5  40641  cdleme0e  40663  cdleme3  40683  cdleme7c  40691  cdleme7ga  40694  cdleme7  40695  cdleme11k  40714  cdleme15b  40721  cdleme16b  40725  cdleme16e  40728  cdleme16f  40729  cdlemednpq  40745  cdleme20zN  40747  cdleme20j  40764  cdleme22aa  40785  cdleme22cN  40788  cdleme22d  40789  cdlemf2  41008  cdlemb3  41052  cdlemg12e  41093  cdlemg17dALTN  41110  cdlemg19a  41129  cdlemg27b  41142  cdlemg31d  41146  cdlemg33c  41154  cdlemg33e  41156  trlcone  41174  cdlemi  41266  tendotr  41276  cdlemk17  41304  cdlemk52  41400  cdleml1N  41422  dian0  41485  dia0  41498  dia2dimlem1  41510  dia2dimlem2  41511  dia2dimlem3  41512  dih0cnv  41729  dihmeetlem4preN  41752  dihmeetlem7N  41756  dihmeetlem17N  41769  dihlspsnat  41779  dihatexv  41784