Theorem hlatl 37374

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

Syntax hints:   → wi 4   ∈ wcel 2106  AtLatcal 37278  CvLatclc 37279  HLchlt 37364

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

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-br 5075  df-iota 6391  df-fv 6441  df-ov 7278  df-cvlat 37336  df-hlat 37365

This theorem is referenced by:  hllat  37377  hlomcmat  37379  intnatN  37421  cvratlem  37435  atcvrj0  37442  atcvrneN  37444  atcvrj1  37445  atcvrj2b  37446  atltcvr  37449  cvrat4  37457  2atjm  37459  atbtwn  37460  3dim2  37482  2dim  37484  1cvrjat  37489  ps-2  37492  ps-2b  37496  islln3  37524  llnnleat  37527  llnexatN  37535  2llnmat  37538  2atm  37541  2llnm3N  37583  2llnm4  37584  2llnmeqat  37585  dalem21  37708  dalem24  37711  dalem25  37712  dalem54  37740  dalem55  37741  dalem57  37743  pmapat  37777  pmapeq0  37780  isline4N  37791  2lnat  37798  2llnma1b  37800  cdlema2N  37806  cdlemblem  37807  pmapjat1  37867  llnexchb2lem  37882  pol1N  37924  pnonsingN  37947  pclfinclN  37964  lhpocnle  38030  lhpmat  38044  lhpmatb  38045  lhp2at0  38046  lhp2atnle  38047  lhp2at0nle  38049  lhpat3  38060  4atexlemcnd  38086  trlatn0  38186  ltrnnidn  38188  trlnidatb  38191  trlnle  38200  trlval3  38201  trlval4  38202  cdlemc5  38209  cdleme0e  38231  cdleme3  38251  cdleme7c  38259  cdleme7ga  38262  cdleme7  38263  cdleme11k  38282  cdleme15b  38289  cdleme16b  38293  cdleme16e  38296  cdleme16f  38297  cdlemednpq  38313  cdleme20zN  38315  cdleme20j  38332  cdleme22aa  38353  cdleme22cN  38356  cdleme22d  38357  cdlemf2  38576  cdlemb3  38620  cdlemg12e  38661  cdlemg17dALTN  38678  cdlemg19a  38697  cdlemg27b  38710  cdlemg31d  38714  cdlemg33c  38722  cdlemg33e  38724  trlcone  38742  cdlemi  38834  tendotr  38844  cdlemk17  38872  cdlemk52  38968  cdleml1N  38990  dian0  39053  dia0  39066  dia2dimlem1  39078  dia2dimlem2  39079  dia2dimlem3  39080  dih0cnv  39297  dihmeetlem4preN  39320  dihmeetlem7N  39324  dihmeetlem17N  39337  dihlspsnat  39347  dihatexv  39352