Theorem hlatl 39616

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

Syntax hints:   → wi 4   ∈ wcel 2113  AtLatcal 39520  CvLatclc 39521  HLchlt 39606

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-iota 6448  df-fv 6500  df-ov 7361  df-cvlat 39578  df-hlat 39607

This theorem is referenced by:  hllat  39619  hlomcmat  39621  intnatN  39663  cvratlem  39677  atcvrj0  39684  atcvrneN  39686  atcvrj1  39687  atcvrj2b  39688  atltcvr  39691  cvrat4  39699  2atjm  39701  atbtwn  39702  3dim2  39724  2dim  39726  1cvrjat  39731  ps-2  39734  ps-2b  39738  islln3  39766  llnnleat  39769  llnexatN  39777  2llnmat  39780  2atm  39783  2llnm3N  39825  2llnm4  39826  2llnmeqat  39827  dalem21  39950  dalem24  39953  dalem25  39954  dalem54  39982  dalem55  39983  dalem57  39985  pmapat  40019  pmapeq0  40022  isline4N  40033  2lnat  40040  2llnma1b  40042  cdlema2N  40048  cdlemblem  40049  pmapjat1  40109  llnexchb2lem  40124  pol1N  40166  pnonsingN  40189  pclfinclN  40206  lhpocnle  40272  lhpmat  40286  lhpmatb  40287  lhp2at0  40288  lhp2atnle  40289  lhp2at0nle  40291  lhpat3  40302  4atexlemcnd  40328  trlatn0  40428  ltrnnidn  40430  trlnidatb  40433  trlnle  40442  trlval3  40443  trlval4  40444  cdlemc5  40451  cdleme0e  40473  cdleme3  40493  cdleme7c  40501  cdleme7ga  40504  cdleme7  40505  cdleme11k  40524  cdleme15b  40531  cdleme16b  40535  cdleme16e  40538  cdleme16f  40539  cdlemednpq  40555  cdleme20zN  40557  cdleme20j  40574  cdleme22aa  40595  cdleme22cN  40598  cdleme22d  40599  cdlemf2  40818  cdlemb3  40862  cdlemg12e  40903  cdlemg17dALTN  40920  cdlemg19a  40939  cdlemg27b  40952  cdlemg31d  40956  cdlemg33c  40964  cdlemg33e  40966  trlcone  40984  cdlemi  41076  tendotr  41086  cdlemk17  41114  cdlemk52  41210  cdleml1N  41232  dian0  41295  dia0  41308  dia2dimlem1  41320  dia2dimlem2  41321  dia2dimlem3  41322  dih0cnv  41539  dihmeetlem4preN  41562  dihmeetlem7N  41566  dihmeetlem17N  41579  dihlspsnat  41589  dihatexv  41594