Theorem hlatl 39820

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

Syntax hints:   → wi 4   ∈ wcel 2114  AtLatcal 39724  CvLatclc 39725  HLchlt 39810

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 2709

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 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-iota 6448  df-fv 6500  df-ov 7363  df-cvlat 39782  df-hlat 39811

This theorem is referenced by:  hllat  39823  hlomcmat  39825  intnatN  39867  cvratlem  39881  atcvrj0  39888  atcvrneN  39890  atcvrj1  39891  atcvrj2b  39892  atltcvr  39895  cvrat4  39903  2atjm  39905  atbtwn  39906  3dim2  39928  2dim  39930  1cvrjat  39935  ps-2  39938  ps-2b  39942  islln3  39970  llnnleat  39973  llnexatN  39981  2llnmat  39984  2atm  39987  2llnm3N  40029  2llnm4  40030  2llnmeqat  40031  dalem21  40154  dalem24  40157  dalem25  40158  dalem54  40186  dalem55  40187  dalem57  40189  pmapat  40223  pmapeq0  40226  isline4N  40237  2lnat  40244  2llnma1b  40246  cdlema2N  40252  cdlemblem  40253  pmapjat1  40313  llnexchb2lem  40328  pol1N  40370  pnonsingN  40393  pclfinclN  40410  lhpocnle  40476  lhpmat  40490  lhpmatb  40491  lhp2at0  40492  lhp2atnle  40493  lhp2at0nle  40495  lhpat3  40506  4atexlemcnd  40532  trlatn0  40632  ltrnnidn  40634  trlnidatb  40637  trlnle  40646  trlval3  40647  trlval4  40648  cdlemc5  40655  cdleme0e  40677  cdleme3  40697  cdleme7c  40705  cdleme7ga  40708  cdleme7  40709  cdleme11k  40728  cdleme15b  40735  cdleme16b  40739  cdleme16e  40742  cdleme16f  40743  cdlemednpq  40759  cdleme20zN  40761  cdleme20j  40778  cdleme22aa  40799  cdleme22cN  40802  cdleme22d  40803  cdlemf2  41022  cdlemb3  41066  cdlemg12e  41107  cdlemg17dALTN  41124  cdlemg19a  41143  cdlemg27b  41156  cdlemg31d  41160  cdlemg33c  41168  cdlemg33e  41170  trlcone  41188  cdlemi  41280  tendotr  41290  cdlemk17  41318  cdlemk52  41414  cdleml1N  41436  dian0  41499  dia0  41512  dia2dimlem1  41524  dia2dimlem2  41525  dia2dimlem3  41526  dih0cnv  41743  dihmeetlem4preN  41766  dihmeetlem7N  41770  dihmeetlem17N  41783  dihlspsnat  41793  dihatexv  41798